Bertrand Mazure

AAAI Conference 2014 Conference Paper

An Experimentally Efficient Method for (MSS,CoMSS) Partitioning

• Eric Grégoire
• Jean-Marie Lagniez
• Bertrand Mazure

The concepts of MSS (Maximal Satisfiable Subset) and CoMSS (also called Minimal Correction Subset) play a key role in many A. I. approaches and techniques. In this paper, a novel algorithm for partitioning a Boolean CNF formula into one MSS and the corresponding CoMSS is introduced. Extensive empirical evaluation shows that it is more robust and more efficient on most instances than currently available techniques.

ECAI Conference 2014 Conference Paper

Enforcing Solutions in Constraint Networks

• Éric Grégoire
• Jean-Marie Lagniez
• Bertrand Mazure

A method is proposed to enforce specific solutions in constraint networks. Contrary to previous approaches, it yields a set of constraints to be dropped whose cardinality is minimal.

IJCAI Conference 2013 Conference Paper

Preserving Partial Solutions while Relaxing Constraint Networks

• Éric Grégoire
• Jean-Marie Lagniez
• Bertrand Mazure

An extension of the CSP optimization framework tailored to identify fair solutions to instances involving multiple optimization functions is studied. Two settings are considered, based on the maximization of the minimum value over all the given functions (MAX-MIN approach) and on its lexicographical refinement where, over all solutions maximizing the minimum value, those maximizing the second minimum value are preferred, and so on, until all functions are considered (LEXMAX-MIN approach). For both settings, the complexity of computing an optimal solution is analyzed and the tractability frontier is charted for acyclic instances, w. r. t. the number and the domains of the functions to be optimized. Larger islands of tractability are then identified via a novel structural approach, based on a notion of guard that is designed to deal with the interactions among constraint scopes and optimization functions.

IJCAI Conference 2013 Conference Paper

Preserving Partial Solutions while Relaxing Constraint Networks

• Éric Grégoire
• Jean-Marie Lagniez
• Bertrand Mazure

This paper is about transforming constraint networks to accommodate additional constraints in specific ways. The focus is on two intertwined issues. First, we investigate how partial solutions to an initial network can be preserved from the potential impact of additional constraints. Second, we study how more permissive constraints, which are intended to enlarge the set of solutions, can be accommodated in a constraint network. These two problems are studied in the general case and the light is shed on their relationship. A case study is then investigated where a more permissive additional constraint is taken into account through a form of network relaxation, while some previous partial solutions are preserved at the same time.

SAT Conference 2011 Conference Paper

On Freezing and Reactivating Learnt Clauses

• Gilles Audemard
• Jean-Marie Lagniez
• Bertrand Mazure
• Lakhdar Saïs

Abstract In this paper, we propose a new dynamic management policy of the learnt clause database in modern sat solvers. It is based on a dynamic freezing and activation principle of the learnt clauses. At a given search state, using a relevant selection function, it activates the most promising learnt clauses while freezing irrelevant ones. In this way, clauses learned at previous steps can be frozen at the current step and might be activated again in future steps of the search process. Our strategy tries to exploit pieces of information gathered from the past to deduce the relevance of a given clause for the remaining search steps. This policy contrasts with all the well-known deletion strategies, where a given learned clause is definitely eliminated. Experiments on sat instances taken from the last competitions demonstrate the efficiency of our proposed technique.

IJCAI Conference 2007 Conference Paper

• Eacute; ric Gr
• eacute; goire
• Bertrand Mazure
• C
• eacute; dric Piette

In this paper, a new complete technique to compute Maximal Satisfiable Subsets (MSS) and Minimally Unsatisfiable Subformulas (MUS) of sets of Boolean clauses is introduced. The approach improves the currently most efficient complete technique in several ways. It makes use of the powerful concept of critical clause and of a computationally inexpensive local search oracle to boost an exhaustive algorithm proposed by Liffiton and Sakallah. These features can allow exponential efficiency gains to be obtained. Accordingly, experimental studies show that this new approach outperforms the best current existing exhaustive ones.

ECAI Conference 2006 Conference Paper

Extracting MUSes

• Éric Grégoire
• Bertrand Mazure
• Cédric Piette

Minimally unsatisfiable subformulas (in short, MUSes) represent the smallest explanations for the inconsistency of SAT instances in terms of the number of involved clauses. Extracting MUSes can thus prove valuable because it circumscribes the sources of contradiction in an instance. In this paper, a new heuristic-based approach to approximate or compute MUSes is presented. It is shown that it often outperforms current competing ones.

SAT Conference 2004 Conference Paper

Automatic Extraction of Functional Dependencies

• Éric Grégoire
• Richard Ostrowski
• Bertrand Mazure
• Lakhdar Saïs

In this paper, a new polynomial time technique for extracting functional dependencies in Boolean formulas is proposed. It makes an original use of the well-known Boolean constraint propagation technique (BCP) in a new preprocessing approach that extracts more hidden Boolean functions and dependent variables than previously published approaches on many classes of instances.

SAT Conference 2004 Conference Paper

Dealing with Symmetries in Quantified Boolean Formulas

• Gilles Audemard
• Bertrand Mazure
• Lakhdar Saïs

Many reasoning task and combinatorial problems exhibit symmetries. Exploiting symmetries has been proved very important in reducing search efforts. This important task is widely investigated in constraint satisfaction problems and satisfiability of boolean formulas. In this paper, we show how symmetries can be naturally extended to Quantified Boolean Formulas (QBFs). A symmetries detection algorithm is given, extending the CNF approach proposed by Aloul et al. A new hybrid solver that handle QBFs and Symmetry Breaking predicates is then proposed. Experiments, conducted on instances from the last competition on QBFs, show that many of them contains symmetries. Breaking such symmetries lead to interesting improvements of QBFs solver on certain class of instances.

AAAI Conference 1997 Conference Paper

Tabu Search for SAT

• Bertrand Mazure

In this paper, tabu search for SAT is investigated from an experimental point of view. To this end, TSAT, a basic tabu search algorithm for SAT, is introduced and compared with Selman et al. Random Walk Strategy GSAT procedure, in short RWS-GSAT. TSAT does not involve the additional stochastic process of RWS-GSAT. This should facilitate the understanding of why simple local search methods for SAT work. It is shown that the length of the tabu list plays a critical role in the performance of the algorithm. Moreover, surprising properties about the (experimental) optimal length of the tabu list are exhibited, raising interesting issues about the nature of hard random SAT problems.

IJCAI Conference 1997 Conference Paper

Tractable Cover Compilations

• Yacine Boujkhad
• Eric Gregoire
• Pierre Marquis
• Bertrand Mazure
• Lakhdar Sais

Tractable covers are introduced as a new ap­ proach to equivalence-preserving compilation of propositional knowledge bases. First, a gen­ eral framework is presented. Then, two specific cases are considered. In the first one, partial interpretations are used to shape the knowl­ edge base into tractable formulas from several possible classes. In the second case, they are used to derive renamable Horn formulas. This last case is proved less space-consuming than prime implicants cover compilations for every knowledge base. Finally, experimental results show that the new approaches can prove effi­ cient w. r. t. direct query answering and offer significant time and space savings w. r. t. prime implicants covers.