Few instances of a computational problem are sui generis; most instead belong to some distribution of related instances, and information gained from solving past instances from the distribution may be leveraged to solve future instances more efficiently. Algorithm portfolio methods and algorithm synthesis systems are two examples of this idea. This paper proposes and demonstrates a third approach. It shows that, for related instances of satisfiability (SAT), variables' values in satisfying assignments can be correlated with structural features of their appearances in those instances, such as the mean polarities of their literals and the statistics of their constraint graph neighborhoods. Experiments on widely-used benchmark collections show that these features can be used by a standard classifier to generate better initial assignments and substantially improve the average performance of a modern solver.

PDF

In Theory and Applications of Satisfiability Testing (SAT), 2011. (extended abstract).

@inproceedings{silverthorn:sat2011, title={Learning Polarity from Structure in SAT}, author={Bryan Silverthorn and Risto Miikkulainen}, booktitle={Theory and Applications of Satisfiability Testing (SAT)}, note={(extended abstract)}, url="http://nn.cs.utexas.edu/?silverthorn:sat2011", year={2011} }