| [1] Cook S A. The complexity of theorem-proving procedures. InProc. the 3rd STOC, May 1971, pp.151-158.[2] Kautz H, Selman B. Pushing the envelope: Planning, proposi-tional logic, and stochastic search. In Proc. the 13th NationalConf. Artificial Intelligence, Aug. 1996, pp.1194-1201.[3] Gomes C P, Selman B, McAloon K, Tretkoff C. Randomiza-tion in backtrack search: Exploiting heavy-tailed profiles forsolving hard scheduling problems. In Proc. the 4th AIPS,June 1998, pp.208-213.[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.317-320.[5] Abdulla P A, Bjesse P, Eén N. Symbolic reachability analy-sis based on SAT solvers. In Proc. the 6th TACAS, March25-April 2, 2000, pp.411-425.[6] Bjesse P, Leonard T, Mokkedem A. Finding bugs in an Alphamicroprocessor using satisfiability solvers. In Proc. the 13thCAV, July 2001, pp.454-464.[7] Jackson D, Schechter I, Shlyakhter I. Alcoa: The alloy con-straint analyzer. In Proc. the 22nd ICSE, June 2000, pp.730-733.[8] Clarke E M, Kroening D, Lerda F. A tool for checking ANSI-C programs. In Proc. the 10th TACAS, Mar. 29-Apr. 2 2004,pp.168-176.[9] Khurshid S, Marinov D. Testera: Specification-based testingof Java programs using SAT. Automated Software Engineer-ing, 2004, 11(4): 403-434.[10] Buro M, BÄuning H K. Report on a SAT competition. Bul-letin of the European Association for Theoretical ComputerScience, 1992, 49: 143-151.[11] Simon L, Le Berre D, Hirsch E A. The SAT2002 competi-tion. Annals of Mathematics and Artificial Intelligence, 2005,43(1): 307-342.[12] Purdom P W, Le Berre D, Simon L. A parsimony tree for theSAT2002 competition. Annals of Mathematics and ArtificialIntelligence, 2005, 43(1): 343-365.[13] Marques-Silva J P, Sakallah K A. GRASP-A new search al-gorithm for satisfiability. In Proc. ICCAD 1996, Nov. 1996,pp.220-227.[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.530-535.[15] Goldberg E, Novikov Y. Berkmin: A fast and robust SAT-solver. In Proc. DATE 2002, Mar. 2002, pp.142-149.[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°ict-clause minimization. In Proc. SAT 2005, June 2005, pp.502-518.[18] Gu J. Efficient local search for very large-scale satisfiabilityproblems. SIGART Bulletin, 1992, 3(1): 8-12.[19] Gent I P, Walsh T. Towards an understanding of hill-climbingprocedures for SAT. In Proc. the 11th AAAI, July 1993,pp.28-33.[20] Ginsberg M L, McAllester D A. GSAT and dynamic back-tracking. In Proc. the 2nd PPCP 1994, May 1994, pp.243-265.[21] Konolige K. Easy to be hard: Difficult problems for greedyalgorithms. In Proc. the 4th KR, May 1994, pp.374-378.[22] Cha B, Iwama K. Adding new clauses for faster local search.In Proc. the 13th AAAI, Aug. 1996, Vol.1, pp.332-337.[23] Frank J, Cheeseman P, Stutz J. When gravity fails: Localsearch topology. Journal of Artificial Intelligence Research,1997, 7: 249-281.[24] Gu J, Purdom P W, Franco J, Wah B W. Algorithms for thesatisfiability (SAT) problem: A survey. In Satisfiability Prob-lem: Theory and Applications, Du D, Gu J, Pardalos R M(eds.), 1997, Vol.35, pp.19-152.[25] Hoos H H. On the run-time behaviour of stochastic localsearch algorithms for SAT. In Proc. the 16th National Conf.Artificial Intelligence and 11th Innovation Applications ofArtificial Intelligence, July 1999, pp.661-666.[26] Hoos H H. An adaptive noise mechanism for walkSAT. InProc. the 18th AAAI, July 28-Aug. 1, 2002, pp.655-660.[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.53-68.[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): 91-111.[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): 319-331.[31] Rish I, Dechter R. To guess or to think? Hybrid algorithmsfor SAT. In Proc. the 2nd CP 1996, Aug. 1996, pp.555-556.[32] Habet D, Li C M, Devendeville L, Vasquez M. A hybrid ap-proach for SAT. In Proc. the 8th CP, Sept. 2002, pp.172-184.[33] Anbulagan A, Pham D N, Slaney J, Sattar A. Old resolu-tion meets modern SLS. In Proc. the 20th AAAI, July 2005,pp.354-359.[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.1-17.[35] Dixon H E, Ginsberg M L, Parkes A J. Generalizing Booleansatisfiability I: Background and survey of existing work. Ar-tificial Intelligence Research, 2004, 21: 193-243.[36] Kautz H, Selman B. The state of SAT. Discrete Applied Math-ematics, 2007, 155(12): 1514-1524.[37] Marques-Silva J. Practical applications of Boolean satisfiabi-lity. In Proc. the 9th WODES, May 2008, pp.74-80.[38] Gomes C P, Kautz H, Sabharwal A, Selman B. Satisfiabilitysolvers. In Foundations of Artificial Intelligence, van Harme-len F, Lifschit Z, Porter B (eds.), 2008, Vol.3, pp.89-134.[39] Biere A, Heule M J, van Maaren H, Walsh T (eds.). Hand-book of Satisfiability. Frontiers in Artificial Intelligence andApplications, Vol.185, IOS Press, 2009.[40] Xu K, Boussemart F, Hemery F, Lecoutre C. Random con-straint satisfaction: Easy generation of hard (satisfiable) in-stances. Artificial Intelligence, 2007, 171(8/9): 514-534.[41] Shostak R E. An algorithm for reasoning about equality.Communications of the ACM, 1978, 21(7): 583-585.[42] Shostak R E. A practical decision procedure for arithmeticwith function symbols. Journal of the ACM, 1979, 26(2):351-360.[43] Nelson G, Oppen D C. Simplification by cooperating decisionprocedures. ACM Transactions on Programming Languagesand Systems, 1979, 1(2): 245-257.[44] Nelson G, Oppen D C. Fast decision procedures based on con-gruence closure. Journal of the ACM, 1980, 27(2): 356-364.[45] Shostak R E. Deciding combinations of theories. Journal ofthe ACM, 1984, 31(1): 1-12.[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.83-124.[47] Boyer R S, Moore J S. A theorem prover for a computationallogic. In Proc. the 10th CADE, July 1990, pp.1-15.[48] Johnson D S. Approximation algorithms for combinatorialproblems. Journal of Computer and System Sciences, 1974,9(3): 256-278.[49] Kautz H A, Selman B. Planning as satisfiability. In Proc. the10th ECAI, Aug. 1992, pp.359-363.[50] Rintanen J, Heljanko K, Niemelä I. Planning as satisfiabi-lity: Parallel plans and algorithms for plan search. ArtificialIntelligence, 2006, 170(12/13): 1031-1080.[51] Vasquez M, Hao J K. A "logic-constrained" knapsack formula-tion and a tabu algorithm for the daily photograph schedulingof an earth observation satellite. Computational Optimizationand Applications, 2001, 20(2): 137-157.[52] Strickland D M, Barnes E R, Sokol J S. Optimal protein struc-ture alignment using maximum cliques. Operations Research,2005, 53(3): 389-402.[53] Miyazaki S, Iwama K, Kambayashi Y. Database queries ascombinatorial optimization problems. In Proc. CODAS 1996,Dec. 1996, pp.477-483.[54] Sandholm T. Algorithm for optimal winner determinationin combinatorial auctions. Artificial Intelligence, 2002,135(1/2): 1-54.[55] Nguyen T A, Perkins W A, Laffey T J, Pecora D. Checkingan expert systems knowledge base for consistency and com-pleteness. In Proc. the 9th IJCAI, Aug. 1985, pp.375-378.[56] Li X Y, Stallmann M F, Berglez F. Optimization algorithmsfor the minimum-cost satisfiability problem [PhD Thesis].North Carolina State University, 2004.[57] Argelich J, Li C M, Manyà F, Planes J. First evaluation ofMax-SAT solvers. http://www.iiia.csic.es/conferences/max-sat06/, 2006.[58] Li C M, Manyà F. Max-SAT, hard and soft constraints. InHandbook of Satisfiability, Biere A, Heule M, van Maaren H,Walsh T (eds.), IOS Press, 2009, pp.613-631.[59] Cha B, Iwama K, Kambayashi Y, Miyazaki S. Local searchalgorithms for partial MaxSAT. In Proc. the 14th AAAI and9th IAAI, July 1997, pp.263-268.[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.573-586.[61] Menai M E B. Solution reuse in Partial Max-SAT problem.In Proc. the 2004 IEEE-IRI, Nov. 2004, pp.481-486.[62] Menai M E B. A two-phase backbone-based search heuristicfor Partial Max-SAT: An initial investigation. In Proc. the18th IEA/AIE, June 2005, pp.681-684.[63] Menai M E B, Batouche M. A backbone-based co-evolutionary heuristic for Partial Max-SAT. In Proc. the 7thEA, Oct. 2005, pp.155-166.[64] Mouhoub M. Systematic versus local search and GA tech-niques for incremental SAT. International Journal of Com-putational Intelligence and Applications, 2008, 7(1): 77-96.[65] Argelich J, Li C M, Manyà F, Planes J. The first and sec-ond Max-SAT evaluations. Journal on Satisfiability, BooleanModeling and Computation, 2008, 4(2/4): 251-278.[66] Argelich J, Li C M, Manyà F, Planes J. Third evaluationof Max-SAT solvers. http://maxsat.ia.udl.cat:81/08/, Feb.2013.[67] Argelich J, Li C M, Manyà F, Planes J. Fourth evaluationof Max-SAT solvers. http://maxsat.ia.udl.cat:81/09/, Feb.2013.[68] Argelich J, Li C M, Manyà F, Planes J. Fifth evaluationof Max-SAT solvers. http://maxsat.ia.udl.cat:81/10/, Feb.2013.[69] Argelich J, Li C M, Manyà F, Planes J. Sixth evaluationof Max-SAT solvers. http://maxsat.ia.udl.cat:81/11/, Feb.2013.[70] Robinson J A. A machine-oriented logic based on the resolu-tion principle. Journal of the ACM, 1965, 12(1): 23-41.[71] Davis M, Putnam H. A computing procedure for quantifica-tion theory. Journal of the ACM, 1960, 7(3): 201-215.[72] Davis M, Logemann G, Loveland D. A machine program fortheorem-proving. Communications of the ACM, 1962, 5(7):394-397.[73] Urquhart A. Hard examples for resolution. Journal of theACM, 1987, 34(1): 209-219.[74] Chatalic P, Simon L. ZRES: The old Davis-Putman proceduremeets ZBDD. In Proc. the 17th CADE, June 2000, pp.449-454.[75] Land A H, Doig A G. An automatic method for solving dis-crete programming problems. Econometrica, 1960, 28(3):497-520.[76] Kuegel A. Improved exact solver for the weighted Max-SATproblem. In Pragmatics of SAT Workshop of the SAT Con-ference, July 2010.[77] Pipatsrisawat K, Darwiche A. Clone: Solving weighted Max-SAT in a reduced search space. In Proc. the 20th AUS-AI2007, Dec. 2007, pp.223-233.[78] Pipatsrisawat K, Palyan A, Chavira M, Choi A, DarwicheA. Solving weighted Max-SAT problems in a reduced searchspace: A performance analysis. Journal on Satisfiability,Boolean Modeling and Computation, 2008, 4(2/4): 191-217.[79] Lin H, Su K. Exploiting inference rules to compute lowerbounds for Max-SAT solving. In Proc. the 20th IJCAI, Jan.2007, pp.2334-2339.[80] Lin H, Su K, Li C M. Within-problem learning for efficientlower bound computation in Max-SAT solving. In Proc. the23rd AAAI, July 2008, pp.351-356.[81] Heras F, Larrosa J, Oliveras A. MiniMaxSAT: A new weightedMax-SAT solver. In Proc. the 10th SAT, May 2007, pp.41-55.[82] Heras F, Larrosa J, Oliveras A. MiniMaxSAT: An efficientweighted Max-SAT solver. Journal of Artificial IntelligenceResearch, 2008, 31: 1-32.[83] Argelich J, Manyà F. Partial Max-SAT solvers with clauselearning. In Proc. the 10th SAT, May 2007, pp.28-40.[84] Ram?3rez M, Geffner H. Structural relaxations by variable re-naming and their compilation for solving MinCostSAT. InProc. the 13th CP, Sept. 2007, pp.605-619.[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 30-Aug. 5, 2005, pp.84-89.[86] Heras F, Larrosa J. New inference rules for efficient Max-SATsolving. In Proc. the 21st AAAI, July 2006, pp.68-73.[87] Larrosa J, Heras F, de Givry S. A logical approach to efficientMax-SAT solving. Artificial Intelligence, 2008, 172(2/3):204-233.[88] Li C M, Manyà F, Mohamedou N, Planes J. Exploiting cyclestructures in Max-SAT. In Proc. the 12th SAT, June 30-July3, 2009, pp.467-480.[89] Darras S, Dequen G, Devendeville L, Li C M. On inconsistentclause-subsets for Max-SAT solving. In Proc. the 13th CP,Sept. 2007, pp.225-240.[90] Li C M, Manyà F, Planes J. Exploiting unit propagation tocompute lower bounds in branch and bound Max-SAT solvers.In Proc. the 11th CP, Oct. 2005, pp.403-414.[91] Li C M, Manyà M, Planes J. Detecting disjoint inconsistentsubformulas for computing lower bounds for Max-SAT. InProc. the 21st AAAI, July 2006, pp.86-91.[92] Darwiche A, Marquis P. A knowledge compilation map. Ar-tificial Intelligence Research, 2002, 17: 229-264.[93] Darwiche A. New advances in compiling CNF into decompos-able negational normal form. In Proc. the 16th ECAI, Aug.2004, pp.328-332.[94] Larrosa J, Heras F. Resolution in Max-SAT and its relation tolocal consistency in weighted CSPs. In Proc. the 19th IJCAI,July 30-Aug. 5, 2005, pp.193-198.[95] de Givry S, Larrosa J, Meseguer P, Schiex T. Solving Max-SAT as weighted CSP. In Proc. the 9th CP, Sept. 29-Oct. 3,2003, pp.363-376.[96] Fu Z, Malik S. On solving the Partial Max-SAT problem. InProc. the 9th SAT, Aug. 2006, pp.252-265.[97] Marques-Silva J, Planes J. On using unsatisfiability for solv-ing maximum satisfiability. Computing Research Repository,arXiv: 0712.1097, 2007.[98] Marques-Silva J, Manquinho V. Towards more effectiveunsatisfiability-based maximum satisfiability algorithms. InProc. the 11th SAT, May 2008, pp.225-230.[99] Marques-Silva J, Planes J. Algorithms for maximumsatisfiability using unsatisfiable cores. In Proc. DATE, Mar.2008, pp.408-413.[100] Manquinho V, Marques-Silva J, Planes J. Algorithms forweighted Boolean optimization. In Proc. the 12th SAT, June30-July 3, 2009, pp.495-508.[101] Ansótegui C, Bonet M L, Levy J. Solving (weighted) partialMax-SAT through satisfiability testing. In Proc. the 12thSAT, June 30-July 3, 2009, pp.427-440.[102] Le Berre D, Parrain A. The Sat4j library (release 2.2). Jour-nal on Satisfiability, Boolean Modeling and Computation,2010, 7(2/3): 59-64.[103] Barth P. A Davis-Putnam based enumeration algorithm forlinear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max-Planck-Institut fÄur Informatik, Im Stadtwald,D-66123 SaarbrÄucken, Germany, Jan. 1995.[104] Xu L, Hutter F, Hoos H H, Leyton-Brown K. SATzilla:Portfolio-based algorithm selection for SAT. Journal of Ar-tificial Intelligence Research, 2008, 32: 565-606.[105] Mouhoub M, Sadaoui S. Solving incremental satisfiability.International Journal on Artificial Intelligence Tools, 2007,16(1): 139-147. |