Abstract
Searching for optimal solutions to a problem using lower bounds obtained from a relaxation is a common idea in Heuristic Search and Planning. In SAT and CSPs, however, explicit relaxations are seldom used. In this work, we consider the use of explicit relaxations for solving MinCostSAT, the problem of finding a minimum cost satisfying assignment. We start with the observation that while a number of SAT and CSP tasks have a complexity that is exponential in the treewidth, such models can be relaxed into weaker models of bounded treewidth by a simple form of variable renaming. The relaxed models can then be compiled in polynomial time and space, so that their solutions can be used effectively for pruning the search in the original problem. We have implemented a MinCostSAT solver using this idea on top of two off-the-shelf tools, a d-DNNF compiler that deals with the relaxation, and a SAT solver that deals with the search. The results over the entire suite of 559 problems from the 2006 Weighted Max-SAT Competition are encouraging: SR( w ), the new solver, solves 56% of the problems when the bound on the relaxation treewidth is set to w = 8, while Toolbar, the winner, solves 73% of the problems, Lazy, the runner up, 55%, and MinCostChaff, a recent MinCostSAT solver, 26%. The relation between the proposed relaxation method and existing structural solution methods such as cutset decomposition and derivatives such as mini-buckets is also discussed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Culberson, J.C., Schaeffer, J.: Pattern Databases. Comp. Int. 14 (1998)
Korf, R.E.: Finding Optimal Solutions to Rubik’s Cube Using Pattern Patabases. In: Proc. AAAI 1998 (1998)
Bonet, B., Geffner, H.: Planning as Heuristic Search. Art. Int. 129 (2001)
Mackworth, A.K.: Consistency in Networks of Relations. Art. Int. 8 (1977)
Li, X.Y.: Optimization Algorithms for the Minimum–Cost Satisfiability Problem. PhD thesis, North Carolina State University (2004)
Dechter, R.: Constraint Processing. Morgan Kauffman, San Francisco (2003)
Darwiche, A.: New Advances in Compiling CNF to Decomposable Negational Normal Form. In: Proc. ECAI 2004 (2004)
Eén, N., Söressón, N.: MiniSAT: an Extensible SAT Solver. Technical report, Chalmers University (2005)
Darwiche, A.: Decomposable Negation Normal Form. Journal of the ACM 48(4), 608–647 (2001)
Marquis, P., Darwiche, A.: Compiling Propositional Weighted Bases. Artificial Intelligence 157(1–2), 81–113 (2004)
Argelich, J., et al.: First Evaluation of Max-SAT solvers (2006), Available at http://www.iiia.csic.es/maxsat06
Fu, Z., Malik, S.: Solving the Minimum Cost Satisfiability Problem using SAT Based Branch-and-Bound Search. In: Proc. of ICCAD 2006 (2006)
Bistarelli, S., Montanari, U., Rossi, F., Schiex, T., Verfaille, G., Fargier, H.: Semiring-Based CSPs and Valued CSPs: Frameworks, Properties and Comparison. Constraints 4(3), 199–240 (2004)
Papadimitrou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)
Giunchiglia, E., Maratea, M.: Solving Optimization Problems with DLL. In: Proc. of ECAI 2006 (2006)
Larrosa, J., Heras, F.: Resolution in Max-SAT and its Relation to Local Consistency in Weighted CSPs. In: Proc. of IJCAI 2005, pp. 193–199 (2005)
Larrosa, J., Heras, F.: New Inference Rules for Efficient Max-SAT Solving. In: Proc. AAAI 2006 (2006)
Li, C.M., Manyá, F., Planes, J.: Detecting Disjoint Inconsistent Subformulas for Computing Lower Bounds for Max-SAT. In: Proc. AAAI 2006 (2006)
de Givry, S., Larrosa, J., Messeguer, P., Schiex, T.: Solving Max-SAT as Weighted CSP. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 363–376. Springer, Heidelberg (2003)
Dechter, R.: Enhancement Schemes for Constraint Processing: Backjumping, Learning and Cutset Decomposition. Artificial Intelligence 43(3), 273–312 (1990)
Gottlob, G., Leone, N., Scarcello, F.: Hypertree decompositions and tractable queries. J. Comput. Syst. Sci. 64(3), 579–627 (2002)
Bidyuk, B., Dechter, R.: On Finding Minimal w-cutset. In: Proc. UAI 2004 (2004)
Dechter, R.: Mini–Buckets: a General Scheme for Generating Approximations in Automated Reasoning. In: Proc. of IJCAI 1997, pp. 1297–1303 (1997)
Dechter, R.: Bucket Elimination: a Unifying Framework for Reasoning. Artificial Intelligence 113(1–2), 41–85 (1999)
Darwiche, A., Marquis, P.: A Knowledge Compilation Map. Journal of AI Research 17, 229–264 (2002)
Darwiche, A.: Recursive Conditioning. Artificial Intelligence 126(1–2), 5–41 (2001)
Coudert, O., Madre, J.C.: New Ideas for Solving Covering Problems. In: Proc. of DAC 1995, pp. 641–646 (1995)
Moskewicz, M.W., Madigan, C.F., et al.: Chaff: Engineeering an Efficient SAT Solver. In: Proc.of DAC 2001 (2001)
Zhang, L., Madigan, C.F., et al.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: Proc. of ICCAD 2001 (2001)
Silva, J.P.M., Sakallah, K.A.: GRASP – A New Search Algorithm for Satisfiability. In: Proc. of ICCAD 1996, pp. 220–227 (1996)
Manquinho, V., Marques-Silva, J.: Search Pruning Techniques in SAT-based Branch-and-Bound Algorithms for the Binate Covering Problem. IEEE Trans. on CAD and Integrated Circuit and Systems 21, 505–516 (2002)
Alsinet, T., Manyá, F., Planes, J.: Improved Exact Solvers for Weighted Max-SAT. In: Proc. of the 8th SAT conference (2005)
Choi, A., Chavira, M., Darwiche, A.: Node splitting: A scheme for generating upper bounds in bayesian networks. In: Proceedings UAI 2007 (to appear 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ramírez, M., Geffner, H. (2007). Structural Relaxations by Variable Renaming and Their Compilation for Solving MinCostSAT. In: Bessière, C. (eds) Principles and Practice of Constraint Programming – CP 2007. CP 2007. Lecture Notes in Computer Science, vol 4741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74970-7_43
Download citation
DOI: https://doi.org/10.1007/978-3-540-74970-7_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74969-1
Online ISBN: 978-3-540-74970-7
eBook Packages: Computer ScienceComputer Science (R0)