Difference between revisions of "Publications/vallade.22.setta"

From LRDE

(Created page with "{{Publication | published = true | date = 2022-12-08 | authors = V Vallade, S Nejati, J Sopena, V Ganesh, S Baarir | title = Diversifying a parallel SAT solver with Bayesian M...")
 
 
Line 3: Line 3:
 
| date = 2022-12-08
  
| date = 2022-12-08
 
| authors = V Vallade, S Nejati, J Sopena, V Ganesh, S Baarir
  
| authors = V Vallade, S Nejati, J Sopena, V Ganesh, S Baarir
−
| title = Diversifying a parallel SAT solver with Bayesian Moment Matching
 +
| title = Diversifying a Parallel SAT Solver with Bayesian Moment Matching
 
| booktitle = Symposium on Dependable Software Engineering TheoriesTools and Applications
  
| booktitle = Symposium on Dependable Software Engineering TheoriesTools and Applications
 
| address = Beijing, China
  
| address = Beijing, China
Line 9: Line 9:
 
| lrdeprojects = AA
  
| lrdeprojects = AA
 
| 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.
  
| 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.
−
| note = accepted
  
 
| type = inproceedings
  
| type = inproceedings
 
| id = vallade.22.setta
  
| id = vallade.22.setta
  +
| identifier = doi:10.1007/978-3-031-21213-0_14
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> vallade.22.setta,
  
@InProceedings<nowiki>{</nowiki> vallade.22.setta,
 
author = <nowiki>{</nowiki>V. Vallade and S. Nejati and J. Sopena and V. Ganesh and
  
author = <nowiki>{</nowiki>V. Vallade and S. Nejati and J. Sopena and V. Ganesh and
 
S. Baarir<nowiki>}</nowiki>,
  
S. Baarir<nowiki>}</nowiki>,
−
title = <nowiki>{</nowiki>Diversifying a parallel SAT solver with Bayesian Moment
 +
title = <nowiki>{</nowiki>Diversifying a Parallel <nowiki>{</nowiki>SAT<nowiki>}</nowiki> Solver with Bayesian Moment
 
Matching<nowiki>}</nowiki>,
  
Matching<nowiki>}</nowiki>,
 
booktitle = <nowiki>{</nowiki>Symposium on Dependable Software Engineering Theories,
  
booktitle = <nowiki>{</nowiki>Symposium on Dependable Software Engineering Theories,
Line 37: Line 37:
 
a satisfiable Boolean formula, and towards those regions
  
a satisfiable Boolean formula, and towards those regions
 
that are likely to contain satisfying assignments. <nowiki>}</nowiki>,
  
that are likely to contain satisfying assignments. <nowiki>}</nowiki>,
−
note = <nowiki>{</nowiki>accepted<nowiki>}</nowiki>
 +
doi = <nowiki>{</nowiki>10.1007/978-3-031-21213-0_14<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
  
<nowiki>}</nowiki>
   

Latest revision as of 10:31, 15 December 2022

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





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/vallade.22.setta&oldid=128267"