Online Estimation of SAT Solving Runtime
Shai Haim, Toby Walsh

TL;DR
This paper introduces an online linear model approach to estimate SAT solving runtime, addressing challenges like backtracking and restarts, and improving solver selection and prediction accuracy.
Contribution
It proposes a novel online estimation method for SAT solving cost using a linear model trained during search, enhancing prediction and solver selection.
Findings
Effective runtime predictions on random and structured problems
Early restart predictions improve subsequent estimates
Cost estimations assist in solver portfolio selection
Abstract
We present an online method for estimating the cost of solving SAT problems. Modern SAT solvers present several challenges to estimate search cost including non-chronological backtracking, learning and restarts. Our method uses a linear model trained on data gathered at the start of search. We show the effectiveness of this method using random and structured problems. We demonstrate that predictions made in early restarts can be used to improve later predictions. We also show that we can use such cost estimations to select a solver from a portfolio.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Logic, programming, and type systems · Formal Methods in Verification
