Diversifying a Parallel SAT Solver with Bayesian Moment Matching

From LRDE

Revision as of 09:31, 15 December 2022 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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}
}