Abstract
Maximum Satisfiability (MaxSAT) is an optimization variant of the Boolean Satisfiability (SAT) problem. In general, MaxSAT algorithms perform a succession of SAT solver calls to reach an optimum solution making extensive use of cardinality constraints. Many of these algorithms are non-incremental in nature, i.e. at each iteration the formula is rebuilt and no knowledge is reused from one iteration to another. In this paper, we exploit the knowledge acquired across iterations using novel schemes to use cardinality constraints in an incremental fashion. We integrate these schemes with several MaxSAT algorithms. Our experimental results show a significant performance boost for these algorithms as compared to their non-incremental counterparts. These results suggest that incremental cardinality constraints could be beneficial for other constraint solving domains.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abío, I., Stuckey, P.J.: Conflict Directed Lazy Decomposition. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 70–85. Springer, Heidelberg (2012)
Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving WPM2 for (Weighted) Partial MaxSAT. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 117–132. Springer, Heidelberg (2013)
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Kullmann (ed.) [30], pp. 427–440
Ansótegui, C., Bonet, M.L., Levy, J.: A New Algorithm for Weighted Partial MaxSAT. In: Fox, M., Poole, D. (eds.) AAAI Conference on Artificial Intelligence. AAAI Press (2010)
Argelich, J., Berre, D.L., Lynce, I., Marques-Silva, J., Rapicault, P.: Solving Linux Upgradeability Problems Using Boolean Optimization. In: Workshop on Logics for Component Configuration, pp. 11–22 (2010)
Asín, R., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research, 1–21 (2012)
Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality Networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)
Audemard, G., Lagniez, J.M., Simon, L.: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013)
Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean Cardinality Constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108–122. Springer, Heidelberg (2003)
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Tech. rep., Department of Computer Science, The University of Iowa (2010), www.SMT-LIB.org
Büttner, M., Rintanen, J.: Satisfiability Planning with Constraints on the Number of Actions. In: Biundo, S., Myers, K.L., Rajan, K. (eds.) International Conference on Automated Planning and Scheduling, pp. 292–299 (2005)
Chen, Y., Safarpour, S., Marques-Silva, J., Veneris, A.G.: Automated Design Debugging With Maximum Satisfiability. IEEE Transactions on CAD of Integrated Circuits and Systems 29(11), 1804–1817 (2010)
Cheng, K.C.K., Yap, R.H.C.: Maintaining Generalized Arc Consistency on Ad-Hoc n-Ary Boolean Constraints. In: Brewka, G., Coradeschi, S., Perini, A., Traverso, P. (eds.) European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol. 141, pp. 78–82. IOS Press (2006)
Cimatti, A., Sebastiani, R. (eds.): SAT 2012. LNCS, vol. 7317, pp. 2012–2015. Springer, Heidelberg (2012)
Davies, J., Bacchus, F.: Exploiting the Power of mip Solvers in maxsat. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166–181. Springer, Heidelberg (2013)
Davies, J., Bacchus, F.: Postponing Optimization to Speed Up MAXSAT Solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247–262. Springer, Heidelberg (2013)
Debruyne, R.: Arc-Consistency in Dynamic CSPs Is No More Prohibitive. In: International Conference on Tools with Artificial Intelligence, pp. 299–307. IEEE (1996)
Dechter, R., Dechter, A.: Belief Maintenance in Dynamic Constraint Networks. In: Shrobe, H.E., Mitchell, T.M., Smith, R.G. (eds.) AAAI Conference on Artificial Intelligence, pp. 37–42. AAAI Press / The MIT Press (1988)
Dutertre, B., de Moura, L.M.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Eén, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science 89(4), 543–560 (2003)
Fu, Z., Malik, S.: On Solving the Partial MAX-SAT Problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)
Graça, A., Lynce, I., Marques-Silva, J., Oliveira, A.L.: Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information. In: Horimoto, K., Nakatsui, M., Popov, N. (eds.) ANB 2010. LNCS, vol. 6479, pp. 38–56. Springer, Heidelberg (2012)
Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: Burgard, W., Roth, D. (eds.) AAAI Conference on Artificial Intelligence. AAAI Press (2011)
Hooker, J.N.: Solving the incremental satisfiability problem. Journal of Logic Programming 15(1&2), 177–186 (1993)
Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Hall, M.W., Padua, D.A. (eds.) Programming Language Design and Implementation, pp. 437–446. ACM (2011)
Kadioglu, S., Malitsky, Y., Sellmann, M.: Non-Model-Based Search Guidance for Set Partitioning Problems. In: Hoffmann, J., Selman, B. (eds.) AAAI Conference on Artificial Intelligence. AAAI Press (2012)
Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 8, 95–100 (2012)
Kullmann, O. (ed.): SAT 2009. LNCS, vol. 5584. Springer, Heidelberg (2009)
Lagerkvist, M.Z., Schulte, C.: Advisors for Incremental Propagation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 409–422. Springer, Heidelberg (2007)
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7(2-3), 59–66 (2010)
Li, C.M., Manyà, F.: MaxSAT, Hard and Soft Constraints. In: Handbook of Satisfiability, pp. 613–631. IOS Press (2009)
Liffiton, M.H., Sakallah, K.A.: Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Journal Automated Reasoning 40(1), 1–33 (2008)
Lonsing, F., Egly, U.: Incremental QBF Solving. Computing Research Repository - arXiv abs/1402.2410 (2014)
Mahajan, Y.S., Fu, Z., Malik, S.: Zchaff2004: An efficient sat solver. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 360–375. Springer, Heidelberg (2005)
Manolios, P., Papavasileiou, V.: Pseudo-Boolean Solving by incremental translation to SAT. In: Bjesse, P., Slobodová, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, pp. 41–45. FMCAD Inc. (2011)
Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization. In: Kullmann (ed.) [30], pp. 495–508
Marin, P., Miller, C., Lewis, M.D.T., Becker, B.: Verification of partial designs using incremental QBF solving. In: Rosenstiel, W., Thiele, L. (eds.) Design, Automation, and Test in Europe Conference, pp. 623–628. IEEE (2012)
Marques-Silva, J., Planes, J.: On using unsatisfiability for solving Maximum Satisfiability. Tech. rep., Computing Research Repository, abs/0712.0097 (2007)
Martins, R., Manquinho, V., Lynce, I.: Parallel Search for Maximum Satisfiability. AI Communications 25(2), 75–95 (2012)
Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a Modular MaxSAT Solver. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Heidelberg (2014)
Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints 18(4), 478–534 (2013)
Morgado, A., Heras, F., Marques-Silva, J.: Improvements to Core-Guided Binary Search for MaxSAT. In: Cimatti, Sebastiani (eds.) [14], pp. 284–297
Nadel, A., Ryvchin, V.: Efficient SAT Solving under Assumptions. In: Cimatti, Sebastiani (eds.) [14], pp. 242–255
Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005)
Shtrichman, O.: Pruning Techniques for the SAT-Based Bounded Model Checking Problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58–70. Springer, Heidelberg (2001)
van Beek, P.: Backtracking Search Algorithms. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, ch. 4. Elsevier (2006)
van Hoeve, W.J., Katriel, I.: Global constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, ch. 6. Elsevier (2006)
Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: A New Incremental Satisfiability Engine. In: Design Automation Conference, pp. 542–545. ACM (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Martins, R., Joshi, S., Manquinho, V., Lynce, I. (2014). Incremental Cardinality Constraints for MaxSAT. In: O’Sullivan, B. (eds) Principles and Practice of Constraint Programming. CP 2014. Lecture Notes in Computer Science, vol 8656. Springer, Cham. https://doi.org/10.1007/978-3-319-10428-7_39
Download citation
DOI: https://doi.org/10.1007/978-3-319-10428-7_39
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10427-0
Online ISBN: 978-3-319-10428-7
eBook Packages: Computer ScienceComputer Science (R0)