Online Bayesian Moment Matching based SAT Solver Heuristics

Jul 12, 2020



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



About ICML 2020

The International Conference on Machine Learning (ICML) is the premier gathering of professionals dedicated to the advancement of the branch of artificial intelligence known as machine learning. ICML is globally renowned for presenting and publishing cutting-edge research on all aspects of machine learning used in closely related areas like artificial intelligence, statistics and data science, as well as important application areas such as machine vision, computational biology, speech recognition, and robotics. ICML is one of the fastest growing artificial intelligence conferences in the world. Participants at ICML span a wide range of backgrounds, from academic and industrial researchers, to entrepreneurs and engineers, to graduate students and postdocs.

Store presentation

Should this presentation be stored for 1000 years?

How do we store presentations

Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%


Recommended Videos

Presentations on similar topic, category or speaker