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 |
+ | | 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 |
+ | 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>, |
||
− | + | 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} }