›› 2013, Vol. 28 ›› Issue (2): 232-246.doi: 10.1007/s11390-013-1325-5

• Theoretical Computer Science • Previous Articles     Next Articles

A Taxonomy of Exact Methods for Partial Max-SAT

Mohamed El Bachir Menai and Tasniem Nasser Al-Yahya   

  1. Department of Computer Science, College of Computer and Information Sciences, King Saud University, P.O.Box 51178Riyadh 11543, Saudi Arabia
  • Received:2012-01-10 Revised:2012-08-30 Online:2013-03-05 Published:2013-03-05
  • Supported by:

    This work was supported by the Research Center of College of Computer and Information Sciences at King Saud University, Saudi Arabia.

Partial Maximum Boolean Satisfiability (Partial Max-SAT or PMSAT) is an optimization variant of Boolean satisfiability (SAT) problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many real-life problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland (DPLL) procedure and Branch and Bound (B&B) algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.

[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.
No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] Fei Xianglin; Liao Lei; Wang Hezhen; Wang Chengzao;. Structured Development Environment Based on the Object-Oriented Concepts[J]. , 1992, 7(3): 193 -201 .
[2] Xu Qingyun; Wang Nengbin;. Concurrency Control Mechanism of Complex Objects[J]. , 1992, 7(4): 305 -310 .
[3] Wang Hui; Liu Dayou; Wang Yafei;. Sequential Back-Propagation[J]. , 1994, 9(3): 252 -260 .
[4] Wang Shijun; Wang Shulin;. Research and Design of a Fuzzy Neural Expert System[J]. , 1995, 10(2): 112 -123 .
[5] Ma Guangsheng; Zhang Zhongwei; and Huang Shaobin;. A New Method of Solving Kernels in Algebraic Decomposition for the Synthesis of Logic Cell Array[J]. , 1995, 10(6): 569 -573 .
[6] XIAO Limin; ZHU Mingfa;. Exploiting the Capabilities of the Interconnection Network on Dawning-1000[J]. , 1999, 14(1): 49 -55 .
[7] GAO Suixiang; LIN Guohui;. Decision Tree Complexity of Graph Properties with Dimension at Most5[J]. , 2000, 15(5): 416 -422 .
[8] Imad Jawhar and Jie Wu. QoS Support in TDMA-Based Mobile Ad Hoc Networks[J]. , 2005, 20(6): 797 -810 .
[9] Cliff Reader. AVS Intellectual Property Rights (IPR) Policy[J]. , 2006, 21(3): 306 -309 .
[10] Chiou-Yng Lee, Jenn-Shyong Horng, and I-Chang Jou. Low-Complexity Bit-Parallel Multiplier over GF(2$^m$) Using Dual Basis Representation[J]. , 2006, 21(6): 887 -892 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

Home
Editorial Board
Author Guidelines
Subscription
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved