Diversifying a Parallel SAT Solver with Bayesian Moment Matching

Authors

V Vallade, S Nejati, J Sopena, V Ganesh, S Baarir

Where

Symposium on Dependable Software Engineering TheoriesTools and Applications

Place

Beijing, China

Type

inproceedings

Projects

AA"AA" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.

Date

2022-12-08

Abstract

In this paper, we present a Bayesian Moment Matching (BMM) in-processing technique for Conflict-Driven Clause-Learning (CDCL) SAT solvers. BMM is a probabilistic algorithm which takes as input a Boolean formula in conjunctive normal form and a prior on a possible satisfying assignment, and outputs a posterior for a new assignment most likely to maximize the number of satisfied clauses. We invoke this BMM method, as an in-processing technique, with the goal of updating the polarity and branching activity scores. The key insight underpinning our method is that Bayesian reasoning is a powerful way to guide the CDCL search procedure away from fruitless parts of the search space of a satisfiable Boolean formula, and towards those regions that are likely to contain satisfying assignments.

Bibtex (lrde.bib)

@InProceedings{	  vallade.22.setta,
  author	= {V. Vallade and S. Nejati and J. Sopena and V. Ganesh and
		  S. Baarir},
  title		= {Diversifying a Parallel {SAT} Solver with Bayesian Moment
		  Matching},
  booktitle	= {Symposium on Dependable Software Engineering Theories,
		  Tools and Applications},
  year		= 2022,
  address	= {Beijing, China},
  month		= oct,
  abstract	= {In this paper, we present a Bayesian Moment Matching (BMM)
		  in-processing technique for Conflict-Driven Clause-Learning
		  (CDCL) SAT solvers. BMM is a probabilistic algorithm which
		  takes as input a Boolean formula in conjunctive normal form
		  and a prior on a possible satisfying assignment, and
		  outputs a posterior for a new assignment most likely to
		  maximize the number of satisfied clauses. We invoke this
		  BMM method, as an in-processing technique, with the goal of
		  updating the polarity and branching activity scores. The
		  key insight underpinning our method is that Bayesian
		  reasoning is a powerful way to guide the CDCL search
		  procedure away from fruitless parts of the search space of
		  a satisfiable Boolean formula, and towards those regions
		  that are likely to contain satisfying assignments. },
  doi		= {10.1007/978-3-031-21213-0_14}
}