Abstract
Current implementations of pseudo-Boolean (PB) solvers working on native PB constraints are based on the CDCL architecture which empowers highly efficient modern SAT solvers. In particular, such PB solvers not only implement a (cutting-planes-based) conflict analysis procedure, but also complementary strategies for components that are crucial for the efficiency of CDCL, namely branching heuristics, learned constraint deletion and restarts. However, these strategies are mostly reused by PB solvers without considering the particular form of the PB constraints they deal with. In this paper, we present and evaluate different ways of adapting CDCL strategies to take the specificities of PB constraints into account while preserving the behavior they have in the clausal setting. We implemented these strategies in two different solvers, namely Sat4j (for which we consider three configurations) and RoundingSat. Our experiments show that these dedicated strategies allow to improve, sometimes significantly, the performance of these solvers, both on decision and optimization problems.
R. Wallon—Most of this paper is based on research conducted by this author while he was working as a PhD student at CRIL (Univ Artois & CNRS).
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
Similar content being viewed by others
References
Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. JAIR 40, 353–373 (2011)
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of IJCAI 2009, pp. 399–404 (2009)
Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Milano, M. (ed.) Proceedings of CP 2012, pp. 118–126 (2012)
Biedenkapp, A., Bozkurt, H.F., Eimer, T., Hutter, F., Lindauer, M.: Dynamic algorithm configuration: foundation of a new meta-algorithmic framework. In: Proceedings of ECAI 2020 (2020)
Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Proceedings of SAT 2008, pp. 28–33 (2008)
Biere, A.: PicoSAT essentials. JSAT 4(2–4), 75–97 (2008)
Biere, A., Fröhlich, A.: Evaluating CDCL variable scoring schemes. In: Proceedings of SAT 2015, pp. 405–422 (2015)
Biere, A., Fröhlich, A.: Evaluating CDCL Restart Schemes. In: Proceedings of Pragmatics of SAT 2015 and 2018. EPiC Series in Computing, vol. 59, pp. 1–17 (2019)
Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver. IEEE Trans. CAD Integrated Circuits Syst., 305–317 (2005)
Cook, W., Coullard, C.R., Turán, G.: On the complexity of cutting-plane proofs. Discrete Appl. Math., 25–38 (1987)
Dixon, H.: Automating pseudo-boolean inference within a DPLL framework. Ph.D. thesis, University of Oregon (2004)
Dixon, H.E., Ginsberg, M.L.: Inference methods for a pseudo-boolean satisfiability solver. In: Proceedings of AAAI 2002, pp. 635–640 (2002)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Proceedings of SAT 2004, pp. 502–518 (2004)
Elffers, J., Giráldez-Crú, J., Nordström, J., Vinyals, M.: Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers. In: Proceedings of SAT 2018, pp. 75–93 (2018)
Elffers, J., Giráldez-Cru, J., Gocht, S., Nordström, J., Simon, L.: Seeking practical CDCL insights from theoretical SAT benchmarks. In: Proceedings of IJCAI 2018, pp. 1300–1308 (2018)
Elffers, J., Nordström, J.: Divide and conquer: towards faster pseudo-boolean solving. In: Proceedings of IJCAI 2018, pp. 1291–1299 (2018)
Gocht, S., Nordström, J., Yehudayoff, A.: On Division Versus Saturation in Pseudo-Boolean Solving. In: Proceedings of IJCAI’2019. pp. 1711–1718 (2019)
Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI 1998, pp. 431–437 (1998)
Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bulletin of the American Mathematical Society, pp. 275–278 (1958)
Haken, A.: The intractability of resolution. Theoretical Computer Science, pp. 297–308 (1985)
Hooker, J.N.: Generalized resolution and cutting planes. Annals of Operations Research, pp. 217–239 (1988)
Huang, J.: The Effect of Restarts on the Efficiency of Clause Learning. In: Proceedings of IJCAI 2007, pp. 2318–2323 (2007)
Le Berre, D., Marquis, P., Mengel, S., Wallon, R.: On irrelevant literals in pseudo-boolean constraint learning. In: Proceedings of IJCAI 2020, pp. 1148–1154 (2020)
Le Berre, D., Marquis, P., Wallon, R.: On Weakening strategies for PB solvers. In: Proceedings of SAT 2020, pp. 322–331 (2020)
Le Berre, D., Parrain, A.: The SAT4J library, Release 2.2, System Description. JSAT, pp. 59–64 (2010)
Le Berre, D., Wallon, R.: On Dedicated CDCL Strategies for PB Solvers Companion Artifact, May 2021. https://doi.org/10.5281/zenodo.4751685
Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Proceedings of SAT 2016, pp. 123–140 (2016)
Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. In: Information Processing Letters, pp. 173–180 (1993)
Manquinho, V., Roussel, O.: The First Evaluation of Pseudo-Boolean Solvers (PB’05). JSAT, pp. 103–143 (2006)
Marques-Silva, J., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput., 220–227 (1999)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of DAC 2001, pp. 530–535 (2001)
Nordström, J.: On the interplay between proof complexity and SAT solving. ACM SIGLOG News, pp. 19–44 (2015)
Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011)
Roussel, O.: Pseudo-Boolean Competition 2016 (2016). http://www.cril.fr/PB16/. Accessed 20 May 2020
Roussel, O., Manquinho, V.M.: Pseudo-Boolean and Cardinality Constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 695–733. IOS Press (2009)
Sheini, H.M., Sakallah, K.A.: Pueblo: a hybrid pseudo-boolean SAT solver. JSAT, pp. 165–189 (2006)
Vinyals, M., Elffers, J., Giráldez-Crú, J., Gocht, S., Nordström, J.: In Between resolution and cutting planes: a study of proof systems for pseudo-boolean SAT solving. In: Proceedings of SAT 2018, pp. 292–310 (2018)
Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: a new incremental satisfiability engine. In: Proceedings of DAC 2001, pp. 542–545 (2001)
Acknowledgement
The authors are grateful to the anonymous reviewers for their numerous comments, that greatly helped to improve the paper. Part of this work was supported by the French Ministry for Higher Education and Research and the Hauts-de-France Regional Council through the “Contrat de Plan État Région (CPER) DATA”. This publication was supported by the Chair “Integrated Urban Mobility”, backed by L’X – École Polytechnique and La Fondation de l’École Polytechnique and sponsored by Uber. The Partners of the Chair shall not under any circumstances accept any liability for the content of this publication, for which the author shall be solely liable.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Le Berre, D., Wallon, R. (2021). On Dedicated CDCL Strategies for PB Solvers. In: Li, CM., Manyà, F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science(), vol 12831. Springer, Cham. https://doi.org/10.1007/978-3-030-80223-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-80223-3_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-80222-6
Online ISBN: 978-3-030-80223-3
eBook Packages: Computer ScienceComputer Science (R0)