Abstract
Most modern state-of-the-art Boolean Satisfiability (SAT) solvers are based on the Davis–Putnam–Logemann–Loveland algorithm and exploit techniques like unit propagation and Conflict-Driven Clause Learning (CDCL). Even though this approach proved to be successful in practice, the success of the Monte Carlo Tree Search (MCTS) algorithm in other domains led to research in using it to solve SAT problems. A recent approach extended the attempt to solve SAT using an MCTS-based algorithm by adding CDCL. We further analyzed the behavior of that approach by using visualizations of the produced search trees and based on the analysis introduced multiple heuristics improving different aspects of the quality of the learned clauses. While the resulting solver can be used to solve SAT on its own, the real strength lies in the learned clauses. By using the MCTS solver as a preprocessor, the learned clauses can be used to improve the performance of existing SAT solvers.
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
Notes
References
Browne, C., Powley, E., Whitehouse, D., Lucas, S.M., Cowling, P.I., Rohlfshagen, P., Tavener, S., Perez, D., Samothrakis, S., Colton, S.: A survey of Monte Carlo tree search methods. IEEE Trans. Comput. Intell. AI Games 4(1), 1–43 (2012)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Goffinet, J., Ramanujan, R.: Monte-Carlo tree search for the maximum satisfiability problem. In: Principles and Practice of Constraint Programming, pp. 251–267 (2016)
Gupta, A., Ganai, M.K., Wang, C.: SAT-based verification methods and applications in hardware verification. In: Formal Methods for Hardware Verification, pp. 108–143 (2006)
Knuth, D.E.: Fascicle 6: Satisfiability, the Art of Computer Programming. Combinatorial Algorithms, vol. 4. Addison-Wesley, Boston (2015)
Le Berre, D., Parrain, A.: The SAT4J library, release 2.2, system description. J. Satisfiabil. Boolean Model. Comput. 7, 59–64 (2010)
Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers. In: Haifa Verification Conference, pp. 225–241. Springer, Berlin (2015)
Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 123–140. Springer, Berlin (2016)
Loth, M., Sebag, M., Hamadi, Y., Schoenauer, M.: Bandit-based search for constraint programming. In: International Conference on Principles and Practice of Constraint Programming, pp. 464–480. Springer, Berlin (2013)
Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131–153 (2009)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conference, pp. 530–535 (2001)
Munos, R.: From bandits to Monte-Carlo tree search: the optimistic principle applied to optimization and planning. Tech. Rep. (2014). https://hal.archives-ouvertes.fr/hal-00747575
Previti, A., Ramanujan, R., Schaerf, M., Selman, B.: Monte-Carlo style UCT search for Boolean satisfiability. In: AI*IA 2011: Artificial Intelligence Around Man and Beyond, pp. 177–188 (2011)
Schloeter, J.: A Monte Carlo tree search based conflict-driven clause learning SAT solver. In: Eibl, M., Gaedke, M. (eds.) INFORMATIK 2017, pp. 2549–2560. Gesellschaft für Informatik, Bonn (2017)
Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Combinational test generation using satisfiability. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 15(9), 1167–1176 (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Keszocze, O., Schmitz, K., Schloeter, J., Drechsler, R. (2020). Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning. In: Drechsler, R., Soeken, M. (eds) Advanced Boolean Techniques. Springer, Cham. https://doi.org/10.1007/978-3-030-20323-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-20323-8_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20322-1
Online ISBN: 978-3-030-20323-8
eBook Packages: EngineeringEngineering (R0)