Daniel Le Berre

IJCAI Conference 2025 Conference Paper

A SAT-based Method for Counting All Singleton Attractors in Boolean Networks

• Rei Higuchi
• Takehide Soh
• Daniel Le Berre
• Morgan Magnin
• Mutsunori Banbara
• Naoyuki Tamura

Boolean networks (BNs) are widely used to model biological regulatory networks. Attractors here hold significant meaning as they represent long-term behaviors such as homeostasis and the results of cell differentiation. As such, computing attractors is of critical importance to guarantee the validity of a model or to assess its stability and robustness. However, this problem is quite challenging when it comes to large real-world models. To overcome the limits of state-of-the-art BDD-based or ASP-based enumeration approaches, we introduce a SAT-based approach to compute fixed points (singleton attractors) of BN and exhibit its merits for counting the number of singleton attractors of large-scale benchmarks well established in the literature.

SAT Conference 2025 Conference Paper

SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints

• Ryoga Ohashi
• Takehide Soh
• Daniel Le Berre
• Hidetomo Nabeshima
• Mutsunori Banbara
• Katsumi Inoue
• Naoyuki Tamura

In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.

SAT Conference 2021 Conference Paper

On Dedicated CDCL Strategies for PB Solvers

• Daniel Le Berre
• Romain Wallon

Abstract Current implementations of pseudo-Boolean (PB) solvers working on native PB constraints are based on the CDCL architecture which empowers highly efficient modern SAT solvers. In particular, such PB solvers not only implement a (cutting-planes-based) conflict analysis procedure, but also complementary strategies for components that are crucial for the efficiency of CDCL, namely branching heuristics, learned constraint deletion and restarts. However, these strategies are mostly reused by PB solvers without considering the particular form of the PB constraints they deal with. In this paper, we present and evaluate different ways of adapting CDCL strategies to take the specificities of PB constraints into account while preserving the behavior they have in the clausal setting. We implemented these strategies in two different solvers, namely Sat4j (for which we consider three configurations) and RoundingSat. Our experiments show that these dedicated strategies allow to improve, sometimes significantly, the performance of these solvers, both on decision and optimization problems.

IJCAI Conference 2020 Conference Paper

On Irrelevant Literals in Pseudo-Boolean Constraint Learning

• Daniel Le Berre
• Pierre Marquis
• Stefan Mengel
• Romain Wallon

Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting planes based inference is not as well understood as clause learning in conflict-driven clause learning solvers. In this paper, we show that PB constraints derived using cutting planes may contain irrelevant literals, i. e. , literals whose assigned values (whatever they are) never change the truth value of the constraint. Such literals may lead to infer constraints that are weaker than they should be, impacting the size of the proof built by the solver, and thus also affecting its performance. This suggests that current implementations of PB solvers based on cutting planes should be reconsidered to prevent the generation of irrelevant literals. Indeed, detecting and removing irrelevant literals is too expensive in practice to be considered as an option (the associated problem is NP-hard).

SAT Conference 2020 Conference Paper

On Weakening Strategies for PB Solvers

• Daniel Le Berre
• Pierre Marquis
• Romain Wallon

Abstract Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generalized resolution, which allows to infer strong constraints, but suffers from the growth of coefficients it generates while combining pseudo-Boolean constraints. Another variant consists in using weakening and division, which is more efficient in practice but may infer weaker constraints. In both cases, weakening is mandatory to derive conflicting constraints. However, its impact on the performance of pseudo-Boolean solvers has not been assessed so far. In this paper, new application strategies for this rule are studied, aiming to infer strong constraints with small coefficients. We implemented them in Sat4j and observed that each of them improves the runtime of the solver. While none of them performs better than the others on all benchmarks, applying weakening on the conflict side has surprising good performance, whereas applying partial weakening and division on both the conflict and the reason sides provides the best results overall.

IJCAI Conference 2018 Conference Paper

Pseudo-Boolean Constraints from a Knowledge Representation Perspective

• Daniel Le Berre
• Pierre Marquis
• Stefan Mengel
• Romain Wallon

We study pseudo-Boolean constraints (PBC) and their special case cardinality constraints (CARD) from the perspective of knowledge representation. To this end, the succinctness of PBC and CARD is compared to that of many standard propositional languages. Moreover, we determine which queries and transformations are feasible in polynomial time when knowledge is represented by PBC or CARD, and which are not (unconditionally or unless P = NP). In particular, the advantages and disadvantages compared to CNF are discussed.

KR Conference 2018 Short Paper

Space-Awareness in a SAT-Based Approach For PSPACE Modal Logics

• Jean Marie Lagniez
• Daniel Le Berre
• Tiago de Lima
• Valentin Montmirail

IJCAI Conference 2017 Conference Paper

A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem

• Jean-Marie Lagniez
• Daniel Le Berre
• Tiago de Lima
• Valentin Montmirail

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both a CEGAR and a RECAR approach for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.

AAAI Conference 2017 Conference Paper

A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem

• Thomas Caridroit
• Jean-Marie Lagniez
• Daniel Le Berre
• Tiago de Lima
• Valentin Montmirail

We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula φ can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula. We implemented a generic SATbased approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i. e. the number of modalities of φ and to evaluate the effect of our caching technique. We also compared our solver against existing modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. These promising results open interesting research directions for the practical resolution of others modal logics (e. g. K, KT, S4)

ECAI Conference 2016 Conference Paper

Fixed-Parameter Tractable Optimization Under DNNF Constraints

• Frédéric Koriche
• Daniel Le Berre
• Emmanuel Lonca
• Pierre Marquis

Minimizing a cost function under a set of combinatorial constraints is a fundamental, yet challenging problem in AI. Fortunately, in various real-world applications, the set of constraints describing the problem structure is much less susceptible to change over time than the cost function capturing user's preferences. In such situations, compiling the set of feasible solutions during an offline step can make sense, especially when the target compilation language renders computationally easier the generation of optimal solutions for cost functions supplied "on the fly", during the online step. In this paper, the focus is laid on Boolean constraints compiled into DNNF representations. We study the complexity of the minimization problem for several families of cost functions subject to DNNF constraints. Beyond linear minimization which is already known to be tractable in the DNNF language, we show that both quadratic minimization and submodular minization are fixed-parameter tractable for various subsets of DNNF. In particular, the fixed-parameter tractability of constrained submodular minimization is established using a natural parameter capturing the structural dissimilarity between the submodular cost function and the DNNF representation.

SAT Conference 2014 Conference Paper

Detecting Cardinality Constraints in CNF

• Armin Biere
• Daniel Le Berre
• Emmanuel Lonca
• Norbert Manthey

Abstract We present novel approaches to detect cardinality constraints expressed in CNF. The first approach is based on a syntactic analysis of specific data structures used in SAT solvers to represent binary and ternary clauses, whereas the second approach is based on a semantic analysis by unit propagation. The syntactic approach computes an approximation of the cardinality constraints AtMost-1 and AtMost-2 constraints very fast, whereas the semantic approach has the property to be generic, i. e. it can detect cardinality constraints AtMost- k for any k, at a higher computation cost. Our experimental results suggest that both approaches are efficient at recovering AtMost-1 and AtMost-2 cardinality constraints.

JELIA Conference 2014 Conference Paper

Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem

• Takehide Soh
• Daniel Le Berre
• Stéphanie Roussel 0001
• Mutsunori Banbara
• Naoyuki Tamura

Abstract The Hamiltonian cycle problem (HCP) is the problem of finding a spanning cycle in a given graph. HCP is NP-complete and has been known as an important problem due to its close relationship to the travelling salesman problem (TSP), which can be seen as an optimization variant of finding a minimum cost cycle. In a different viewpoint, HCP is a special case of TSP. In this paper, we propose an incremental SAT-based method for solving HCP. The number of clauses needed for a CNF encoding of HCP often prevents SAT-based methods from being scalable. Our method reduces that number of clauses by relaxing some constraints and by handling specifically cardinality constraints. Our approach has been implemented on top of the SAT solver Sat4j using Scarab. An experimental evaluation is carried out on several benchmark sets and compares our incremental SAT-based method against an existing eager SAT-based method and specialized methods for HCP.

ICAPS Conference 2013 Conference Paper

Planning Personalised Museum Visits

• Daniel Le Berre
• Pierre Marquis
• Stéphanie Roussel 0001

In this paper, we consider the problem of designing personalised museum visits. Given a set of preferences and constraints a visitor might express on her visit, the aim is to compute the tour that best matches her requirements. The museum visits problem can be expressed as a planning problem, with cost optimization. We show how to bound the number of steps required to find an optimal solution, via the resolution of an instance of the shortest complete walk problem. We also point out an alternative encoding of the museum visits problem as an optimization problem with pseudo-Boolean constraints and a linear objective function. We have evaluated several constraints solvers, a planner and a tailored solver on a number of benchmarks, representing various instances of the museum visits problem corresponding to real museums. Our empirical results show the feasibility of both the planning and the constraint programming approaches. Optimal solutions can be computed for short visits and ``practically good'' solutions for much longer visits.

ECAI Conference 2006 Conference Paper

An Alternative Inference for Qualitative Choice Logic

• Salem Benferhat
• Daniel Le Berre
• Karima Sedki

Qualitative Choice Logic adds to classical propositional logic a new connective, called ordered disjunction, used to express preferences between alternatives. We present an alternative inference relation for the QCL language that overcomes some QCL limitations.

KR Conference 2006 Conference Paper

Representing Policies for Quantified Boolean Formulas

• Sylvie Coste-Marquis
• Helene Fargier
• Jerome Lang
• Daniel Le Berre
• Pierre Marquis

The practical use of Quantified Boolean Formulae (QBFs) often calls for more than solving the validity problem QBF. For this reason we investigate the corresponding function problems whose expected outputs are policies. QBFs which do not evaluate to true do not have any solution policy, but can be of interest nevertheless; for handling them, we introduce a notion of partial policy.

SAT Conference 2005 Conference Paper

A Branching Heuristics for Quantified Renamable Horn Formulas

• Sylvie Coste-Marquis
• Daniel Le Berre
• Florian Letombe

Abstract Many solvers have been designed for \(\mathcal{QBF}\) s, the validity problem for Quantified Boolean Formulas for the past few years. In this paper, we describe a new branching heuristics whose purpose is to promote renamable Horn formulas. This heuristics is based on Hébrard’s algorithm for the recognition of such formulas. We present some experimental results obtained by our qbf solver Qbfl with the new branching heuristics and show how its performances are improved.

AIJ Journal 2004 Journal Article

Qualitative choice logic

• Gerhard Brewka
• Salem Benferhat
• Daniel Le Berre

Qualitative choice logic (QCL) is a propositional logic for representing alternative, ranked options for problem solutions. The logic adds to classical propositional logic a new connective called ordered disjunction: A × → B intuitively means: if possible A, but if A is not possible then at least B. The semantics of qualitative choice logic is based on a preference relation among models. Consequences of QCL theories can be computed through a compilation to stratified knowledge bases which in turn can be compiled to classical propositional theories. We also discuss potential applications of the logic, several variants of QCL based on alternative inference relations, and their relation to existing nonmonotonic formalisms. 1 1 This is a revised and extended version of the paper that appeared in Proc. 8th Internat. Conference on Principles of Knowledge Representation and Reasoning (KR 2002), Toulouse, France, 2002, pp. 158–169.

AIJ Journal 2004 Journal Article

Weakening conflicting information for iterated revision and knowledge integration

• Salem Benferhat
• Souhila Kaci
• Daniel Le Berre
• Mary-Anne Williams

The ability to handle exceptions, to perform iterated belief revision and to integrate information from multiple sources is essential for a commonsense reasoning agent. These important skills are related in the sense that they all rely on resolving inconsistent information. In this paper we develop a novel and useful strategy for conflict resolution, and compare and contrast it with existing strategies. Ideally the process of conflict resolution should conform with the principle of Minimal Change and should result in the minimal loss of information. Our approach to minimizing the loss of information is to weaken information involved in conflicts rather than completely discarding it. We implemented and tested the relative performance of our new strategy in three different ways. Surprisingly, we are able to demonstrate that it provides a computationally effective compilation of the lexicographical strategy; a strategy which is known to have desirable theoretical properties.

SAT Conference 2003 Conference Paper

Challenges in the QBF Arena: the SAT'03 Evaluation of QBF Solvers

• Daniel Le Berre
• Laurent Simon 0001
• Armando Tacchella

Abstract The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important issue in several research fields such as Formal Verification, Planning, and Reasoning about Knowledge. Several QBF solvers have been implemented in the last few years, most of them extending the well-known Davis, Putnam, Logemann, Loveland procedure (DPLL) for propositional satisfiability (SAT). At the same time, a substantial breed of QBF benchmarks emerged, both in the form of statistical models for the generation of random formulas, and in the form of real-world instances. In this paper we report about the – first ever – evaluation of QBF solvers that was run as a joint event to SAT’03 Conference on Theory and Applications of Satisfiability Testing. Owing to the relative youngness of QBF tools and applications, we decided to run the comparison on a non-competitive basis, using the same technology that powered SAT’02 and SAT’03 competitions of SAT solvers. Running the evaluation enabled us to collect all sorts of data regarding the relative strength of different solvers and methods, the quality of the benchmarks, and to understand some of the current challenges for researchers involved in the QBF arena.

SAT Conference 2003 Conference Paper

The Essentials of the SAT 2003 Competition

• Daniel Le Berre
• Laurent Simon 0001

Abstract The SAT 2003 Competition ran in February – May 2003, in conjunction with SAT’03 (the Sixth Fifth International Symposium on the Theory and Applications of Satisfiability Testing). One year after the SAT 2002 competition, it was not clear that significant progress could be made in the area in such a little time. The competition was a success – 34 solvers and 993 benchmarks, needing 522 CPU days – with a number of brand new solvers. Several 2003 competitors were even able to solve within 15mn benchmarks remained unsolved within 6 hours by 2002 competitors. We report here the essential results of the competition, interpret and statistically analyse them, and at last provide some suggestions for the future competitions.

KR Conference 2002 Conference Paper

Qualitative Choice Logic

• Gerhard Brewka
• Salem Benferhat
• Daniel Le Berre

ECAI Conference 1996 Conference Paper

Using the Davis and Putnam Procedure for an Efficient Computation of Preferred Models

• Thierry Castell
• Claudette Cayrol
• Michel Cayrol
• Daniel Le Berre