Reasoning About Inconsistent Formulas

1 Introduction

In a wide range of settings, one must reason about inconsistent formulas. This is the case for example when debugging inconsistent system specifications, e.g. for understanding which constraints make the system inconsistent. This is also the case in model-based diagnosis [Reiter, 1987], where the system representation is inconsistent with its expected input-output behavior. In turn, model-based diagnosis finds a number of significant applications, that include axiom pinpointing in description logics, software fault localization, type error debugging, spreadsheet debugging, or analysis of inconsistent knowledge bases, to name a few. Inconsistency is also often used when solving optimization problems, e.g. in

In this paper we focus on inconsistent formulas of monotonic logics, e.g. first-order logic and its fragments. However, there is also interest in non-monotonic logics [Brewka et al., 2019]. When analyzing inconsistent formulas, a number of computational problems arise. In some settings, one is interested in explaining one possible reason of inconsistency. In some other settings, the goal is to propose ways to correct the source of inconsistency. Finally, in yet some other settings, the purpose is to enumerate all explanations or corrections of an inconsistent formula.

The purpose of this paper is to provide an overview of recent work on reasoning about inconsistent formulas. The paper addresses the problems of explaining and correcting inconsistency, but also highlights enumeration of explanations and corrections, and briefly overviews how inconsistency is exploited when solving optimization problems. The paper also demonstrates that most of the algorithms proposed in recent years for reasoning about inconsistency, most of which originally devised in the context of analyzing propositional formulas, can be also be applied in any monotonic logic.

The paper is organized as follows. Section 2 introduces the definitions and notation used throughout the paper. Section 3 covers approaches for finding (or extracting) subset-minimal explanations and corrections. Section 4 overviews the relationship between reasoning about inconsistency and optimization problems. Section 5 highlights algorithms for the enumeration of both corrections and explanations. A sample of practical applications is briefly discussed in Section 6. Finally, the paper concludes in Section 7.

2 Preliminaries

Basic definitions. The paper assumes definitions standard for first-order logic (FOL) [Ben-Ari, 2012]. We will be interested in formulas expressed in some (decidable) fragment of FOL 1 , and so respecting monotonicity of entailment. For simplicity, we will not consider the use of function symbols, but that does not affect the results in the paper. Throughout, FOL formulas will be represented in clausal form and will most often be inconsistent. In general, we consider an inconsistent FOL formula F, such that some clauses in F can be relaxed (i.e. allowed not to be satisfied) to restore consistency, whereas others cannot. Thus, we assume that F is partitioned into two first-order subformulas F = B∪S, where S contains the relaxable (soft) clauses, and B contains the non-relaxable clauses. B can be viewed as background knowledge, which is assumed to be consistent and must always be satisfied.

The paper uses other standard notation. P ⊨Q denotes that any model of P is also a model of Q. As a result, P ⊨⊥ is used to denote that P is inconsistent, and P ⊭⊥ denotes that P is consistent. Set notation will be used to improve readability. For example, P ∪Q⊨R is used to denote ∧c∈P∪Qc ⊨R.

Generalizations from the propositional domain. This paper covers the analysis of inconsistent formulas in very generic terms, opting not to focus exclusively on propositional formulas. A number of concepts often used in the propositional domain can be easily generalized to different fragments of first-order logic. These will prove instrumental in showing how different algorithms, often described for propositional formulas, can in fact be generalized well beyond. A simple observation is that propositional variables can be viewed as predicate symbols. Thus, concepts such as reification of clauses, or constraints over propositional variables, can be used in more general settings. For example, pseudo-boolean constraints, including cardinality constraints, can be readily used in fragments of FOL. Furthermore, although QBF may seem to involve non-standard quantification (from a FOL perspective), there are well-known translations from QBF to EPR [Seidl et al., 2012], and so the proposed generalizations also extend to QBF.

1 As a result, the results presented in the paper apply in different settings, including SAT, ILP, CSP, QBF, SMT (specific theories), among others. Decidability is expected, since we will need to be able to answer decision problems both positively and negatively.

Subset-minimal explanations and corrections. Given an inconsistent clausal formula F, we are interested in identifying the clauses that are responsible for unsatisfiability among those that can be relaxed, as defined next.

Definition 1 (MUS). Let F = B∪S be an inconsistent set of clauses (F ⊨⊥). M ⊆ S is a Minimal Unsatisfiable Subset (MUS) iff B ∪M⊨⊥ and ∀M′⊊M, B ∪M′ ⊭⊥.

Informally, an MUS provides the minimal information that needs to be added to the background knowledge B to obtain inconsistency; thus, an MUS represents an explanation for the causes of inconsistency. Alternatively, one might be interested in correcting the formula, removing some clauses to achieve consistency.

Definition 2 (MCS). Let F = B ∪ S be an inconsistent set of clauses (F ⊨⊥). C ⊆ S is a Minimal Correction Subset (MCS) iff B ∪ S \ C ⊭⊥ and ∀C′⊊C, B ∪ S \ C ′ ⊨⊥.

With each MCS C, one associates a Maximal Satisfiable Subset (MSS), given by S \ C. Moreover, there exists a wellknown (subset-)minimal hitting set (MHS) relationship between MUSes and MCSes:

Proposition 1. MCSes are MHSes of MUSes and vice-versa.

The MHS relationship between MUSes and MCSes was first demonstrated in the context of model-based diagnosis [Reiter, 1987] and later investigated for propositional formulas in clausal form [Birnbaum and Lozinskii, 2003].

Recent years have witnessed the proposal of a large number of novel algorithms for the extraction and enumeration of MUSes and MCSes [Menc´ıa et al., 2015; Bacchus and Katsirelos, 2015; Liffiton et al., 2016; Bacchus and Katsirelos, 2016; Menc´ıa et al., 2016; Previti et al., 2018; Gr´egoire et al., 2018; Narodytska et al., 2018; Bend´ık et al., 2018], where MUS enumeration algorithms build on the MHS relationship between MUSes and MCSes.

Tractable theories have also been studied, as Horn formulas [Marques-Silva et al., 2016]. In addition, there has been interest in computing the union of all MUSes [Menc´ıa et al., 2019], which can be approximated by the so-called lean kernel [Kleine B¨uning and Kullmann, 2009; Kullmann and Marques-Silva, 2015; Pe˜naloza et al., 2017].

Minimal sets over monotone predicates (MSMP). The similarity among solutions for a number of apparently unrelated problems motivated the proposal of a unifying paradigm, MSMP [Marques-Silva et al., 2013b; MarquesSilva et al., 2017], consisting in computing minimal sets over a monotone predicate. In this setting, a predicate P: 2R → {0, 1}, defined over a reference set R, is monotone if whenever P(R0) holds, with R0 ⊆ R, then P(R1) also holds, with R0 ⊆ R1 ⊆ R. By defining different problems as instances of MSMP, one can devise algorithms that can be used to solve different problems, many of which are related with the analysis of inconsistent formulas. Earlier work [Marques-Silva et al., 2017] proposed a partition of MSMP problems into three classes, depending on the type of monotone predicate considered. (Due to space constraints, the predicate forms are only hinted at in this paper.)

Maximum satisfiability and optimization problems. Given F = B ∪ S, with B ∪ S ⊨⊥, the maximum satisfiability (MaxSAT) problem asks for the largest subset S ′ of S, such that B ∪ S ′ ⊭⊥. A cost can be associated with each clause in S, and so the MaxSAT problem corresponds instead to selecting the subset S ′ of the largest cost. There is a wellknown relationship between MaxSAT solutions and MSSes, in that every MaxSAT solution is an MSS, and so the complement of a MaxSAT solution is an MCS. Furthermore, it is well-known that standard optimization problems can be cast as MaxSAT (where MaxSAT can be interpreted at the propositional level, but also within any fragment of FOL):

where wi ≥ 0, and each pi can be viewed as a 0-place predicate. In this case, just let B ≜M, S ≜ {(¬pi)} and associate with each clause ci in S a cost wi. Thus, F = B ∪ S is inconsistent and an MSS (in terms of cost) of F is a solution to the optimization problem.

Running example. Figure 1 shows an example 2 , used throughout this paper to illustrate the operation of algorithms for extracting and enumerating MUSes and MCSes. As it can be observed, the example is written in Bernays-Sch¨onfinkel's fragment of first-order logic, also referred to as effectively propositional logic (EPR) 3 . It is well-known that EPR is NEXP-complete [Lewis, 1980]. In this example, we have a knowledge base (see Figure 1a) with a number of general statements about parents (P) of new newborn children (N) being proud (R), and that fathers or mothers are parents. We also indicate that there should be no proud people (with the objective of finding proud parents). Moreover, we also have statements about concrete people {aw, rw, hw, pw, mw}. We declare the general statements as hard, denoting that we are certain that the statements are true. In contrast, the information about concrete people is declared as soft, denoting that we are uncertain about whether the information is true or not. The set of statements is inconsistent. Using an existing reasoner for EPR [Korovin, 2013] as an oracle, we can identify two minimal explanations (MUSes) of inconsistency as well as four minimal corrections (MCSes) for eliminating inconsistency. These sets are shown in Figure 1b. The justification for the inconsistencies serve to convey the facts that aw and rw can be inferred to be proud parents, and this is inconsistent with the requirement of no one being proud. As can be observed, the MUSes are MHSes of the MCSes and vice-versa.

2 Adapted from [Nilsson and Maluszynski, 1995, Section 3.1].

3 By using EPR, we highlight that most of the proposed algorithms generalize beyond the propositional cases and beyond oracles for NP. There are dedicated algorithms for the analysis of EPR formulas [Xie and Luo, 2016], but these are fundamentally different from the algorithms studied here.

3 Subset-Minimal Sets

This section overviews approaches for extracting subsetminimal explanations and corrections of inconsistency 4 .

Subset-minimal explanations. Given an inconsistent formula F = B ∪ S, there is a fairly straightforward algorithm for finding one MUS. Starting from a set of clauses M ≜ S, iteratively remove one clause u fromM. If B ∪ (M- {u}) is inconsistent, then we can safely discard u. Otherwise, we must keep u, to preserve inconsistency. After analyzing all clauses of S, the resulting set M is an MUS of F. Variants of this algorithm have been studied since at least the early 90s [Chinneck and Dravnieks, 1991; Bakker et al., 1993; Dershowitz et al., 2006]. Algorithm 1 represents a possible instantiation of this approach for computing MUSes, but which also exploits the MSMP framework. As a result, one must specify which predicate to use for MUS extraction. Following [Marques-Silva et al., 2013b; Marques-Silva et al., 2017], we use the predicate P(B, S,W) ≜ ¬SAT(B ∧W), with W ⊆ R, and R ≜ S. The SAT test for the running example needs to decide the satisfiability of an EPR formula. In general, SAT must solve the decision problem for the logic used to represent B and R. Figure 2 summarizes a possible execution of Algorithm 1 on the formula from Figure 1. Clearly, the computed MUS depends on the order of clauses considered. In this case, the computed MUS is {c3, c4} ≜ {F(aw, pw),N(pw)} which, together with B, is inconsistent and minimal.

4 We consider clausal representations. Analysis of non-clausal formulas has also been investigated in the past [Liffiton and Sakallah, 2008; Belov and Marques-Silva, 2011].

It is simple to conclude that Algorithm 1 requires Θ(|R|) predicate tests. There is no known approach for computing one MUS that improves asymptotically on this bound. A number of algorithms for MUS extraction have been proposed over the years e.g. [Junker, 2004; Marques-Silva et al., 2013b] but without exception, in the worst-case, the number of predicate calls is Ω(|S|). Depending on the target decision problem, different optimizations can be envisioned for MUS extraction, e.g. [Belov et al., 2012; Wieringa, 2012; Lonsing and Egly, 2015]. Table 1 summarizes the query complexity of well-known algorithms for extracting a single MUS, where m and k denote the number of clauses in S and the size of the largest minimal set respectively.

Subset-minimal corrections. Given an inconsistent formula F = B ∪ S, the following approach can be used for finding one MCS. Starting from a set of clauses M ≜ ∅, iteratively consider one clause u ∈ S. If B ∪M∪ {u} is consistent, add u to M. After considering all clauses in S, the clauses that could not be added to M denote an MCS of F. Such an algorithm has been used since at least the mid 00s [Bailey and Stuckey, 2005], and has more recently

Function CLD(P, B, S, R) 1 X ← ∅; 2 (R′ , Y ) ← ReifyClauses(R, X); 3 D← DCLAUSE(Y ); 4 while true do 5 (st , M) ← P(B, S, R′ ∧ D); 6 if ¬st then return M ← SetElements(R, Y ); 7 X ← PickSatisfiedRVars(M, Y ); 8 (R′ , Y ) ← ReifyClauses(R, X); 9 D ← DCLAUSE(Y );

been referred to as basic linear search (BLS) [Marques-Silva et al., 2013a]. As implicit in earlier work [Marques-Silva et al., 2013b; Marques-Silva et al., 2017], by changing the predicate used, Algorithm 1 corresponds to BLS, as outlined above. For this case, the predicate to use is defined as follows: P (B, S, W) ≜ SAT(B ∧ (S \ W)), with W ⊆ R and R ≜ S. Figure 3 illustrates the execution of Algorithm 1 for computing an MCS. The computed set is {c2, c4} ≜ {N(hw), N(pw)}. A number of optimizations to the BLS algorithm have been proposed in earlier work [Marques-Silva et al., 2013a; Menc´ıa et al., 2015]. These include, among others, exploiting models to save a number of predicate tests.

BLS is one of a number of algorithms that have been proposed for extracting MCSes. A conceptually simple solution is to find an MCS using maximum satisfiability [Liffiton and Sakallah, 2008]. In practice, solvingMaxSAT, even if requiring fewer oracle calls in the worst case, is not as effective as other alternatives. One of the most widely used methods for the extraction of MCSes is the Clause D (CLD) algorithm [Marques-Silva et al., 2013a]. For some kinds of MSMP problems, the CLD algorithm can be used.

Algorithm 2 summarizes the main steps of CLD. One starts by reifying each clause ci ∈ S with a fresh relaxation variable (or 0-place predicate): (ri ∨ ci), thus creating a replacement R′ for the original R. Moreover, a disjunction is created with a literal ¬ri for each ri variable (this is the D clause). Then, the algorithm iteratively tests B ∪ R′ ∪ {D}. (Observe that this requires at least one ri to be assigned value 0.) If this formula is satisfiable, then some soft clause(s) ci can be satisfied without assigning ri to 1. Thus, we recreate the formula by dropping any ri assigned value 0 and recreate the D clause without the corresponding literals. The process is repeated until the D clause contains a set of literals that, given the other clauses, cannot be satisfied. These literals identify an MCS 5 . In contrast to the deletion-based approach, as well as to many other algorithms for MUS extraction, CLD expects the oracle call to return a model, from which it can identify the clauses that will no longer be reified. Thus, the predicate call must test for consistency and not for inconsistency. Nevertheless, as shown in earlier work, a large number of minimal set problems are defined by testing for consistency.

Table 2 summarizes the query complexity of well-known algorithms for extracting a single MCS, where n is the number of variables in S, and m and k have the same meaning as before, with the exception of CLD, where k is the size of the smallest MCS. Moreover, there are algorithms that compute an MCS by modifying the oracle, imposing a fixed branching preference [Rosa et al., 2010; Bacchus et al., 2014].

4 Cardinality- &PreferredMinimal Sets

Solving maximum satisfiability. MaxSAT is solved by finding smallest (cost) MCSes. A well-known approach for solving MaxSAT is branch-and-bound search (B&B) [Li and Many`a, 2009]. Since the mid 00s, experimental evidence from a number of applications showed that B&B does not scale in practice [Morgado et al., 2013; Ans´otegui et al., 2013]. An alternative approach consists in reifying all the soft clauses, i.e. replace (ci), with ci ∈ S, with (ri ∨ ci), obtaining Sr; and then defining a constraint X ≜ ∑i wi × ri ≤ τ , where τ ranges from 0 to ∑i wi. As a result, finding the smallest value of τ, such that B ∧ Sr ∧ X is consistent, can then be achieved with linear search [Le Berre and Parrain, 2010], by refining lower or upper bounds on the value of τ, or with binary search [Koshimura et al., 2012]. When the number of soft clauses is large, the representation or handling of X can be a problem. Motivated by this drawback, two approaches for solving MaxSAT using SAT oracles have been proposed since the mid 00s, both of which reason about inconsistency. Core-guided approaches relax soft clauses on demand (see [Morgado et al., 2013; Ans´otegui et al., 2013] for surveys of earlier work and [Martins et al., 2014; Morgado et al., 2014; Alviano et al., 2015] for recent improvements). An alternative is based on the iterative computation of minimum hitting sets (MinHS) on clauses describing (minimal) unsatisfiable cores [Davies and Bacchus, 2011]. Core-guided approaches reify clauses on demand given identified (minimal) unsatisfiable subsets. Cardinality (for unweighted problems) or pseudo-boolean constraints (for weighted problems) are then specified using the relaxation variables and existing lower or upper bounds. MinHS approaches do not reify clauses on demand. Instead, computed (minimal) unsatisfiable subsets serve as sets that must be hit when selecting the next minimum cost subset of clauses whose satisfiability is to be tested. Not surprisingly, both approaches generalize beyond the propositional case.

5 The propositional version admits optimizations, including the fact that reification is unnecessary. Some optimizations are not restricted to the propositional version.

6 In the propositional case one obtains O(min(n, m - k)).

7 LBX can only be used with non-quantified formulas.

Smallest explanations. The previous section argued that existing algorithms for computing an MUS require Θ(|S|) calls to a suitable oracle. In contrast, computing a cardinalityminimal (or smallest) MUS (SMUS) seems to require solving a computationally harder problem. For the case of propositional logic, deciding whether there exists an MUS of size not greater than some k is complete for ΣP2 [Liberatore, 2005], and so computing a smallest MUS requires a logarithmic number of calls to a ΣP2 oracle. The state of the art in computing smallest explanations is FORQES [Ignatiev et al., 2015]. As with other methods studied in this paper, the FORQES algorithm generalizes beyond the propositional case. Earlier work proposed worst-case exponential propositional encodings for this problem [Lynce and Marques-Silva, 2004].

Computing preferred sets. In propositional logic, preferences of inclusion of clauses in MUSes and MCSes are hard for the second level of the polynomial hierarchy [MarquesSilva and Previti, 2014]. Preferences of non-inclusion of clauses in MUSes and MCSes are in FP NP . Similar increases in complexity are expected to hold beyond the propositional case.

5 Enumeration of Minimal Sets

Enumeration of minimal corrections. Enumeration of MCSes can be achieved by enumerating MaxSAT solutions [Liffiton and Sakallah, 2008]. More recent work proposed dedicated algorithms for MCS enumeration [MarquesSilva et al., 2013a; Bacchus et al., 2014; Previti et al., 2017; Previti et al., 2018; Gr´egoire et al., 2018; Narodytska et al., 2018]. To implement enumeration of MCSes, one needs to prevent the same MCS from being computed again. This can be done by blocking the selection of the set of clauses corresponding to an MCS. Most recent work focuses on how to optimize the enumeration process.

Enumeration of minimal explanations. To our best knowledge, enumeration of minimal explanations is harder than the enumeration of minimal corrections, and cannot be obtained directly by iterative extraction of MUSes 8 . One

8 Implicit enumeration of all possible sets [Reiter, 1987; Bailey and Stuckey, 2005] could be considered, but these approaches do not scale in practice [Liffiton and Sakallah, 2008].

Function MINSETENUM(PXYZ, B, S) 1 (N , P) ← (∅, ∅); 2 while true do 3 (st λ, λ) ← FindMHS(N , P); 4 if ¬stλ then break; 5 (st ρ, ρ) ← ChkXYZ(B, S, Cls(λ)); 6 if stρ then 7 τ ← GetXYZ(PXYZ, B, S, S \ Cls(λ)); 8 ReportXYZ(τ ); 9 N ← N ∪ NegClIDs(τ ); 10 else 11 ReportABC(Cls(λ)); 12 P ← P ∪ PosClIDs(Cls(λ));

well-known solution is the enumeration of all MCSes, from which all the MUSes can be obtained by computing all the minimal hitting sets. This was implemented for example in the CAMUS tool [Liffiton and Sakallah, 2008]. A difficulty of these approaches is that MUSes can be computed only after all the MCSes have been computed, which can be exponential in number. A recent alternative is the MARCO algorithm [Liffiton et al., 2016], which iteratively enumerates both MUSes and MCSes, and can be configured such that only one kind of minimal set needs to be extracted.

Algorithm 3 outlines a modified MARCO algorithm, where the preference for a specific kind of minimal set is made explicit. The two configurations are shown in Table 3. Let us focus on the one that gives preference to finding MUSes (the other one is analogous). In this case, XYZ is set to MUS, and ABC to MCS. The algorithm maintains two sets of sets of indices (where index ij is associated to clause cj ∈ S): N, with sets blocking all MUSes found; and P, with sets blocking all MCSes found. Iteratively, a minimal hitting set (MHS) λ of N subject to P is computed, which induces the set of clauses Cls(λ). Then, if ¬SAT(B∧S\Cls(λ)) holds, an MUS is extracted from S \ Cls(λ), which is blocked in N. Otherwise, Cls(λ) represents an MCS, which is blocked in P. The process continues until no MHS exists, guaranteeing that all MUSes and MCSes have been reported. Figure 4 illustrates the execution of Algorithm 3 on the running example. Improvements to MARCO have been proposed in recent years [Bacchus and Katsirelos, 2016; Narodytska et al., 2018; Bend´ık et al., 2018]. Besides, MARCO and variants have a growing number of applications [Polikarpova et al., 2016; Rothenberg and Grumberg, 2016; Brandt et al., 2018].

6 Example Applications

This section provides a brief glimpse of the applications of reasoning about inconsistency. Optimizing linear cost functions subject to sets of constraints is ubiquitous in a growing range of domains. One well-known application domain is program analysis [Si et al., 2017]. Additional examples include Pseudo-Boolean Optimization but also optimization subject to quantified constraints and multi-objective optimization [Terra-Neves et al., 2017]. The relationship between the analysis of inconsistent formulas and model-based diagnosis (MBD) can be traced to the seminal work of Reiter [Reiter, 1987]. Approaches based on solving MaxSAT or computing MCSes have been proposed [Metodi et al., 2014; Marques-Silva et al., 2015; Ignatiev et al., 2019a]. A concrete instantiation of MBD is axiom pinpointing. In this respect, several of the algorithms presented in this paper have been applied to axiom pinpoiting in EL+ ontologies [Sebastiani and Vescovi, 2009; Arif et al., 2015]. In addition, MUS extraction finds application in formal verification and model checking [McMillan and Amla, 2003; Nadel, 2010]. Explainability is arguably a strategic area in Machine Learning (ML). Most existing approaches for explaining ML models are heuristic, with recent results raising concerns about the global validity of the computed explanations [Ignatiev et al., 2019d]. Recent work relates explanations with prime implicants, and so with analyzing inconsistent formulas [Ignatiev et al., 2019b]. Furthermore, recent work has also shown important links between explanations, adversarial examples and the seminal work of Reiter [Ignatiev et al., 2019c].

7 Conclusions &Research Directions

This paper overviews solutions for the analysis of inconsistent formulas, including the identification of minimal corrections and minimal explanations, but also their enumeration. The paper highlights that most of the algorithms proposed for reasoning about inconsistent formulas generalize beyond the propositional case, being applicable in more expressive logics. Motivated by the many existing applications, the recent fast pace of improvement of algorithms for inconsistency analysis is expected to continue in the near future.

Acknowledgements

This work is supported by the AI Interdisciplinary Institute ANITI, funded by the French program "Investing for the Future - PIA3" under Grant agreement no ANR-19-PI3A0004, by the Spanish Government under project TIN201679190-R and by the Principality of Asturias under grant IDI/2018/000176.