[Submitted on 7 May 2020]

Download PDF

Abstract: There are two competing paradigms in successful SAT solvers: Conflict-driven
clause learning (CDCL) and stochastic local search (SLS). CDCL uses systematic
exploration of the search space and has the ability to learn new clauses. SLS
examines the neighborhood of the current complete assignment. Unlike CDCL, it
lacks the ability to learn from its mistakes. This work revolves around the
question whether it is beneficial for SLS to add new clauses to the original
formula. We experimentally demonstrate that clauses with a large number of
correct literals w. r. t. a fixed solution are beneficial to the runtime of
SLS. We call such clauses high-quality clauses.

Empirical evaluations show that short clauses learned by CDCL possess the
high-quality attribute. We study several domains of randomly generated
instances and deduce the most beneficial strategies to add high-quality clauses
as a preprocessing step. The strategies are implemented in an SLS solver, and
it is shown that this considerably improves the state-of-the-art on randomly
generated instances. The results are statistically significant.