Hi every one,
I'm happy to annonce the publication of the following papers :
1) In SETTA'2022
Title : Diversifying a parallel SAT solver with Bayesian Moment Matching
Authors : V. Vallade, S.Nejati, J.Sopena, V. Ganesh and S. Baarir
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.
2) In VMCAI'2023
Title : CosySEL: Improving SAT Solving Using Local Symmetries
Authors : S. Saouli , S. Baarir , C. Dutheillet and J. Devriendt
Abstract : Many satisfiability problems exhibit symmetry properties. Thus, the development
of symmetry exploitation techniques seems a natural way to try to improve the efficiency
of solvers by preventing them from exploring isomorphic parts of the search space. These
techniques can be classified into two categories: dynamic and static symmetry breaking.
Static approaches have often appeared to be more effective than dynamic ones. But although
these approaches can be considered as complementary, very few works have tried to combine
them. In this paper, we present a new tool, CosySEL, that implements a composition of the
static Effective Symmetry Breaking Predicates (esbp) technique with the dynamic Symmetric
Explanation Learning (sel). esbp exploits symmetries to prune the search tree and sel uses
symmetries to speed up the tree traversal. These two accelerations are complementary and
their combination was made possible by the introduction of Local symmetries. We conduct
our experiments on instances issued from the last ten sat competitions and the results
show that our tool outperforms the existing tools on highly symmetrical problems
See you,
Souheib.
Show replies by date