Laurent Simon

JAIR Journal 2019 Journal Article

Community Structure in Industrial SAT Instances

• Carlos Ansótegui
• Maria Luisa Bonet
• Jesús Giráldez-Cru
• Jordi Levy
• Laurent Simon

Modern SAT solvers have experienced a remarkable progress on solving industrial instances. It is believed that most of these successful techniques exploit the underlying structure of industrial instances. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. Representing SAT instances as graphs, we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver, and observe that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. Motivated by this observation, we finally present an application that exploits the community structure to detect relevant learned clauses, and we show that detecting these clauses results in an improvement on the performance of the SAT solver. Empirically, we observe that this improves the performance of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.

IJCAI Conference 2018 Conference Paper

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

• Jan Elffers
• Jesús Giráldez-Cru
• Stephan Gocht
• Jakob Nordström
• Laurent Simon

Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.

AAAI Conference 2017 Conference Paper

Diagnosability Planning for Controllable Discrete Event Systems

• Hassan Ibrahim
• Philippe Dague
• Alban Grastien
• Lina Ye
• Laurent Simon

In this paper, we propose an approach to ensure the diagnosability of a partially controllable system. Given a model of correct and faulty behaviors of a partially observable discrete event system, equipped with a set of elementary actions that do not intertwine with autonomous events, we search a diagnosability plan, i. e. , a sequence of applicable actions that leads the system from an initial belief state (a set of potentially current states) to a diagnosable belief state, in which the system is then left to run freely. This helps in reducing the diagnosis interaction with running systems and can be applied, e. g. , on the output of a repair plan, like in power networks. The two successive stages of this approach keep diagnosability planning, including diagnosability tests, in PSPACE in comparison to the EXPTIME test for the more complex active diagnosability used usually in such cases. For this, we propose to construct incrementally the twin plant structure of the given system and to exploit its parts already constructed while testing the candidate plans and constructing its next parts. This helps in pruning the twin plant constructions and many non-diagnosability plan tests. We have created a special benchmark and tested three proposed methods, according to the recycling level of twin plants construction, with one cost function used for plan optimality and an optional heuristics.

IJCAI Conference 2013 Conference Paper

Just-in-Time Compilation of Knowledge Bases

• Gilles Audemard
• Jean-Marie Lagniez
• Laurent Simon

Since the first principles of Knowledge Compilation (KC), most of the work has been focused in finding a good compilation target language in terms of compromises between compactness and expressiveness. The central idea remains unchanged in the last fifteen years: an off-line, very hard, stage, allows to “compile” the initial theory in order to guarantee (theoretically) an efficient on-line stage, on a set of predefined queries and operations. We propose a new “Just-in-Time” approach for KC. Here, any Knowledge Base (KB) will be immediately available for queries, and the effort spent on past queries will be partly amortized for future ones. To guarantee efficient answers, we rely on the tremendous progresses made in the practical solving of SAT and incremental SAT applicative problems. Even if each query may be theoretically hard, we show that our approach outperforms previous KC approaches on the set of classical problems used in the field, and allows to handle problems that are out of the scope of current approaches.

AAAI Conference 2013 Conference Paper

Resolution and Parallelizability: Barriers to the Efficient Parallelization of SAT Solvers

• George Katsirelos
• Ashish Sabharwal
• Horst Samulowitz
• Laurent Simon

Recent attempts to create versions of Satisfiability (SAT) solvers that exploit parallel hardware and information sharing have met with limited success. In fact, the most successful parallel solvers in recent competitions were based on portfolio approaches with little to no exchange of information between processors. This experience contradicts the apparent parallelizability of exploring a combinatorial search space. We present evidence that this discrepancy can be explained by studying SAT solvers through a proof complexity lens, as resolution refutation engines. Starting with the observation that a recently studied measure of resolution proofs, namely depth, provides a (weak) upper bound to the best possible speedup achievable by such solvers, we empirically show the existence of bottlenecks to parallelizability that resolution proofs typically generated by SAT solvers exhibit. Further, we propose a new measure of parallelizability based on the best-case makespan of an offline resource constrained scheduling problem. This measure explicitly accounts for a bounded number of parallel processors and appears to empirically correlate with parallel speedups observed in practice. Our findings suggest that efficient parallelization of SAT solvers is not simply a matter of designing the right clause sharing heuristics; even in the best case, it can be — and indeed is — hindered by the structure of the resolution proofs current SAT solvers typically produce.

AIJ Journal 2012 Journal Article

Optimizing with minimum satisfiability

• Chu Min Li
• Zhu Zhu
• Felip Manyà
• Laurent Simon

IJCAI Conference 2011 Conference Paper

Minimum Satisfiability and Its Applications

• Chu-Min Li
• Zhu Zhu
• Felip Many
• agrave;
• Laurent Simon

We define solving techniques for the Minimum Satisfiability Problem (MinSAT), propose an efficient branch-and-bound algorithm to solve the Weighted Partial MinSAT problem, and report on an empirical evaluation of the algorithm on Min-3SAT, MaxClique, and combinatorial auction problems. Techniques solving MinSAT are substantially different from those for the Maximum Satisfiability Problem (MaxSAT). Our results provide empirical evidence that solving combinatorial optimization problems by reducing them to MinSAT may be substantially faster than reducing them to MaxSAT, and even competitive with specific algorithms. We also use MinSAT to study an interesting correlation between the minimum number and the maximum number of satisfied clauses of a SAT instance.

AAAI Conference 2010 Conference Paper

A Restriction of Extended Resolution for Clause Learning SAT Solvers

• Gilles Audemard
• George Katsirelos
• Laurent Simon

Modern complete SAT solvers almost uniformly implement variations of the clause learning framework introduced by Grasp and Chaff. The success of these solvers has been theoretically explained by showing that the clause learning framework is an implementation of a proof system which is as poweful as resolution. However, exponential lower bounds are known for resolution, which suggests that significant advances in SAT solving must come from implementations of more powerful proof systems. We present a clause learning SAT solver that uses extended resolution. It is based on a restriction of the application of the extension rule. This solver outperforms existing solvers on application instances from recent SAT competitions as well as on instances that are provably hard for resolution, such as XOR-SAT instances.

IJCAI Conference 2009 Conference Paper

• Gilles Audemard
• Laurent Simon

Beside impressive progresses made by SAT solvers over the last ten years, only few works tried to understand why Conflict Directed Clause Learning algorithms (CDCL) are so strong and efficient on most industrial applications. We report in this work a key observation of CDCL solvers behavior on this family of benchmarks and explain it by an unsuspected side effect of their particular Clause Learning scheme. This new paradigm allows us to solve an important, still open, question: How to designing a fast, static, accurate, and predictive measure of new learnt clauses pertinence. Our paper is followed by empirical evidences that show how our new learning scheme improves state-of-the art results by an order of magnitude on both SAT and UNSAT industrial problems.

LPAR Conference 2008 Conference Paper

Distributed Consistency-Based Diagnosis

• Vincent Armant
• Philippe Dague
• Laurent Simon

Abstract A lot of methods exist to prevent errors and incorrect behaviors in a distributed framework, where all peers work together for the same purpose, under the same protocol. For instance, one may limit them by replication of data and processes among the network. However, with the emergence of web services, the willing for privacy, and the constant growth of data size, such a solution may not be applicable. For some problems, failure of a peer has to be detected and located by the whole system. In this paper, we propose an approach to diagnose abnormal behaviors of the whole system by extending the well known consistency-based diagnosis framework to a fully distributed inference system, where each peer only knows the existence of its neighbors. Contrasting with previous works on model-based diagnosis, our approach computes all minimal diagnoses in an incremental way, without needs to get any conflict first.

IJCAI Conference 2007 Conference Paper

• Gilles Audemard
• Laurent Simon

Local search algorithms for satisfiability testing are still the best methods for a large number of problems, despite tremendous progresses observed on complete search algorithms over the last few years. However, their intrinsic limit does not allow them to address UNSAT problems. Ten years ago, this question challenged the community without any answer: was it possible to use local search algorithm for UNSAT formulae? We propose here a first approach addressing this issue, that can beat the best resolution-based complete methods. We define the landscape of the search by approximating the number of filtered clauses by resolution proof. Furthermore, we add high-level reasoning mechanism, based on Extended Resolution and Unit Propagation Look-Ahead to make this new and challenging approach possible. Our new algorithm also tends to be the first step on two other challenging problems: obtaining short proofs for UNSAT problems and build a real local-search algorithm for QBF.

ECAI Conference 2004 Conference Paper

Distributed Reasoning in a Peer-to-Peer Setting

• Philippe Adjiman
• Philippe Chatalic
• François Goasdoué
• Marie-Christine Rousset
• Laurent Simon