Built on

The complexity of satisfiability problems
T. J. Schaefer · 1978
Earlier work this paper cites.
Efficient conflict driven learning in a boolean satisfiability solver
L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik · 2001
Earlier work this paper cites.

Similar

An extensible sat-solver
N. Eén and N. Sörensson · 2003
Cited alongside, same era.
Backbones and backdoors in satisfiability
P. Kilby, J. Slaney, S. Thiébaux, T. Walsh, et al · 2005
Cited alongside, same era.

Then

Satzilla: portfolio-based algorithm selection for sat
L. Xu, F. Hutter, H. H. Hoos, and K. Leyton-Brown · 2008
Later among the works it cites.
Predicting satisfiability at the phase transition
L. Xu, H. H. Hoos, and K. Leyton-Brown · 2012
Later among the works it cites.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…

2017

Improve SAT-solving with Machine Learning

Wu, Haoze

Understand

In this project, we aimed to improve the runtime of Minisat, a Conflict-Driven Clause Learning (CDCL) solver that solves the Propositional Boolean Satisfiability (SAT) problem.

We first used a logistic regression model to predict the satisfiability of propositional boolean formulae after fixing the values of a certain fraction of the variables in each formula.
We then applied the logistic model and added a preprocessing period to Minisat to determine the preferable initial value (either true or false) of each boolean variable using a Monte-Carlo approach.
Concretely, for each Monte-Carlo trial, we fixed the values of a certain ratio of randomly selected variables, and calculated the confidence that the resulting sub-formula is satisfiable with our logistic regression model.