Model counting (#SAT) is a fundamental yet #P-complete problem central to probabilistic reasoning. In this work, we address incremental model counting, where sequences of structurally similar formulas must be counted. We propose an approach that amortizes computation via a persistent caching mechanism, retaining component data across solver calls to avoid redundant search. Additionally, we investigate branching heuristics adapted for this setting. We focus on the problems of argumentation and soft core, for which incremental model counting is natural. Experiments demonstrate that our method improves performance compared to current model counters, highlighting the capability of structure-aware reuse in dynamic environments.

Knowledge Compilation (KC) is a powerful paradigm that enables efficient reasoning by transforming propositional formulas into tractable target languages, such as Deterministic, Decomposable Negation Normal Form (d-DNNF). However, as real-world problem instances grow in complexity, the offline compilation phase becomes a significant computational bottleneck, often exceeding the memory and temporal limits of single-node systems. While distributed computing has been successfully applied to model counting (#SAT), extending these techniques to knowledge compilation remains a challenge due to the difficulty of sharing partial circuit fragments across distributed nodes. In this paper, we propose dkc, the first distributed knowledge compiler designed for large-scale Decision-DNNF generation.Leveraging a Cube-and-Conquer strategy, dkc effectively partitions the search space into independent subproblems, mitigating the communication overhead typically associated with work-stealing architectures in circuit-based tasks. Recognizing that the utility of compilation lies in subsequent querying, we further introduce dreasoner, a distributed reasoning engine. dreasoner is capable of performing core inference tasks (including model counting, direct access, and uniform sampling) across a distributed d-DNNF structure, even under variable conditioning. Our experimental evaluation on benchmarks demonstrates that our distributed architecture scales effectively, enabling the compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers.

Industrial automated reasoning demands the rapid, repeated extraction of insights from complex formulas. Knowledge compilation into the Deterministic Decomposable Negation Normal Form (d-DNNF) addresses this by reducing natively intractable tasks to polynomial-time operations. We present decdnnf_rs, a performant framework for executing advanced reasoning queries directly on d-DNNF circuits. The library provides unified support for Satisfiability, Model Counting, Disjoint Model Enumeration, Direct Access, and Uniform Sampling. Crucially, decdnnf_rs handles dynamic contexts through implicit conditioning via weight propagation, avoiding the computational overhead of explicit graph modification. It also incorporates dynamic smoothness tracking to maintain a compact memory footprint. Bridging theoretical advancements with robust software engineering, decdnnf_rs offers an optimized toolset for exact and stochastic reasoning.

Boolean circuits in d-DNNF (determinstic Decomposable Negation Normal Form) enable tractable probabilistic inference, motivating research into compilers that transform arbitrary Boolean circuit into this form. However, d-DNNF compilers commonly require the input to be in conjunctive normal form (CNF), which means that a user must first convert their Boolean circuit into CNF. In this work, we argue that d-DNNF compilation would substantially benefit from reasoning over the original input circuit's structure, rather than solely relying on its CNF representation. To this end, we adapt an existing compiler and implement an optimisation that becomes more readily available once we reason over the input circuit: the identification and elimination of don't care variables. We empirically demonstrate the effectiveness of this approach, achieving a significant improvement in both the number of solved instances and the size of the resulting circuits.

Assumption-Based Argumentation (ABA) is a prominent formalism for structured argumentation, widely applied in domains such as healthcare, law, and robotics. Despite its inherent computational complexity, ABA has seen the development of effective techniques that successfully address key tasks, including evaluating the acceptability of literals and computing framework extensions. These approaches typically involve translating the initial ABA framework into an intermediate formalism, such as an Answer Set Program or an Abstract Argumentation Framework, which is then encoded into a Boolean satisfiability (SAT) problem. However, this translation can lead to large and complex intermediate representations, posing challenges for state-of-the-art SAT solvers. In this work, we propose a Counterexample-Guided Abstraction Refinement (CEGAR) approach that bypasses the initial translation step, at the cost of incrementally discovering certain ABA constraints that are not explicitly captured in the initial SAT encoding. We analyze the performance of our method and demonstrate that it outperforms state-of-the-art approaches on specific problem classes, while remaining competitive with the best existing solvers more broadly.

Model counting (also known as #SAT) is a fundamental problem in knowledge representation and reasoning, with applications ranging from probabilistic inference to formal verification. However, state-of-the-art model counters are limited by computational resources on a single machine. In this paper, we propose a novel distributed framework for model counting, exploiting the embarrassingly parallel nature of the problem. By decomposing the search space into independent subproblems and distributing them across different computation nodes, our approach achieves near-linear scalability on practical instances. Extensive experiments on standard benchmarks demonstrate both the effectiveness and efficiency of our framework.

Formal explainability is an emerging field that aims to provide mathematically guaranteed explanations for the predictions made by machine learning models. Recent work in this area focuses on computing “probabilistic explanations” for the predictions made by classifiers based on specific data instances. The goal of this paper is to extend the concept of probabilistic explanations to the regression setting, treating the target regressor as a black box function. The class of probabilistic explanations consists of linear functions that meet a sparsity constraint, alongside a hyperplane constraint defined for the data instance being explained. While minimizing the precision error of such explanations is generally $\text{NP}^{\text{PP}}$-hard, we demonstrate that it can be approximated by substituting the precision measure with a fidelity measure. Optimal explanations based on this fidelity objective can be effectively approached using Mixed Integer Programming (MIP). Moreover, we show that for certain distributions used to define the precision measure, explanations with approximation guarantees can be computed in polynomial time using a variant of Iterative Hard Thresholding (IHT). Experiments conducted on various datasets indicate that both the MIP and IHT approaches outperform the state-of-the-art LIME and MAPLE explainers.

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.

The All-Solution Satisfiability Problem (AllSAT) extends SAT by requiring the identification of all possible solutions for a propositional formula. In practice, enumerating all complete models is often infeasible, making the identification of partial models essential for generating a concise representation of the solution set. Deterministic Decomposable Negation Normal Form (d-DNNF) serves as a language for representation known to offer polynomial-time algorithms for model enumeration. Specifically, when a propositional formula is encoded in d-DNNF, it enables iterative model enumeration with polynomial delay between models. However, despite the existence of theoretical algorithms for this purpose, no available implementations are currently accessible. Furthermore, these theoretical approaches are nearly impractical as they solely yield complete models. We introduce a novel algorithm that maintains a polynomial delay between partial models while significantly enhancing efficiency compared to baseline approaches. Furthermore, through experimental validation, we demonstrate the superiority of compiling a CNF formula Σ into a d-DNNF formula Σ′ and subsequently enumerating models of Σ′ over existing state-of-the-art methodologies for CNF partial model enumeration.

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X . Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.

Boosted trees is a dominant ML model, exhibiting high accuracy. However, boosted trees are hardly intelligible, and this is a problem whenever they are used in safety-critical applications. Indeed, in such a context, provably sound explanations for the predictions made are expected. Recent work have shown how subset-minimal abductive explanations can be derived for boosted trees, using automated reasoning techniques. However, the generation of such well-founded explanations is intractable in the general case. To improve the scalability of their generation, we introduce the notion of tree-specific explanation for a boosted tree. We show that tree-specific explanations are provably sound abductive explanations that can be computed in polynomial time. We also explain how to derive a subset-minimal abductive explanation from a tree-specific explanation. Experiments on various datasets show the computational benefits of leveraging tree-specific explanations for deriving subset-minimal abductive explanations.

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.

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.

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 minimum-sized 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.

International audience

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.

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.

Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SAT-solvers, this level of exigence has not yet percolated for tools solving more complex tasks, such as model counting or knowledge compilation. In this paper, the focus is laid on a general family of top-down Decision-DNNF compilers. We explain how those compilers can be tweaked so as to output certifiable Decision-DNNF circuits, which are mainly standard Decision-DNNF circuits decorated by annotations serving as certificates. We describe a polynomial-time checker for testing whether a given CNF formula is equivalent or not to a given certifiable Decision-DNNF circuit. Finally, leveraging a modified version of the compiler d4 for generating certifiable Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are in practice certifiable Decision-DNNF circuits, and how much time is needed to compute and to check such circuits.

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.

Iterated belief change aims to determine how the belief state of a rational agent evolves given a sequence of change formulae. Several families of iterated belief change operators (revision operators, improvement operators) have been pointed out so far, and characterized from an axiomatic point of view. This paper focuses on the inference problem for iterated belief change, when belief states are represented as a special kind of stratified belief bases. The computational complexity of the inference problem is identified and shown to be identical for all revision operators satisfying Darwiche and Pearl's (R*1-R*6) postulates. In addition, some complexity bounds for the inference problem are provided for the family of soft improvement operators. We also show that a revised belief state can be computed in a reasonable time for large-sized instances using SAT-based algorithms, and we report empirical results showing the feasibility of iterated belief change for bases of significant sizes.

NACRE, for Nogood And Clause Reasoning Engine, is a constraint solver written in C++. It is based on a modular architecture designed to work with generic constraints while implementing several state-of-the-art search methods and heuristics. Interestingly, its data structures have been carefully designed to play around nogoods and clauses, making it suit- able for implementing learning strategies. NACRE was submitted to the CSP MiniTrack of the 2018 and 2019 XCSP3 [8] competitions where it took the first place. This paper gives a general description of NACRE as a framework. We present its kernel, the available search algorithms, and the default settings (notably, used for XCSP3 competitions), which makes NACRE efficient in practice when used as a black-box solver.

We present a recursive algorithm for projected model counting, i.e., the problem consisting in determining the number of models k∃X.Σk of a propositional formula Σ after eliminating from it a given set X of variables. Based on a ”standard” model counter, our algorithm projMC takes advantage of a disjunctive decomposition scheme of ∃X.Σ for computing k∃X.Σk. It also looks for disjoint components in its input for improving the computation. Our experiments show that in many cases projMC is significantly more efficient than the previous algorithms for projected model counting from the literature.

We consider the problem of identifying the change formula in a belief revision scenario: given that an unknown announcement (a formula mu) led a set of agents to revise their beliefs and given the prior beliefs and the revised beliefs of the agents, what can be said about mu? We show that under weak conditions about the rationality of the revision operators used by the agents, the set of candidate formulae has the form of a logical interval. We explain how the bounds of this interval can be tightened when the revision operators used by the agents are known and/or when mu is known to be independent from a given set of variables. We also investigate the completeness issue, i.e., whether mu can be exactly identified. We present some sufficient conditions for it, identify its computational complexity, and report the results of some experiments about it.

The enumeration of all Maximal Satisfiable Subsets (MSSes) or all Minimal Correction Subsets (MCSes) of an unsatisfiable CNF Boolean formula is a useful and sometimes necessary step for solving a variety of important A.I. issues. Although the number of different MCSes of a CNF Boolean formula is exponential in the worst case, it remains low in many practical situations; this makes the tentative enumeration possibly successful in these latter cases. In the paper, a technique is introduced that boosts the currently most efficient practical approaches to enumerate MCSes. It implements a model rotation paradigm that allows the set of MCSes to be computed in an heuristically efficient way.

We present and evaluate DMC, a distributed model counter for propositional CNF formulae based on the state-of-the-art sequential model counter D4. DMC can take advantage of a (possibly large) number of sequential model counters running on (possibly heterogeneous) computing units spread over a network of computers. For ensuring an efficient workload distribution, the model counting task is shared between the model counters following a policy close to work stealing. The number and the sizes of the messages which are exchanged by the jobs are kept small. The results obtained show DMC as a much more efficient counter than D4, the distribution of the computation yielding large improvements for some benchmarks. DMC appears also as a serious challenger to the parallel model counter CountAntom and to the distributed model counter dCountAntom.

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 phi can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5-satisfiability 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 SAT-based 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 phi and to evaluate the effect of our caching technique. We also compared our solver againstexisting 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)

We present SAT encoding schemes for distance-based belief merging operators relying on the (possibly weighted) drastic distance or the Hamming distance between interpretations, and using sum, GMax (leximax) or GMin (leximin) as aggregation function. In order to evaluate these encoding schemes, we generated benchmarks of a time-tabling problem and translated them into belief merging instances. Then, taking advantage of these schemes, we compiled the merged bases of the resulting instances into query-equivalent CNF formulae. Experiments have shown the benefits which can be gained by considering the SAT encoding schemes we pointed out. Especially, thanks to them, we succeeded in computing query-equivalent formulae for merging instances based on hundreds of variables, which are out of reach of previous implementations.

The search for one consensus that reconciles several conflicting agents or information sources is a key paradigm in both everyday-life and A.I. In this paper, we improve a recent approach to consensus-finding that has been developed in the Boolean logic framework. In that recent approach consensuses are defined as being some specific non-conflicting fragments of the set-theoretic union of all the information to be mitigated. In order to be a consensus, such a fragment must be conflict-free with every information source, taken individually. That approach has also introduced a generic method to compute one consensus that obeys various possible maximality criteria, including maximality with respect to set-theoretical inclusion, i.e., max⊆ consensuses. As max⊆ consensuses are of clear interest, the focus is on their computation in this paper. We develop an algorithm for computing one max⊆ consensus that is experimentally more time and space efficient than the computational method proposed in the initial study.

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.

We present and evaluate a new compiler, called d4, targeting the Decision-DNNF language. As the state-of-the-art compilers C2D and Dsharp targeting the same language, d4 is a top-down tree-search algorithm exploring the space of propositional interpretations. d4 is based on the same ingredients as those considered in C2D and Dsharp (mainly, disjoint component analysis, conflict analysis and non-chronological backtracking, component caching). d4 takes advantage of a dynamic decomposition approach based on hypergraph partitioning, used sparingly. Some simplification rules are also used to minimize the time spent in the partitioning steps and to promote the quality of the decompositions. Experiments show that the compilation times and the sizes of the Decision-DNNF representations computed by d4 are in many cases significantly lower than the ones obtained by C2D and Dsharp.

The efficient extraction of one maximal information subset that does not conflict with multiple contxts or additional information sources is a key basic issue in many A.I. domains, especially when these contexts or sources can be mutually conflicting. In this paper, this question is addressed from a computational point of view in clausal Boolean logic. A new approach is introduced that experimentally outperforms the currently most efficient technique.

We present and evaluate a new CNF encoding scheme for reducing probabilistic inference from a graphical model to weighted model counting. This new encoding scheme elaborates on the CNF encoding scheme ENC4 introduced by Chavira and Darwiche, and improves it by taking advantage of log encodings of the elementary variable/value assignments and of the implicit encoding of the most frequent probability value per conditional probability table. From the theory side, we show that our encoding scheme is faithful, and that for each input network, the CNF formula it leads to contains less variables and less clauses than the CNF formula obtained using ENC4. From the practical side, we show that the C2D compiler empowered by our encoding scheme performs in many cases significantly better than when ENC4 is used, or when the state-of-the-art ACE compiler is considered instead.

Consensus-finding plays a ubiquitous role in A.I. In this paper, a consensus among agents is defined as a non-contradictory fragment of all the information conveyed by the agents such that this fragment does not logically conflict with any of the agents. This concept is investigated in modal logic S5 in order to meet representation needs that are put in light by this concept of consensus itself. Interestingly, an optimization-based approach to compute maximal consensuses is developed and shown experimentally efficient very often for both the standard Boolean and S5 frameworks.

An original method for the extraction of one maximal subset of a set of Boolean clauses that must be satisfiable with possibly mutually contradictory assumptive contexts is motivated and experimented. Noticeably, it performs a direct computation and avoids the enumeration of all subsets that are satisfiable with at least one of the contexts. The method applies for subsets that are maximal with respect to inclusion or cardinality.

Nowadays, argumentation is a salient keyword in artificial intelligence. The use of argumentation techniques is particularly convenient for thematics such that multiagent systems, where it allows to describe dialog protocols (using persuasion, negotiation, ...) or on-line discussion analysis, it also allows to handle queries where a single agent has to reason with conflicting information (inference in the presence of inconsistency, inconsistency measure). This very rich framework gives numerous reasoning tools, thanks to several acceptability semantics and inference policies. On the other hand, the progress of SAT solvers in the recent years, and more generally the progress on Constraint Programming paradigms, lead to some powerful approaches that permit to tackle theoretically hard problems. The needs of efficient applications to solve the usual reasoning tasks in argumentation, together with the capabilities of modern Constraint Programming solvers, lead us to study the encoding of usual acceptability semantics into logical settings. We propose diverse use of Constraint Programming techniques to develop a software library dedicated to argumentative reasoning. We present a library which offers the advantages to be generic and easily adaptable. We finally describe an experimental study of our approach for a set of semantics and inference tasks, and we describe the behaviour of our solver during the First International Competition on Computational Models of Argumentation.

The concepts of MSS (Maximal Satisfiable Subset) andCoMSS (also called Minimal Correction Subset) playa key role in many A.I. approaches and techniques. Inthis paper, a novel algorithm for partitioning a BooleanCNF formula into one MSS and the correspondingCoMSS is introduced. Extensive empirical evaluationshows that it is more robust and more efficient on mostinstances than currently available techniques.

This paper is concerned with preprocessing techniques for propositional model counting. We have implemented a preprocessor which includes many elementary preprocessing techniques, including occurrence reduction, vivification, backbone identification, as well as equivalence, AND and XOR gate identification and replacement. We performed intensive experiments, using a huge number of benchmarks coming from a large number of families. Two approaches to model counting have been considered downstream: ”direct” model counting using Cachet and compilation-based model counting, based on the C2D compiler. The experimental results we have obtained show that our preprocessor is both efficient and robust.

In this paper, symmetries are exploited for achieving significant space savings in a knowledge compilation perspective. More precisely, the languages FBDD and DDG of decision diagrams are extended to the languages Sym-FBDDX,Yand Sym-DDGX,Yof symmetry-driven decision diagrams, where X is a set of “symmetry-free” variables and Y is a set of “top” variables. Both the time efficiency and the space efficiency of Sym-FBDDX,Yand Sym-DDGX,Yare analyzed, in order to put those languages in the knowledge compilation map for propositional representations. It turns out that each of Sym-FBDDX,Yand Sym-DDGX,Ysatisfies CT (the model counting query). We prove that no propositional language over a set X∪Y of variables, satisfying both CO (the consistency query) and CD (the conditioning transformation), is at least as succinct as any of Sym-FBDDX,Yand Sym-DDGX,Yunless the polynomial hierarchy collapses. The price to be paid is that only a restricted form of conditioning and a restricted form of forgetting are offered by Sym-FBDDX,Yand Sym-DDGX,Y. Nevertheless, this proves sufficient for a number of applications, including configuration and planning. We describe a compiler targeting Sym-FBDDX,Yand Sym-DDGX,Yand give some experimental results on planning domains, highlighting the practical significance of these languages.

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.

An original encoding of multiple contraction in Boolean logic through Partial-Max-SAT is proposed. Multiple contraction of a set of clauses Δ by a set of formulas Γ delivers one maximum cardinality subset of Δ from which no formula of Γ can be deduced. Equivalently, multiple contraction can be defined as the extraction of one maximum cardinality subset of Δ that is satisfiable together with a given set of formulas. Noticeably, the encoding schema allows multiple contraction to be computed through a number of calls to a SAT solver that is bound by the number of formulas in Γ and one call to Partial-Max-SAT. On the contrary, in the worst case, a direct approach requires us to compute for each formula γ in Γ all inclusion-maximal subsets of Δ that do not entail γ. Extensive experimental results show that the encoding allows multiple contraction to be computed in a way that is practically viable in many cases and outperforms the direct approach.

When a constraint network is unsatisfiable, it can be of prime importance to provide the network designer with a full-fledged explanation of what causes the absence of any solution to the network. In this respect, minimal unsatisfiable cores (in short, MUCs) form the basis for such an explanation. Efficient MUC extractors are often made of an initial incomplete minimization step that delivers an upper-approximation of a MUC, followed by a refinement step. The first step is assumed crucial for the performance of the whole approach. In this paper, its actual importance is investigated. Especially, it is shown that the first step can be skipped when the refinement process dynamically exploits the information that this latter treatment itself entails.

This paper is concerned with a form of relaxation of constraint networks. The focus is on situations where additional constraints are intended to extend a non-empty set of preexisting solutions. These constraints require a specific treatment since merely inserting them inside the network would lead to their preemption by more restrictive ones. Several approaches to handle these additional constraints are investigated from conceptual and experimental points of view.

In this paper, a new heuristic for polarity selection is proposed. This heuristic is defined for parallel SAT solvers. The selected polarity is an important component of modern SAT solvers, in particular in portfolio ones. Indeed, these solvers are often based on the cooperation/competition principle. In this case, the polarity can be used to guide the solver in the search space. A criterion based on the intention notion is proposed in order to evaluate whether two solvers are to study the same search space or not. Once this criterion defined, a dynamical heuristic polarity is proposed for tuning the different solvers. Experimental results show that our approach is efficient and provides significant improvements on a range of industrial instances.

In this paper a learning based local search approach for propositional satisfiability is presented. It is based on an original adaptation of the conflict driven clause learning (CDCL) scheme to local search. First an extended implication graph for complete assignments of the set of variables is proposed. Secondly, a unit propagation based technique for building and using such implication graph is designed. Finally, we show how this new learning scheme can be integrated to the state-of-the-art local search solver WSAT. Interestingly enough, the obtained local search approach is able to prove unsatisfiability. Experimental results show very good performances on many classes of SAT instances from the last SAT competitions.