Souheib Baarir

CDCLSym: Introducing effective symmetry breaking in SAT solving

By Hakan Metin, Souheib Baarir, Maximilien Colange, Fabrice Kordon

2018-01-05

In Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS’18)

Abstract SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones.

Continue reading

PaInleSS: A framework for parallel SAT solving

By Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon

2017-06-30

In Proceedings of the 20th international conference on theory and applications of satisfiability testing (SAT’17)

Abstract Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are now numerous solvers that dier by parallelization strategies, programming languages, concurrent programming, involved libraries, etc. Hence, comparing the eciency of the theoretical approaches is a challenging task. Moreover, the introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool.

Continue reading

Parallel learning portfolio-based solvers

By Tarek Menouer, Souheib Baarir

2017-06-01

In Proceedings of the international conference on computational science (ICCS)

Abstract Exploiting multi-core architectures is a way to tackle the CPU time consumption when solving SAT- isfiability (SAT) problems. Portfolio is one of the main techniques that implements this principle. It consists in making several solvers competing, on the same problem, and the winner will be the first that answers. In this work, we improved this technique by using a learning schema, namely the Exploration- Exploitation using Exponential weight (EXP3), that allows smart resource allocations.

Continue reading

Parallel satisfiability solver based on hybrid partitioning method

By Tarek Menouer, Souheib Baarir

2017-03-01

In Proceedings of the 25th euromicro international conference on parallel, distributed and network-based processing (PDP)

Abstract This paper presents a hybrid partitioning method used to improve the performance of solving a Satisfiability (SAT) problems. The principle of our approach consist firstly to apply a static partitioning to decompose the search tree in finite set of disjoint sub-trees, than assign each sub-tree to one computing core. However it is not easy to choose the relevant branching variables to partition the search tree. We propose in this context to partition the search tree according to the variables that occur more frequently then others.

Continue reading

SAT-based minimization of deterministic $\omega$-automata

By Souheib Baarir, Alexandre Duret-Lutz

2015-09-01

In Proceedings of the 20th international conference on logic for programming, artificial intelligence, and reasoning (LPAR’15)

Abstract We describe a tool that inputs a deterministic $\omega$-automaton with any acceptance condition, and synthesizes an equivalent $\omega$-automaton with another arbitrary acceptance condition and a given number of states, if such an automaton exists. This tool, that relies on a SAT-based encoding of the problem, can be used to provide minimal $\omega$-automata equivalent to given properties, for different acceptance conditions.

Continue reading

Mechanizing the minimization of deterministic generalized Büchi automata

By Souheib Baarir, Alexandre Duret-Lutz

2014-03-21

In Proceedings of the 34th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’14)

Abstract Deterministic Büchi automata (DBA) are useful to (probabilistic) model checking and synthesis. We survey techniques used to obtain and minimize DBAs for different classes of properties. We extend these techniques to support DBA that have generalized and transition-based acceptance (DTGBA) as they can be even smaller. Our minimization technique—a reduction to a SAT problem—synthesizes a DTGBA equivalent to the input DTGBA for any given number of states and number of acceptance sets (assuming such automaton exists).

Continue reading

Search

Tags