Ludovic Le Frioux

In Proceedings of the 26 th international conference on principles and practice of constraint programming (CP’20)

Abstract In this paper, we present a machine learning based splitting heuristic for divide-and-conquer parallel Boolean SAT solvers. Splitting heuristics, whether they are look-ahead or look-back, are designed using proxy metrics, which when optimized, approximate the true metric of minimizing solver runtime on sub-formulas resulting from a split. The rationale for such metrics is that they have been empirically shown to be excellent proxies for runtime of solvers, in addition to being cheap to compute in an online fashion.

On the usefulness of clause strengthening in parallel SAT solving

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

2020-08-01

In Proceedings of the 12th NASA formal methods symposium (NFM’20)

Abstract In the context of parallel SATisfiability solving, this paper presents an implementation and evaluation of a clause strengthening algorithm. The developed component can be easily combined with (virtually) any CDCL-like SAT solver. Our implementation is integrated as a part of Painless, a generic and modular framework for building parallel SAT solvers.

Community and LBD-based clause sharing policy for parallel SAT solving

By Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Vijay Ganesh, Fabrice Kordon

2020-06-01

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

Abstract Modern parallel SAT solvers rely heavily on effective clause sharing policies for their performance. The core problem being addressed by these policies can be succinctly stated as “the problem of identifying high-quality learnt clauses” that when shared between the worker nodes of parallel solvers results in improved performance than otherwise. The term “high-quality clauses” is often defined in terms of metrics that solver designers have identified over years of empirical study.

Towards more efficient parallel SAT solving

By Ludovic Le Frioux

2019-07-03

In

Abstract Boolean SATisfiability has been used successfully in many applicative contexts. This is due to the capability of modern SAT solvers to solve complex problems involving millions of variables. Most SAT solvers have long been sequential and based on the CDCL algorithm. The emergence of many-core machines opens new possibilities in this domain. There are numerous parallel SAT solvers that differ by their strategies, programming languages, etc. Hence, comparing the efficiency of the theoretical approaches in a fair way is a challenging task.

Modular and efficient divide-and-conquer SAT solver on top of the Painless framework

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

2019-02-13

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

Abstract Over the last decade, parallel SATisfiability solving has been widely studied from both theoretical and practical aspects. There are two main approaches. First, divide-and-conquer (D&C) splits the search space, each solver being in charge of a particular subspace. The second one, portfolio launches multiple solvers in parallel, and the first to find a solution ends the computation. However although D&C based approaches seem to be the natural way to work in parallel, portfolio ones experimentally provide better performances.

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.

A machine learning based splitting heuristic for divide-and-conquer solvers

On the usefulness of clause strengthening in parallel SAT solving

Community and LBD-based clause sharing policy for parallel SAT solving

Towards more efficient parallel SAT solving

Modular and efficient divide-and-conquer SAT solver on top of the Painless framework

PaInleSS: A framework for parallel SAT solving

Search

Tags