Improve SAT-solving with Machine Learning

TL;DR

This paper enhances SAT solver performance by integrating machine learning to predict variable assignments, specifically targeting backbone variables, leading to a 23% runtime reduction in satisfiable cases, though preprocessing time remains a challenge.

Contribution

Introduces a machine learning-based preprocessing method for SAT solving that improves initial variable assignments, especially for backbone variables, reducing overall runtime.

Findings

Successfully predicted backbone variables with 78% accuracy.

Reduced Minisat runtime by 23% on satisfiable formulas.

Preprocessing time offset gains in runtime performance.

Abstract

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. The initial value of each variable was set based on the mean confidence scores of the trials that started from the literals of that variable. We were particularly interested in setting the initial values of the backbone variables correctly, which are variables that have the same value in all solutions of a SAT formula. Our Monte-Carlo method was able to set 78% of the backbones correctly. Excluding the preprocessing time, compared with the default setting of Minisat, the runtime of Minisat for satisfiable formulae decreased by 23%. However, our method did not outperform vanilla Minisat in runtime, as the decrease in the conflicts was outweighed by the long runtime of the preprocessing period.