部分合取范式最大可满足问题的一类精确解方法

doi:10.1007/s11390-013-1325-5

摘要/Abstract

部分合取范式最大可满足问题 (Partial Max-SAT 或 PMSAT) 是布尔可满足问题(SAT)的一种优化变种, 在PMSAT的一个布尔表达式中, 要求变量的真值指派必须满足所有的硬子句和最大数量的软子句。尽管在解决实际问题的过程中会违反一些约束条件, 但是PMSAT的解决方案还是可以接受的, 所以PMSAT被认为是解决许多现实生活问题的一种有趣的编码领域。在这些问题中, 有些可以表示为规划和调度问题。从2006年开始的Max-SAT测评以来, 已经出现了很多关于PMSAT问题的新研究。实际上, 一些PMSAT问题的精确解主要都是基于Davis-Putnam-Logemann-Loveland (DPLL)过程和分支定界(B&B)算法发展起来的。在本论文中, 我们研究和分析了一些PMSAT的精确解方法。将不同的技术集成在统一的视角中从而形成了一个通用的框架。在这个框架中, 针对主要的精确解算法, 我们提出了一类精确解方法。通过使用这类精确解方法和重点研究最前沿的研究方向, 我们对参加2007-2011年Max-SAT测评的精确解进行了分类, 从而说明了它的高效性。

Abstract: 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.

Mohamed El Bachir Menai and Tasniem Nasser Al-Yahya. 部分合取范式最大可满足问题的一类精确解方法[J]. , 2013, 28(2): 232-246.

Mohamed El Bachir Menai and Tasniem Nasser Al-Yahya. A Taxonomy of Exact Methods for Partial Max-SAT[J]. , 2013, 28(2): 232-246.

参考文献

[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.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed