• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
CrystalBall: Gazing in the Black Box of SAT Solving.
Mate Soos, Raghav Kulkarni and Kuldeep S. Meel.
In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), July 2019.
Boolean satisfiability is a fundamental problem in computer science with a wide range of applications including planning, configuration management, design and verification of software/hardware systems. The annual SAT competition continues to witness impressive improvements in the performance of the winning SAT solvers largely thanks to the development of new heuristics arising out of intensive collaborative research in the SAT community. Modern SAT solvers achieve scalability and robustness with complex heuristics that are challenging to understand and explain. Consequently, the development of new algorithmic insights has been largely restricted to expert intuitions and evaluation ofthe new insights have been restricted to performance measurement in terms of the runtime of solvers or a proxy for the runtime of solvers. In this context, one may ask: whether it is possible to develop a framework to provide white-box access to the execution of SAT solver that can aid both SAT solver developers and users to synthesize algorithmic heuristics for modern SAT solvers?The primary focus of our project is precisely such a framework, which we call CrystalBall More precisely, we propose to view modern conflict-driven clause learning (CDCL) solvers as a composition of classifiers and regressors for different tasks such as branching, clause memory management, and restarting. The primary objective of this paper is to introduce a framework to peek inside the SAT solvers -- CrystalBall -- to the AI and SAT community. The current version of CrystalBall focuses on deriving a classifier to keep or throw away a learned clause. In a departure from recent machine learning based techniques, CrystalBall, employs supervised learning and uses extensive, multi-gigabyte data extracted from runs of a single SAT solver to perform predictive analytics.
@inproceedings{SKM19,
title={CrystalBall: Gazing in the Black Box of SAT Solving},
author={Soos, Mate and Kulkarni, Raghav and Meel, Kuldeep S.},
bib2html_pubtype={Refereed Conference},
booktitle=SAT,
month=jul,
year={2019},
bib2html_rescat={Solver Engineering},
bib2html_dl_pdf={../Papers/sat19skm.pdf},
code={https://github.com/msoos/cryptominisat/tree/crystalball},
abstract={ Boolean satisfiability is a fundamental problem in computer science with a wide range of applications
including planning, configuration management, design and verification of software/hardware systems.
The annual SAT competition continues to witness impressive improvements in the performance of the winning SAT solvers
largely thanks to the development of new heuristics arising out of intensive collaborative research in the SAT community.
Modern SAT solvers achieve scalability and robustness with complex heuristics that are challenging to understand and explain.
Consequently, the development of new algorithmic insights has been largely restricted to expert intuitions and evaluation of
the new insights have been restricted to performance measurement in terms of the runtime of solvers or a proxy for the
runtime of solvers. In this context, one may ask: whether it is possible to develop a framework to provide white-box
access to the execution of SAT solver that can aid both SAT
solver developers and users to synthesize algorithmic heuristics for modern SAT solvers?
The primary focus of our project is precisely such a framework, which we call CrystalBall
More precisely, we propose to view modern conflict-driven clause learning (CDCL) solvers as a
composition of classifiers and regressors for different tasks such as branching, clause memory
management, and restarting. The primary objective of this paper is to introduce a framework to
peek inside the SAT solvers -- CrystalBall -- to the AI and SAT community. The current version
of CrystalBall focuses on deriving a classifier to keep or throw away a learned clause. In a
departure from recent machine learning based techniques, CrystalBall, employs supervised learning
and uses extensive, multi-gigabyte data extracted from runs of a single SAT solver to perform predictive analytics.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Aug 22, 2024 18:37:34