Abstract:
In this paper, we present a Bayesian Moment Matching (BMM) based method aimed at solving the initialization problem in Boolean SAT solvers. The initialization problem can be stated as follows: given a SAT formula φ, compute an initial order over the variables of φ and values/polarity for these variables such that the runtime of SAT solvers on input φ is minimized. At the start of a solver run, our BMM-based methods compute a posterior probability distribution for an assign- ment to the variables of the input formula after analyzing its clauses. This probability distribution is then used by the solver to initialize its search. We perform extensive experiments to evaluate the efficacy of our BMM-based heuristic against 4 other initialization methods (random, survey propagation, Jeroslow-Wang, and default) in state-of-the-art solvers, MapleCOMSPS and MapleLCMDistChronotBT over the SAT competition 2018 application benchmark, as well as the best-known solvers in the cryptographic category, namely, CryptoMiniSAT, Glucose and MapleSAT. On the cryptographic benchmark, BMM-based solvers out-perform all other initialization methods. Further, the BMM-based MapleCOMSPS significantly out-perform the same solver using all other initialization methods by 12 additional instances solved and better average runtime, over the SAT 2018 competition benchmark.
We performed extensive experiments to evaluate the efficacy of our BMM-based heuristics on SAT competition 2018 application and hard cryptographic benchmarks. We implemented our heuristics in state-of-the-art solvers (MapleCOMSPS and MapleLCMDistChronotBT for SAT competition 2018 application benchmarks) and CryptoMiniSAT, Glucose and MapleSAT (in the context of cryptographic benchmarks), against 4 other initialization methods. Our solvers out-perform the baselines by solving 12 more instances from the SAT competition 2018 application benchmark and are %40 faster on average in solving hard cryptographic instances.
