
›› 2013, Vol. 28 ›› Issue (2): 232246.doi: 10.1007/s1139001313255
• Theoretical Computer Science • Previous Articles Next Articles
Mohamed El Bachir Menai and Tasniem Nasser AlYahya
[1] Cook S A. The complexity of theoremproving procedures. InProc. the 3rd STOC, May 1971, pp.151158. [2] Kautz H, Selman B. Pushing the envelope: Planning, propositional logic, and stochastic search. In Proc. the 13th NationalConf. Artificial Intelligence, Aug. 1996, pp.11941201. [3] Gomes C P, Selman B, McAloon K, Tretkoff C. Randomization in backtrack search: Exploiting heavytailed profiles forsolving hard scheduling problems. In Proc. the 4th AIPS,June 1998, pp.208213. [4] Biere A, Cimatti A, Clarke E M, Fujita M, Zhu Y. Symbolicmodel checking using SAT procedures instead of BDDs. InProc. the 36th DAC, June 1999, pp.317320. [5] Abdulla P A, Bjesse P, Eén N. Symbolic reachability analysis based on SAT solvers. In Proc. the 6th TACAS, March25April 2, 2000, pp.411425. [6] Bjesse P, Leonard T, Mokkedem A. Finding bugs in an Alphamicroprocessor using satisfiability solvers. In Proc. the 13thCAV, July 2001, pp.454464. [7] Jackson D, Schechter I, Shlyakhter I. Alcoa: The alloy constraint analyzer. In Proc. the 22nd ICSE, June 2000, pp.730733. [8] Clarke E M, Kroening D, Lerda F. A tool for checking ANSIC programs. In Proc. the 10th TACAS, Mar. 29Apr. 2 2004,pp.168176. [9] Khurshid S, Marinov D. Testera: Specificationbased testingof Java programs using SAT. Automated Software Engineering, 2004, 11(4): 403434. [10] Buro M, BÄuning H K. Report on a SAT competition. Bulletin of the European Association for Theoretical ComputerScience, 1992, 49: 143151. [11] Simon L, Le Berre D, Hirsch E A. The SAT2002 competition. Annals of Mathematics and Artificial Intelligence, 2005,43(1): 307342. [12] Purdom P W, Le Berre D, Simon L. A parsimony tree for theSAT2002 competition. Annals of Mathematics and ArtificialIntelligence, 2005, 43(1): 343365. [13] MarquesSilva J P, Sakallah K A. GRASPA new search algorithm for satisfiability. In Proc. ICCAD 1996, Nov. 1996,pp.220227. [14] Moskewicz M W, Madigan C F, Zhao Y, Zhang L, Malik S.Chaff: Engineering an efficient SAT solver. In Proc. the 38thDAC, June 2001, pp.530535. [15] Goldberg E, Novikov Y. Berkmin: A fast and robust SATsolver. In Proc. DATE 2002, Mar. 2002, pp.142149. [16] Nadel A. The Jerusat SAT solver [Master's Thesis]. HebrewUniversity of Jerusalem, 2002. [17] Eén N, SÄorensson N. MiniSat: A SAT solver with con°ictclause minimization. In Proc. SAT 2005, June 2005, pp.502518. [18] Gu J. Efficient local search for very largescale satisfiabilityproblems. SIGART Bulletin, 1992, 3(1): 812. [19] Gent I P, Walsh T. Towards an understanding of hillclimbingprocedures for SAT. In Proc. the 11th AAAI, July 1993,pp.2833. [20] Ginsberg M L, McAllester D A. GSAT and dynamic backtracking. In Proc. the 2nd PPCP 1994, May 1994, pp.243265. [21] Konolige K. Easy to be hard: Difficult problems for greedyalgorithms. In Proc. the 4th KR, May 1994, pp.374378. [22] Cha B, Iwama K. Adding new clauses for faster local search.In Proc. the 13th AAAI, Aug. 1996, Vol.1, pp.332337. [23] Frank J, Cheeseman P, Stutz J. When gravity fails: Localsearch topology. Journal of Artificial Intelligence Research,1997, 7: 249281. [24] Gu J, Purdom P W, Franco J, Wah B W. Algorithms for thesatisfiability (SAT) problem: A survey. In Satisfiability Problem: Theory and Applications, Du D, Gu J, Pardalos R M(eds.), 1997, Vol.35, pp.19152. [25] Hoos H H. On the runtime behaviour of stochastic localsearch algorithms for SAT. In Proc. the 16th National Conf.Artificial Intelligence and 11th Innovation Applications ofArtificial Intelligence, July 1999, pp.661666. [26] Hoos H H. An adaptive noise mechanism for walkSAT. InProc. the 18th AAAI, July 28Aug. 1, 2002, pp.655660. [27] Li X Y, Stallmann M F, Brglez F. A local search SAT solverusing an effective switching strategy and an efficient unitpropagation. In Proc. the 6th SAT, May 2003, pp.5368. [28] Hoos H, StÄutzle T. Stochastic Local Search: Foundations &Applications. San Francisco, CA, USA: Morgan Kaufmann,2004. [29] Hirsch E A, Kojevnikov A. UnitWalk: A new SAT solver thatuses local search guided by unit clause elimination. Annalsof Mathematics and Artificial Intelligence, 2005, 43(1/4): 91111. [30] Mazure B, Saïs L, Grégoire E. Boosting complete techniquesthanks to local search methods. Annals of Mathematics andArtificial Intelligence, 1998, 22(3/4): 319331. [31] Rish I, Dechter R. To guess or to think? Hybrid algorithmsfor SAT. In Proc. the 2nd CP 1996, Aug. 1996, pp.555556. [32] Habet D, Li C M, Devendeville L, Vasquez M. A hybrid approach for SAT. In Proc. the 8th CP, Sept. 2002, pp.172184. [33] Anbulagan A, Pham D N, Slaney J, Sattar A. Old resolution meets modern SLS. In Proc. the 20th AAAI, July 2005,pp.354359. [34] Cook S A, Mitchell D G. Finding hard instances of thesatisfiability problem: A survey. In Satisfiability Problem:Theory and Applications, Du D, Gu J, Pardalos P M (eds.),1997, Vol.35, pp.117. [35] Dixon H E, Ginsberg M L, Parkes A J. Generalizing Booleansatisfiability I: Background and survey of existing work. Artificial Intelligence Research, 2004, 21: 193243. [36] Kautz H, Selman B. The state of SAT. Discrete Applied Mathematics, 2007, 155(12): 15141524. [37] MarquesSilva J. Practical applications of Boolean satisfiability. In Proc. the 9th WODES, May 2008, pp.7480. [38] Gomes C P, Kautz H, Sabharwal A, Selman B. Satisfiabilitysolvers. In Foundations of Artificial Intelligence, van Harmelen F, Lifschit Z, Porter B (eds.), 2008, Vol.3, pp.89134. [39] Biere A, Heule M J, van Maaren H, Walsh T (eds.). Handbook of Satisfiability. Frontiers in Artificial Intelligence andApplications, Vol.185, IOS Press, 2009. [40] Xu K, Boussemart F, Hemery F, Lecoutre C. Random constraint satisfaction: Easy generation of hard (satisfiable) instances. Artificial Intelligence, 2007, 171(8/9): 514534. [41] Shostak R E. An algorithm for reasoning about equality.Communications of the ACM, 1978, 21(7): 583585. [42] Shostak R E. A practical decision procedure for arithmeticwith function symbols. Journal of the ACM, 1979, 26(2):351360. [43] Nelson G, Oppen D C. Simplification by cooperating decisionprocedures. ACM Transactions on Programming Languagesand Systems, 1979, 1(2): 245257. [44] Nelson G, Oppen D C. Fast decision procedures based on congruence closure. Journal of the ACM, 1980, 27(2): 356364. [45] Shostak R E. Deciding combinations of theories. Journal ofthe ACM, 1984, 31(1): 112. [46] Boyer R S, Moore J S. Integrating decision procedures intoheuristic theorem provers: A case study of linear arithmetic.Machine Intelligence, Hayes J E, Michie D, Richards J (eds.),New York, NY, USA: Oxford University Press, Inc., 1988,pp.83124. [47] Boyer R S, Moore J S. A theorem prover for a computationallogic. In Proc. the 10th CADE, July 1990, pp.115. [48] Johnson D S. Approximation algorithms for combinatorialproblems. Journal of Computer and System Sciences, 1974,9(3): 256278. [49] Kautz H A, Selman B. Planning as satisfiability. In Proc. the10th ECAI, Aug. 1992, pp.359363. [50] Rintanen J, Heljanko K, Niemelä I. Planning as satisfiability: Parallel plans and algorithms for plan search. ArtificialIntelligence, 2006, 170(12/13): 10311080. [51] Vasquez M, Hao J K. A "logicconstrained" knapsack formulation and a tabu algorithm for the daily photograph schedulingof an earth observation satellite. Computational Optimizationand Applications, 2001, 20(2): 137157. [52] Strickland D M, Barnes E R, Sokol J S. Optimal protein structure alignment using maximum cliques. Operations Research,2005, 53(3): 389402. [53] Miyazaki S, Iwama K, Kambayashi Y. Database queries ascombinatorial optimization problems. In Proc. CODAS 1996,Dec. 1996, pp.477483. [54] Sandholm T. Algorithm for optimal winner determinationin combinatorial auctions. Artificial Intelligence, 2002,135(1/2): 154. [55] Nguyen T A, Perkins W A, Laffey T J, Pecora D. Checkingan expert systems knowledge base for consistency and completeness. In Proc. the 9th IJCAI, Aug. 1985, pp.375378. [56] Li X Y, Stallmann M F, Berglez F. Optimization algorithmsfor the minimumcost satisfiability problem [PhD Thesis].North Carolina State University, 2004. [57] Argelich J, Li C M, Manyà F, Planes J. First evaluation ofMaxSAT solvers. http://www.iiia.csic.es/conferences/maxsat06/, 2006. [58] Li C M, Manyà F. MaxSAT, hard and soft constraints. InHandbook of Satisfiability, Biere A, Heule M, van Maaren H,Walsh T (eds.), IOS Press, 2009, pp.613631. [59] Cha B, Iwama K, Kambayashi Y, Miyazaki S. Local searchalgorithms for partial MaxSAT. In Proc. the 14th AAAI and9th IAAI, July 1997, pp.263268. [60] Kautz H, Selman B, Jiang Y. A general stochastic approachto solving problems with hard and soft constraints. In TheSatisfiability Problem: Theory and Applications, Gu D, DuJ, Pardalos P (eds.), American Mathematical Society, 1997,Vol.35, pp.573586. [61] Menai M E B. Solution reuse in Partial MaxSAT problem.In Proc. the 2004 IEEEIRI, Nov. 2004, pp.481486. [62] Menai M E B. A twophase backbonebased search heuristicfor Partial MaxSAT: An initial investigation. In Proc. the18th IEA/AIE, June 2005, pp.681684. [63] Menai M E B, Batouche M. A backbonebased coevolutionary heuristic for Partial MaxSAT. In Proc. the 7thEA, Oct. 2005, pp.155166. [64] Mouhoub M. Systematic versus local search and GA techniques for incremental SAT. International Journal of Computational Intelligence and Applications, 2008, 7(1): 7796. [65] Argelich J, Li C M, Manyà F, Planes J. The first and second MaxSAT evaluations. Journal on Satisfiability, BooleanModeling and Computation, 2008, 4(2/4): 251278. [66] Argelich J, Li C M, Manyà F, Planes J. Third evaluationof MaxSAT solvers. http://maxsat.ia.udl.cat:81/08/, Feb.2013. [67] Argelich J, Li C M, Manyà F, Planes J. Fourth evaluationof MaxSAT solvers. http://maxsat.ia.udl.cat:81/09/, Feb.2013. [68] Argelich J, Li C M, Manyà F, Planes J. Fifth evaluationof MaxSAT solvers. http://maxsat.ia.udl.cat:81/10/, Feb.2013. [69] Argelich J, Li C M, Manyà F, Planes J. Sixth evaluationof MaxSAT solvers. http://maxsat.ia.udl.cat:81/11/, Feb.2013. [70] Robinson J A. A machineoriented logic based on the resolution principle. Journal of the ACM, 1965, 12(1): 2341. [71] Davis M, Putnam H. A computing procedure for quantification theory. Journal of the ACM, 1960, 7(3): 201215. [72] Davis M, Logemann G, Loveland D. A machine program fortheoremproving. Communications of the ACM, 1962, 5(7):394397. [73] Urquhart A. Hard examples for resolution. Journal of theACM, 1987, 34(1): 209219. [74] Chatalic P, Simon L. ZRES: The old DavisPutman proceduremeets ZBDD. In Proc. the 17th CADE, June 2000, pp.449454. [75] Land A H, Doig A G. An automatic method for solving discrete programming problems. Econometrica, 1960, 28(3):497520. [76] Kuegel A. Improved exact solver for the weighted MaxSATproblem. In Pragmatics of SAT Workshop of the SAT Conference, July 2010. [77] Pipatsrisawat K, Darwiche A. Clone: Solving weighted MaxSAT in a reduced search space. In Proc. the 20th AUSAI2007, Dec. 2007, pp.223233. [78] Pipatsrisawat K, Palyan A, Chavira M, Choi A, DarwicheA. Solving weighted MaxSAT problems in a reduced searchspace: A performance analysis. Journal on Satisfiability,Boolean Modeling and Computation, 2008, 4(2/4): 191217. [79] Lin H, Su K. Exploiting inference rules to compute lowerbounds for MaxSAT solving. In Proc. the 20th IJCAI, Jan.2007, pp.23342339. [80] Lin H, Su K, Li C M. Withinproblem learning for efficientlower bound computation in MaxSAT solving. In Proc. the23rd AAAI, July 2008, pp.351356. [81] Heras F, Larrosa J, Oliveras A. MiniMaxSAT: A new weightedMaxSAT solver. In Proc. the 10th SAT, May 2007, pp.4155. [82] Heras F, Larrosa J, Oliveras A. MiniMaxSAT: An efficientweighted MaxSAT solver. Journal of Artificial IntelligenceResearch, 2008, 31: 132. [83] Argelich J, Manyà F. Partial MaxSAT solvers with clauselearning. In Proc. the 10th SAT, May 2007, pp.2840. [84] Ram?3rez M, Geffner H. Structural relaxations by variable renaming and their compilation for solving MinCostSAT. InProc. the 13th CP, Sept. 2007, pp.605619. [85] de Givry S, Heras F, Zytnicki M, Larrosa J. Existential arcconsistency: Getting closer to full arc consistency in weightedCSPs. In Proc. the 19th IJCAI, July 30Aug. 5, 2005, pp.8489. [86] Heras F, Larrosa J. New inference rules for efficient MaxSATsolving. In Proc. the 21st AAAI, July 2006, pp.6873. [87] Larrosa J, Heras F, de Givry S. A logical approach to efficientMaxSAT solving. Artificial Intelligence, 2008, 172(2/3):204233. [88] Li C M, Manyà F, Mohamedou N, Planes J. Exploiting cyclestructures in MaxSAT. In Proc. the 12th SAT, June 30July3, 2009, pp.467480. [89] Darras S, Dequen G, Devendeville L, Li C M. On inconsistentclausesubsets for MaxSAT solving. In Proc. the 13th CP,Sept. 2007, pp.225240. [90] Li C M, Manyà F, Planes J. Exploiting unit propagation tocompute lower bounds in branch and bound MaxSAT solvers.In Proc. the 11th CP, Oct. 2005, pp.403414. [91] Li C M, Manyà M, Planes J. Detecting disjoint inconsistentsubformulas for computing lower bounds for MaxSAT. InProc. the 21st AAAI, July 2006, pp.8691. [92] Darwiche A, Marquis P. A knowledge compilation map. Artificial Intelligence Research, 2002, 17: 229264. [93] Darwiche A. New advances in compiling CNF into decomposable negational normal form. In Proc. the 16th ECAI, Aug.2004, pp.328332. [94] Larrosa J, Heras F. Resolution in MaxSAT and its relation tolocal consistency in weighted CSPs. In Proc. the 19th IJCAI,July 30Aug. 5, 2005, pp.193198. [95] de Givry S, Larrosa J, Meseguer P, Schiex T. Solving MaxSAT as weighted CSP. In Proc. the 9th CP, Sept. 29Oct. 3,2003, pp.363376. [96] Fu Z, Malik S. On solving the Partial MaxSAT problem. InProc. the 9th SAT, Aug. 2006, pp.252265. [97] MarquesSilva J, Planes J. On using unsatisfiability for solving maximum satisfiability. Computing Research Repository,arXiv: 0712.1097, 2007. [98] MarquesSilva J, Manquinho V. Towards more effectiveunsatisfiabilitybased maximum satisfiability algorithms. InProc. the 11th SAT, May 2008, pp.225230. [99] MarquesSilva J, Planes J. Algorithms for maximumsatisfiability using unsatisfiable cores. In Proc. DATE, Mar.2008, pp.408413. [100] Manquinho V, MarquesSilva J, Planes J. Algorithms forweighted Boolean optimization. In Proc. the 12th SAT, June30July 3, 2009, pp.495508. [101] Ansótegui C, Bonet M L, Levy J. Solving (weighted) partialMaxSAT through satisfiability testing. In Proc. the 12thSAT, June 30July 3, 2009, pp.427440. [102] Le Berre D, Parrain A. The Sat4j library (release 2.2). Journal on Satisfiability, Boolean Modeling and Computation,2010, 7(2/3): 5964. [103] Barth P. A DavisPutnam based enumeration algorithm forlinear pseudoBoolean optimization. Technical Report MPII952003, MaxPlanckInstitut fÄur Informatik, Im Stadtwald,D66123 SaarbrÄucken, Germany, Jan. 1995. [104] Xu L, Hutter F, Hoos H H, LeytonBrown K. SATzilla:Portfoliobased algorithm selection for SAT. Journal of Artificial Intelligence Research, 2008, 32: 565606. [105] Mouhoub M, Sadaoui S. Solving incremental satisfiability.International Journal on Artificial Intelligence Tools, 2007,16(1): 139147. 
No related articles found! 

