Gilles Audemard

IJCAI Conference 2024 Conference Paper

Deriving Provably Correct Explanations for Decision Trees: The Impact of Domain Theories

• Gilles Audemard
• Jean-Marie Lagniez
• Pierre Marquis
• Nicolas Szczepanski

We are interested in identifying the complexity of computing local explanations of various types given a decision tree, when the Boolean conditions used in the tree are not independent. This is usually the case when decision trees are learned from instances described using numerical or categorical attributes. In such a case, considering the domain theory indicating how the Boolean conditions occurring in the tree are logically connected is paramount to derive provably correct explanations. However, the nature of the domain theory may have a strong impact on the complexity of generating explanations. In this paper, we identify the complexity of deriving local explanations (abductive or contrastive) given a decision tree in the general case, and under several natural restrictions about the domain theory.

ECAI Conference 2024 Conference Paper

Designing an XAI Interface for Tree-Based ML Models

• Gilles Audemard
• Sylvie Coste-Marquis
• Pierre Marquis
• Mehdi Sabiri
• Nicolas Szczepanski

We present and evaluate empirically an XAI protocol for ruling interactions between a tree-based ML model (the AI system) and its user U, in the context of a prediction task. The pieces of knowledge held by U concerning the prediction task are supposed to be representable by a set of classification rules that is reliable and consistent, but (typically) incomplete. The proposed protocol aims to help U decide what to do with each prediction made by AI (accept it, reject it). It also aims to improve the quality of further predictions made by AI thanks to the expertise of U, and, reciprocally, to complete the pieces of knowledge held by U by leveraging the predictions made by AI. Experiments show that the approach can prove valuable in practice.

ECAI Conference 2024 Conference Paper

On the Computation of Contrastive Explanations for Boosted Regression Trees

• Gilles Audemard
• Jean-Marie Lagniez
• Pierre Marquis

A contrastive explanation is a local explanation that is looked for when the prediction achieved by an ML model on an input instance x differs from what was foreseen. A contrastive explanation indicates how to change x to another instance xc from which a prediction that complies with the user’s expectations can be obtained. In this paper, we present a constraint-based approach to the generation of contrastive explanations that are suited to regression functions represented by boosted trees. We show how to compute the smallest interval containing all the regression values that are attainable given a set of characteristics of x that are protected (i. e. , not amenable to change). We also show how to generate minimal contrastive explanations for x given a target interval, i. e. , instances with regression values within the specified interval and that are as close as possible to x. Closeness is captured using user-dependent mappings reflecting preferences about value change for the attributes (or combinations of attributes) considered in the representation of x.

IJCAI Conference 2024 Conference Paper

On the Computation of Example-Based Abductive Explanations for Random Forests

• Gilles Audemard
• Jean-Marie Lagniez
• Pierre Marquis
• Nicolas Szczepanski

We show how to define and compute example-based abductive explanations. Such explanations are guaranteed to be 100% correct, fairly general, and persuasive enough since they cover sufficiently many reference instances furnished by the explainee. We prove that the latter coverage condition yields a complexity shift to the second level of the polynomial hierarchy. We present a CEGAR-based algorithm to derive such explanations, and show how to modify it to derive most anchored example-based abductive explanations, i. e. , example-based abductive explanations that cover as many reference instances as possible. We also explain how to reduce example-based abductive explanations to get subset-minimal explanations. Experiments in the case of random forest classifiers show that our CEGAR-based algorithm is quite efficient in practice.

IJCAI Conference 2024 Conference Paper

PyXAI: An XAI Library for Tree-Based Models

• Gilles Audemard
• Jean-Marie Lagniez
• Pierre Marquis
• Nicolas Szczepanski

PyXAI (Python eXplainable AI) is a Python library designed for providing explanations and cor- recting tree-based Machine Learning (ML) models. It is suited to decision trees, random forests, and boosted trees, when used for regression or classification tasks. In contrast to many model-agnostic approaches to XAI, PyXAI exploits the model it- self to generate explanations, ensuring them to be faithful. PyXAI includes several algorithms for the generation of explanations, which can be abductive or contrastive. PyXAI also includes algorithms for correcting tree-based models when their predictions conflict with pieces of user knowledge.

IJCAI Conference 2023 Conference Paper

Computing Abductive Explanations for Boosted Regression Trees

• Gilles Audemard
• Steve Bellart
• Jean-Marie Lagniez
• Pierre Marquis

We present two algorithms for generating (resp. evaluating) abductive explanations for boosted regression trees. Given an instance x and an interval I containing its value F (x) for the boosted regression tree F at hand, the generation algorithm returns a (most general) term t over the Boolean conditions in F such that every instance x′ satisfying t is such that F (x′ ) ∈ I. The evaluation algorithm tackles the corresponding inverse problem: given F, x and a term t over the Boolean conditions in F such that t covers x, find the least interval I_t such that for every instance x′ covered by t we have F (x′ ) ∈ I_t. Experiments on various datasets show that the two algorithms are practical enough to be used for generating (resp. evaluating) abductive explanations for boosted regression trees based on a large number of Boolean conditions.

ECAI Conference 2023 Conference Paper

On Contrastive Explanations for Tree-Based Classifiers

• Gilles Audemard
• Jean-Marie Lagniez
• Pierre Marquis
• Nicolas Szczepanski

We define contrastive explanations that are suited to tree-based classifiers. In our framework, contrastive explanations are based on the set of (possibly non-independent) Boolean characteristics used by the classifier and are at least as general as contrastive explanations based on the set of characteristics of the instances considered at start. We investigate the computational complexity of computing contrastive explanations for Boolean classifiers (including tree-based ones), when the Boolean conditions used are not independent. Finally, we present and evaluate empirically an algorithm for computing minimum-size contrastive explanations for random forests.

SAT Conference 2022 Conference Paper

A New Exact Solver for (Weighted) Max#SAT

• Gilles Audemard
• Jean-Marie Lagniez
• Marie Miceli

We present and evaluate d4Max, an exact approach for solving the Weighted Max#SAT problem. The Max#SAT problem extends the model counting problem (#SAT) by considering a tripartition of the variables {X, Y, Z}, and consists in maximizing over X the number of assignments to Y that can be extended to a solution with some assignment to Z. The Weighted Max#SAT problem is an extension of the Max#SAT problem with weights associated on each interpretation. We test and compare our approach with other state-of-the-art solvers on the challenging task in probabilistic inference of finding the marginal maximum a posteriori probability (MMAP) of a given subset of the variables in a Bayesian network and on exist-random quantified SSAT benchmarks. The results clearly show the overall superiority of d4Max in term of speed and number of instances solved. Moreover, we experimentally show that, in general, d4Max is able to quickly spot a solution that is close to optimal, thereby opening the door to an efficient anytime approach.

IJCAI Conference 2022 Conference Paper

On Preferred Abductive Explanations for Decision Trees and Random Forests

• Gilles Audemard
• Steve Bellart
• Louenas Bounia
• Frederic Koriche
• Jean-Marie Lagniez
• Pierre Marquis

Abductive explanations take a central place in eXplainable Artificial Intelligence (XAI) by clarifying with few features the way data instances are classified. However, instances may have exponentially many minimum-size abductive explanations, and this source of complexity holds even for ``intelligible'' classifiers, such as decision trees. When the number of such abductive explanations is huge, computing one of them, only, is often not informative enough. Especially, better explanations than the one that is derived may exist. As a way to circumvent this issue, we propose to leverage a model of the explainee, making precise her / his preferences about explanations, and to compute only preferred explanations. In this paper, several models are pointed out and discussed. For each model, we present and evaluate an algorithm for computing preferred majoritary reasons, where majoritary reasons are specific abductive explanations suited to random forests. We show that in practice the preferred majoritary reasons for an instance can be far less numerous than its majoritary reasons.

AAAI Conference 2022 Conference Paper

Trading Complexity for Sparsity in Random Forest Explanations

• Gilles Audemard
• Steve Bellart
• Louènas Bounia
• Frédéric Koriche
• Jean-Marie Lagniez
• Pierre Marquis

Random forests have long been considered as powerful model ensembles in machine learning. By training multiple decision trees, whose diversity is fostered through data and feature subsampling, the resulting random forest can lead to more stable and reliable predictions than a single decision tree. This however comes at the cost of decreased interpretability: while decision trees are often easily interpretable, the predictions made by random forests are much more difficult to understand, as they involve a majority vote over multiple decision trees. In this paper, we examine different types of reasons that explain “why” an input instance is classified as positive or negative by a Boolean random forest. Notably, as an alternative to prime-implicant explanations taking the form of subset-minimal implicants of the random forest, we introduce majoritary reasons which are subset-minimal implicants of a strict majority of decision trees. For these abductive explanations, the tractability of the generation problem (finding one reason) and the optimization problem (finding one minimumsized reason) are investigated. Unlike prime-implicant explanations, majoritary reasons may contain redundant features. However, in practice, prime-implicant explanations for which the identification problem is DP-complete - are slightly larger than majoritary reasons that can be generated using a simple linear-time greedy algorithm. They are also significantly larger than minimum-sized majoritary reasons which can be approached using an anytime PARTIAL MAXSAT algorithm.

KR Conference 2021 Conference Paper

On the Computational Intelligibility of Boolean Classifiers

• Gilles Audemard
• Steve Bellart
• Louenas Bounia
• Frédéric Koriche
• Jean-Marie Lagniez
• Pierre Marquis

In this paper, we investigate the computational intelligibility of Boolean classifiers, characterized by their ability to answer XAI queries in polynomial time. The classifiers under consideration are decision trees, DNF formulae, decision lists, decision rules, tree ensembles, and Boolean neural nets. Using 9 XAI queries, including both explanation queries and verification queries, we show the existence of large intelligibility gap between the families of classifiers. On the one hand, all the 9 XAI queries are tractable for decision trees. On the other hand, none of them is tractable for DNF formulae, decision lists, random forests, boosted decision trees, Boolean multilayer perceptrons, and binarized neural networks.

KR Conference 2020 Conference Paper

On Tractable XAI Queries based on Compiled Representations

• Gilles Audemard
• Frédéric Koriche
• Pierre Marquis

One of the key purposes of eXplainable AI (XAI) is to develop techniques for understanding predictions made by Machine Learning (ML) models and for assessing how much reliable they are. Several encoding schemas have recently been pointed out, showing how ML classifiers of various types can be mapped to Boolean circuits exhibiting the same input-output behaviours. Thanks to such mappings, XAI queries about classifiers can be delegated to the corresponding circuits. In this paper, we define new explanation and/or verification queries about classifiers. We show how they can be addressed by combining queries and transformations about the associated Boolean circuits. Taking advantage of previous results from the knowledge compilation map, this allows us to identify a number of XAI queries that are tractable provided that the circuit has been first turned into a compiled representation.

SAT Conference 2020 Conference Paper

SAT Heritage: A Community-Driven Effort for Archiving, Building and Running More Than Thousand SAT Solvers

• Gilles Audemard
• Loïc Paulevé
• Laurent Simon 0001

Abstract SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. Moreover, there has been more than a thousand solvers published so far, some of them released in the early 90’s. If the SAT community wants to archive and be able to keep track of all the solvers that made its history, it urgently needs to deploy an important effort. We propose to initiate a community-driven effort to archive and to allow easy compilation and running of all SAT solvers that have been released so far. We rely on the best tools for archiving and building binaries (thanks to Docker, GitHub and Zenodo) and provide a consistent and easy way for this. Thanks to our tool, building (or running) a solver from its source (or from its binary) can be done in one line.

ECAI Conference 2020 Conference Paper

Segmented Tables: An Efficient Modeling Tool for Constraint Reasoning

• Gilles Audemard
• Christophe Lecoutre
• Mehdi Maamar

These last years, there has been a growing interest for structures like tables and decision diagrams in Constraint Programming (CP). This is due to the universal character of these structures, enabling the representation of any (group of) constraints under extensional form, and to the efficient filtering algorithms developed for constraints based on (ordinary/short/compressed/smart) tables and multi-valued decision diagrams. In this paper, we propose the concept of segmented tables where entries can combine ordinary values, universal values (*) and sub-tables. Segmented tables can be seen as a generalization of compressed tables. We propose an algorithm enforcing Generalized Arc Consistency (GAC) on segmented table constraints, and show their modeling and practical interests on a realistic problem.

SAT Conference 2017 Conference Paper

A Distributed Version of Syrup

• Gilles Audemard
• Jean-Marie Lagniez
• Nicolas Szczepanski
• Sébastien Tabary

Abstract A portfolio SAT solver has to share clauses in order to be efficient. In a distributed environment, such sharing implies additional problems: more information has to be exchanged and communications among solvers can be time consuming. In this paper, we propose a new version of the state-of-the-art SAT solver Syrup that is now able to run on distributed architectures. We analyze and compare different programming models of communication. We show that, using a dedicated approach, it is possible to share many clauses without penalizing the solvers. Experiments conducted on SAT 2016 benchmarks with up to 256 cores show that our solver is very effective and outperforms other approaches. This opens a broad range of possibilities to boost parallel solvers needing to share many data.

SAT Conference 2016 Conference Paper

Extreme Cases in SAT Problems

• Gilles Audemard
• Laurent Simon 0001

Abstract With the increasing performance of SAT solvers, a lot of distinct problems, coming from very disparate fields, are added to the pool of Application problems, regularly used to rank solvers. These problems are also widely used to measure the positive impact of any new idea. We show in this paper that many of them have extreme behaviors that any SAT solvers must cope with. We show that, by adding a few, simple, human-readable, indicators, we can let Glucose choose between four strategies to show important improvements on the set of the hardest problems from all the competitions between 2002 and 2013 included. Moreover, once the SAT solver has been specialized, we show that a new restart polarity policy can improve even more the results. Without the first specialization step mentioned above, this new and effective policy would have been jugged inefficient. Our final Glucose is capable of solving \(20\, \%\) more problems than the original one, while speeding up also UNSAT answers.

SAT Conference 2014 Conference Paper

Impact of Community Structure on SAT Solver Performance

• Zack Newsham
• Vijay Ganesh 0001
• Sebastian Fischmeister
• Gilles Audemard
• Laurent Simon 0001

Abstract Modern CDCL SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. It is clear that these solvers somehow exploit the structure of real-world instances. However, to-date there have been few results that precisely characterise this structure. In this paper, we provide evidence that the community structure of real-world SAT instances is correlated with the running time of CDCL SAT solvers. It has been known for some time that real-world SAT instances, viewed as graphs, have natural communities in them. A community is a sub-graph of the graph of a SAT instance, such that this sub-graph has more internal edges than outgoing to the rest of the graph. The community structure of a graph is often characterised by a quality metric called Q. Intuitively, a graph with high-quality community structure (high Q) is easily separable into smaller communities, while the one with low Q is not. We provide three results based on empirical data which show that community structure of real-world industrial instances is a better predictor of the running time of CDCL solvers than other commonly considered factors such as variables and clauses. First, we show that there is a strong correlation between the Q value and Literal Block Distance metric of quality of conflict clauses used in clause-deletion policies in Glucose-like solvers. Second, using regression analysis, we show that the the number of communities and the Q value of the graph of real-world SAT instances is more predictive of the running time of CDCL solvers than traditional metrics like number of variables or clauses. Finally, we show that randomly-generated SAT instances with 0. 05 ≤ Q ≤ 0. 13 are dramatically harder to solve for CDCL solvers than otherwise.

SAT Conference 2014 Conference Paper

Lazy Clause Exchange Policy for Parallel SAT Solvers

• Gilles Audemard
• Laurent Simon 0001

Abstract Managing learnt clauses among a parallel, memory shared, SAT solver is a crucial but difficult task. Based on some statistical experiments made on learnt clauses, we propose a simple parallel version of Glucose that uses a lazy policy to exchange clauses between cores. This policy does not send a clause when it is learnt, but later, when it has a chance to be useful locally. We also propose a strategy for clauses importation that put them in ”probation” before a potential entry in the search, thus limiting the negative impact of high importation rates, both in terms of noise and decreasing propagation speed.

SAT Conference 2013 Conference Paper

Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction

• Gilles Audemard
• Jean-Marie Lagniez
• Laurent Simon 0001

Abstract Beside the important progresses observed in SAT solving, a number of applications explicitly rely on incremental SAT solving only. In this paper, we focus on refining the incremental SAT Solver Glucose, from the SAT engine perspective, and address a number of unseen problems this new use of SAT solvers opened. By playing on clause database cleaning, assumptions managements and other classical parameters, we show that our approach immediately and significantly improves an intensive assumption-based incremental SAT solving task: Minimal Unsatisfiable Set. We believe this work could bring immediate benefits in a number of other applications relying on incremental SAT.

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.

SAT Conference 2012 Conference Paper

Revisiting Clause Exchange in Parallel SAT Solving

• Gilles Audemard
• Benoît Hoessen
• Saïd Jabbour
• Jean-Marie Lagniez
• Cédric Piette

Abstract Managing learnt clause database is known to be a tricky task in SAT solvers. In the portfolio framework, the collaboration between threads through learnt clause exchange makes this problem even more difficult to tackle. Several techniques have been proposed in the last few years, but practical results are still in favor of very limited collaboration, or even no collaboration at all. This is mainly due to the difficulty that each thread has to manage a large amount of learnt clauses generated by the other workers. In this paper, we propose new efficient techniques for clause exchanges within a parallel SAT solver. In contrast to most of the current clause exchange methods, our approach relies on both export and import policies, and makes use of recent techniques that proves very effective in the sequential case. Extensive experimentations show the practical interest of the proposed ideas.

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.

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.

SAT Conference 2008 Conference Paper

A Generalized Framework for Conflict Analysis

• Gilles Audemard
• Lucas Bordeaux
• Youssef Hamadi
• Saïd Jabbour
• Lakhdar Saïs

Abstract This paper presents an extension of Conflict Driven Clauses Learning (CDCL). It relies on an extended notion of implication graph containing additional arcs, called inverse arcs. These are obtained by taking into account the satisfied clauses of the formula, which are usually ignored by conflict analysis. This extension captures more conveniently the whole propagation process, and opens new perspectives for CDCL-based approaches. Among other benefits, our extension leads to a new conflict analysis scheme that exploits the additional arcs to back-jump to higher levels. Experimental results show that the integration of our generalized conflict analysis scheme within two state-of-the-art solvers improves their performance.

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.

IJCAI Conference 2007 Conference Paper

• Gilles Audemard
• Sa
• iuml; d Jabbour
• Lakhdar Sa
• iuml; s

Many reasoning task and combinatorial problems exhibit symmetries. Exploiting such symmetries has been proved to be very important in reducing search efforts. Breaking symmetries using additional constraints is currently one of the most used approaches. Extending such symmetry breaking techniques to quantified boolean formulae (QBF) is a very challenging task. In this paper, an approach to break symmetries in quantified boolean formulae is proposed. It makes an original use of universally quantified auxiliary variables to generate new symmetry breaking predicates and a new ordering of the QBF prefix is then computed leading to a new equivalent QBF formula with respect to validity. Experimental evaluation of the state-of-the-art QBF solver semprop shows significant improvements (up to several orders of magnitude) on many QBFs instances.

SAT Conference 2007 Conference Paper

Circuit Based Encoding of CNF Formula

• Gilles Audemard
• Lakhdar Saïs

Abstract In this paper a new circuit SAT based encoding of boolean formula is proposed. It makes an original use of the concept of restrictive models introduced by Boufkhad to polynomially translate any formula in conjunctive normal form (CNF) to a circuit SAT representation (a conjunction of gates and clauses). Our proposed encoding preserves the satisfiability of the original formula. The set of models of the obtained circuit w. r. t. the original set of variables is a subset of the models (with special characteristics) of the original formula. We also provided a connection between our encoding and the satisfiability of the original formula i. e. when the input formula is satisfiable, our proposed translation delivers a full circuit formula. A new incremental preprocessing process is designed leading to interesting experimental improvements of the Minisat satisfiability solver.

SAT Conference 2005 Conference Paper

A Symbolic Search Based Approach for Quantified Boolean Formulas

• Gilles Audemard
• Lakhdar Saïs

Abstract Solving Quantified Boolean Formulas (QBF) has become an important and attractive research area, since several problem classes might be formulated efficiently as QBF instances (e. g. planning, non monotonic reasoning, two-player games, model checking, etc). Many QBF solvers has been proposed, most of them perform decision tree search using the DPLL-like techniques. To set free the variable ordering heuristics that are traditionally constrained by the static order of the QBF quantifiers, a new symbolic search based approach ( QBdd(Sat) ) is proposed. It makes an original use of binary decision diagram to represent the set of models (or prime implicants) of the boolean formula found using search-based satisfiability solver. Our approach is enhanced with two interesting extensions. First, powerful reduction operators are introduced in order to dynamically reduce the BDD size and to answer the validity of the QBF. Second, useful cuts are achieved on the search tree thanks to the nogoods generated from the BDD representation. Using DPLL-likes (resp. local search) techniques, our approach gives rise to a complete QBdd(DPLL) (resp. incomplete QBdd(LS) ) solver. Our preliminary experimental results show that on some classes of instances from the QBF evaluation, QBdd(DPLL) and QBdd(LS) are competitive with state-of-the-art QBF solvers.

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.