Fast Algorithms for Lexicographic Inference

1 Introduction

Non-monotonic reasoning from conditional knowledge bases is a central topic within knowledge representation and reasoning [Lehmann and Magidor, 1989; Kraus et al., 1990; Lehmann, 1995; Kern-Isberner, 2001; Nute and Cross, 2002; Haldimann et al., 2025]. It addresses the inadequacy of reasoning with classical logic in the presence of default or defeasible rules, from now on called conditionals, such as "birds typically fly". Concrete approaches such as rational closure [Lehmann and Magidor, 1989] or lexicographic inference [Lehmann, 1995] typically rely on plausibility orders that rank classical interpretations in terms of how well they satisfy the conditionals of a given knowledge base. Lexicographic inference, which will be the focus of this paper, furthermore relies on the so-called Z-partitioning of the conditionals of the knowledge base, which sorts conditionals in terms of their exceptionality. Classical interpretations are then ranked according to a lexicographic comparison with respect to the number of falsified conditionals on the different levels of exceptionality. Lexicographic inference satisfies a series of desirable properties and is generally regarded as a plausible approach for non-monotonic reasoning from conditional knowledge [Benferhat et al., 1993; Heyninck et al., 2023].

As outlined above, lexicographic inference is defined on rather complex structures such as Z-partitionings and orderings over interpretations. It is therefore no surprise that the computational complexity of lexicographic inference is rather high [Cayrol et al., 1998; Eiter and Lukasiewicz, 2000]. More concretely, the problem of deciding, whether a propositional formula ψ is lexicographically inferred by a propositional formula ϕ, given a set of conditionals ∆, is P NP -complete [Cayrol et al., 1998]. The challenge of addressing this problem algorithmically has, to the best of our knowledge, only been addressed in a recent paper by Haldimann et al. [2025], who develop an algorithm based on minimal correction sets and MaxSAT solver technology. In this paper, we present two new algorithms to address the very same problem. Our first algorithm relies on a compact representation of the lexicographic comparison criterion as a SAT encoding and thus avoids the costly (and repeated) computation of minimal correction sets. Given the Z-partitioning of a set of conditionals, our first algorithm repeatedly determines interpretations of increasing plausibility, by employing said SAT encoding, and depending on whether the finally found interpretation satisfies or violates the queried inference problem, can safely return the correct answer. Our second algorithm also employs (weighted) MaxSAT solver technology and first determines a maximal plausible interpretation for the satisfaction of the query. It then checks (using a single further SAT solver call) whether there is any interpretation for the violation of the query that is at least as plausible as that one, and can then safely return the correct answer. Our extensive experimental evaluation shows that both our new algorithms significantly outperform the algorithm from [Haldimann et al., 2025].

In summary, the main contributions of this paper are as follows:

1. We revisit the computational complexity of lexicographic inference and identify the complexity of certain sub-problems that can be used for algorithmic purposes (Section 3)
2. We present two algorithms for lexicographic inference (Section 4)
3. We instantiate the relevant sub-procedures of our algorithms with suitable (Max)SAT encodings (Section 5)
4. We conduct an extensive experimental evaluation (Section 6)

We present necessary preliminaries in Section 2 and conclude in Section 7. Proofs of all technical results, as well as supplementary material, can be found in an extended version of this paper 1 .

1 Link to extended version: https://zenodo.org/records/20081561

2 Preliminaries

For a (finite) set At of atoms (also called signature) let L(At) be the corresponding propositional language constructed using the usual connectives ∧ (and), ∨ (or), ¬ (negation) and → (material implication). A (classical) interpretation (also called possible world) ω for a propositional language L(At) is a function ω : At → {t, f}. Let Ω(At) denote the set of all interpretations for At. We simply write Ω if the set of atoms is implicitly given. An interpretation ω satisfies (or is a model of) an atom a ∈ At, denoted by ω |= a, if and only if ω(a) = t. The satisfaction relation |= is extended to formulas as usual. As an abbreviation we sometimes identify an interpretation ω with its complete conjunction, i. e., if a1, . . . , an ∈ At are those atoms that are assigned t by ω and an+1, . . . , am ∈ At are those propositions that are assigned f by ω we identify ω by a1 . . . anan+1 . . . am (or any permutation of this). For example, the interpretation ω on {a, b, c} with ω(a) = ω(c) = t and ω(b) = f is abbreviated by abc. For Φ ⊆ L(At) we also define ω |= Φ if and only if ω |= ϕ for every ϕ ∈ Φ. We define the set of models Mod(X) = {ω ∈ Ω(At) | ω |= X} for every formula or set of formulas X. A formula or set of formulas X1 entails another formula or set of formulas X2, denoted by X1 ⊢ X2, if Mod(X1) ⊆ Mod(X2).

For α, β ∈ L(At) the object δ = (β|α) is called a conditional and models the defeasible rule "If α then usually β". A conditional belief base ∆ is a set of conditionals. For every conditional (β|α) define Λ(β|α) : Ω → {v, f, n} via

If Λ(β|α)(ω) = v, we say that ω verifies (β|α), if Λ(β|α)(ω) = f , we say that ω falsifies (β|α), and if Λ(β|α)(ω) = n, we say that ω is not applicable to (β|α).

The central concepts for lexicographical inference [Lehmann, 1995] are as follows.

Definition 1. Let ∆ be a conditional belief base.

1. A conditional δ is tolerated by ∆ if there is ω ∈ Ω with Λδ(ω) = v and Λδ′ (ω) ̸= f for all δ′ ∈ ∆.
2. The Z-Partitioning Z(∆) of ∆ is recursively defined as follows:
3. (a) Z(∆) = (∆) if every δ ∈ ∆ is tolerated by ∆
4. (b) Z(∆) = (∆0 ,∆1 , . . . ,∆k ) if ∆0 is the set of all δ ∈ ∆ that are tolerated by ∆ and Z(∆ \ ∆0 ) = (∆1 , . . . ,∆k ).

Note that the Z-partitioning is not well-defined for every conditional belief base (e. g., it is undefined for ∆ = {(¬a|a)}). We say a conditional belief base ∆ is consistent iff Z(∆) is well-defined, i. e., that Z(∆) exists as defined in Definition 1. For consistent ∆ with Z-Partitioning Z(∆) = (∆0 ,∆1 , . . . ,∆k ) define

for all i = 1, . . . , n. In other words, ξ i∆(ω) is the set of conditionals in the i-th partition of Z(∆) that are falsified by ω.

For a1, . . . , an, b1, . . . , bn ∈ N we write (a1, . . . , an) <lex (b1, . . . , bn) if there is k ∈ {1, . . . , n} such that ak < bk and ai = bi for all i = k + 1, . . . , n. We also write (a1, . . . , an) =lex (b1, . . . , bn) if ai = bi for all i = 1, . . . , n and define ≤lex accordingly.

For the definition of lexicographic inference we use the characterisation from [Haldimann et al., 2025].

Definition 2. Let ∆ be a consistent conditional belief base with Z(∆) = (∆0 ,∆1 , . . . ,∆n ).

• For ω, ω′ ∈ Ω we write ω ≺lex ∆ ω′ iff (|ξ 0∆(ω)|, . . . , |ξ n∆(ω)|) <lex (|ξ 0∆(ω′ )|, . . . , |ξ n∆(ω′ )|). Let ⪯lex ∆ be defined accordingly.
• For formulas ϕ, ψ ∈ L(At) we write ϕ|∼lex ∆ ψ iff for all ω′ ∈ Mod(ϕ ∧ ¬ψ) there is ω ∈ Mod(ϕ ∧ ψ) with ω ≺lex ∆ ω′ .

In other words, a formula ψ can be lexicographically inferred by a formula ϕ, given the conditional knowledge in ∆, iff for all interpretations ω′ that falsify the conditional (ψ|ϕ), we can find another interpretation ω that verifies (ψ|ϕ) and is more plausible according to ≺lex ∆ . Moreover, an interpretation ω is more plausible than an interpretation ω′ , according to ≺lex ∆ , iff ω falsifies strictly less conditionals of some "level" i in Z(∆) and falsifies the same number of conditionals in all higher "levels" of Z(∆). Intuitively, this means that ω is more compatible with the less exceptional conditionals of ∆.

Example 1. We consider the classical penguins example, see, e. g., [Lehmann and Magidor, 1989; Haldimann et al., 2025]. We consider the signature At = {B, P, F, W} with

and the conditional knowledge base

that models that penguins are usually birds, birds usually fly, penguins usually do not fly, and birds usually have wings.

Note that the interpretation BPFW verifies both (F|B) and (W|B) and does not falsify (B|P) and (¬F|P). Moreover, the interpretation BPFW verifies both (B|P) and (¬F|P). This gives us the Z-Partitioning of ∆ as Z(∆) = (∆0 , ∆1 ) with

Then we get, for example, that

and therefore BPFW ≺lex ∆ BPFW. The complete order ≺lex ∆ over Ω(∆) is given in Table 1. We can now infer, for example, that penguins usually have wings, i. e., P|∼lex ∆ W, since for all ω′ ∈ Mod(P ∧ ¬W) there is ω ∈ Mod(P ∧W) with ω ≺lex ∆ ω′ . In particular, we have BPFW ≺lex ∆ ω′ for all ω′ ∈ Mod(P ∧ ¬W).

6 BPFW, BPFW 5 BPFW 4 BPFW, BPFW, BPFW 3 BPFW, BPFW 2 BPFW, BPFW, BPFW

• 1 BPFW, BPFW, BPFW, BPFW, BPFW

Table 1: The order ≺lex ∆ from Example 1, structured into the corresponding layers, i. e., we have ω′ ⪯lex ∆ ω and ω ⪯lex ∆ ω′ for all ω and ω′ in the same layer and ω′ ≺lex ∆ ω if ω′ is in layer i and ω′ is in layer j and i < j.

As hinted at in the above example, we briefly note here that the "for all" and "there is" parts of the definition of lexicographic inference above (see Definition 2) can be swapped without changing the meaning. This representation will be used to show the correctness of our algorithms later.

Proposition 1. Let ∆ be a consistent conditional belief base and ϕ, ψ ∈ L(At). Then ϕ|∼lex ∆ ψ iff there is ω ∈ Mod(ϕ∧ψ) such that ω ≺lex ∆ ω′ for all ω′ ∈ Mod(ϕ ∧¬ψ).

In other words, a formula ψ can be lexicographically inferred by a formula ϕ, given the conditional knowledge in ∆, iff there is an interpretation ω that verifies (ψ|ϕ) and is more plausible, according to ≺lex ∆ , than all interpretations ω′ that falsify the conditional (ψ|ϕ).

In this paper, we are interested in the following computational problem:

LEXINFERENCE Input: Conditional belief base ∆,

formulas ϕ, ψ ∈ L(At)

Output: YES iff ϕ|∼lex ∆ ψ

3 The Computational Complexity of Lexicographic Inference, Revisited

It has been shown in [Cayrol et al., 1998], see also the discussion in [Eiter and Lukasiewicz, 2000], that LEXINFERENCE is P NP -complete. The class P NP , also denoted as ∆P2 , is the class of decision problems that can be solved by an algorithm that runs in deterministic polynomial time and has access to an NP-oracle, i. e., a polynomial-time algorithm that can instantly solve an NP-complete problem in each step, cf. [Papadimitriou, 1994]. In the following, we make some more concrete observations on certain sub-problems of LEXINFERENCE that allows us to devise an effective algorithm in the next section.

We first note that Z(∆) can be determined by successive calls to an NP-oracle.

Proposition 2. Let δ be a conditional and ∆ a consistent conditional belief base.

1. Deciding whether δ is tolerated by ∆ is NP-complete.
2. Determining Z(∆) can be accomplished in polynomial time with at most |∆|(|∆| + 1)/2 calls to an NP-oracle.

Central to our algorithms is the following observation.

Proposition 3. Given ϕ ∈ L, ω ∈ Ω, and the Z-partitioning Z(∆) of a consistent conditional belief base ∆, deciding

Algorithm 1 Algorithm FastLexi

Input: Conditional belief base ∆, formulas ϕ, ψ ∈ L(At) Output: YES iff ϕ|∼lex ∆ ψ 1: Z = ComputeZ(∆) 2: ω′ ← null 3: while true do 4: ω ←SmallerModel(ϕ ∧ψ, ω′ ,Z,∆,≺lex ∆ ) 5: if ω = null then 6: return NO 7: ω′ ←SmallerModel(ϕ ∧¬ψ, ω,Z,∆,⪯lex ∆ ) 8: if ω′ = null then 9: return YES

whether there is ω′ ∈ Ω with ω′ ∈ Mod(ϕ) and ω′ ⪯lex ∆ ω is NP-complete.

Observe that the statement of the previous proposition remains true if we use ≺lex ∆ instead of ⪯lex ∆ .

4 The Algorithms

Our first algorithm FastLexi is depicted in Algorithm 1. It takes a conditional belief base ∆ and two formulas ϕ and ψ as input and starts with computing the Z-partitioning of ∆, using a sub-routine ComputeZ that will be implemented via SAT-encodings in Section 5 and is based on the algorithm sketched in the proof of Proposition 2. In the while-loop in lines 3-9, the algorithm then iteratively determines models of ϕ ∧ ψ and ϕ ∧ ¬ψ that are increasingly smaller wrt. the lexicographic order. More specifically, the sub-routine SmallerModel(γ, ω,Z,∆,⊙) with ⊙ ∈ {≺lex ∆ , ⪯lex ∆ } finds an interpretation ω′ ∈ Mod(γ) such that ω′ ⊙ ω (or returns "null" if no such ω′ can be found). If ω = null then SmallerModel(γ, ω,Z,∆,⊙) returns just any model of γ. The sub-routine SmallerModel will also be implemented using SAT-encodings in Section 5. Here, we only note that according to Proposition 3, SmallerModel can be implemented using a single NP oracle call.

If the algorithm FastLexi terminates in line 6, this means we have not found an interpretation ω that is a model of ϕ∧ψ and strictly more plausible as the model ω′ of ϕ∧¬ψ. In this case the algorithm returns NO. If the algorithm terminates in line 9, this means we have not found an interpretation ω′ that is a model of ϕ ∧ ¬ψ and at least as plausible as the model ω of ϕ ∧ ψ. In this case, the algorithm returns YES.

The formal correctness of the algorithm and its theoretical runtime are given by the following two theorems.

Theorem 1. Assume ∆ is consistent. Algorithm FastLexi returns YES if and only if ϕ|∼lex ∆ ψ.

Theorem 2. Assume ∆ is consistent. Algorithm FastLexi runs in polynomial time and makes at most |∆|(|∆|+1)/2+ 2|∆| calls to an NP-oracle.

Note that the additional assumption in the above two theorems, namely ∆ being consistent, is a technical one. In fact, we can determine the consistency of ∆ while the ZPartitioning of ∆ is computed in the sub-routine ComputeZ without additional effort (see below), and abort the algorithm

Algorithm 2 Algorithm FastLexiMax

if ∆ is found to be inconsistent. We omitted this aspect from Algorithm 1 (and also for our second algorithm FastLexiMax below) to avoid the additional case differentiation.

Algorithm FastLexi iteratively seeks more plausible (wrt. ≺lex ∆ ) interpretations and always switches between interpretations verifying or violating the query under consideration. However, Proposition 1 also allows for another approach to check for a valid inference, namely by first determining some minimal interpretation that verifies the query and then checking whether there is another interpretation that violates it and is at least as plausible as the previously found query. Algorithm FastLexiMax, depicted in Algorithm 2, formalises this idea. Here, the sub-routine SmallestModel(γ,∆,Z) finds a ω ∈ Mod(γ) such that there is no ω′ ∈ Mod(γ) with ω′ ≺lex ∆ ω. As we will see in the next section, SmallestModel(γ,∆,Z) can be implemented through an encoding as a weighted MaxSAT problem and a single call to a (weighted) MaxSAT solver.

Theorem 3. Assume ∆ is consistent. Algorithm FastLexiMax returns YES if and only if ϕ|∼lex ∆ ψ.

Theorem 4. Assume ∆ is consistent. Algorithm FastLexiMax runs in polynomial time and makes at most |∆|(|∆| + 1)/2 + |∆| + 1 calls to an NP-oracle.

The above theorem assumes that SmallestModel requires |∆| calls to an NP-oracle. Since we will encode SmallestModel as a weighted MaxSAT-problem and MaxSAT-solvers use more sophisticated search procedures than linear search, this value can be regarded as a very rough upper bound. Still, from a theoretical point of view, FastLexiMax is already more effective than FastLexi (compare Theorems 2 and 4).

5 Encodings for ComputeZ, SmallerModel, and SmallestModel

We first implement the sub-routines ComputeZ and SmallerModel from Algorithms 1 and 2 using SAT-solving technology [Biere et al., 2021] and encode the underlying decision problems as satisfiability problems. For the rest of this section, let ∆ = {δ1, . . . , δm} be a conditional belief base with δi = (βi|αi) for i = 1, . . . ,m, and let ϕ|∼lex ∆ ψ be the query under consideration.

We first consider ComputeZ. Central to computing the ZPartitioning of ∆ is the question of tolerance. Recall that a conditional δ is tolerated by ∆ if there is ω ∈ Ω with Λδ(ω) = v and Λδ′(ω) ̸= f for all δ′ ∈ ∆. Proposition 2, item 1, noted that this question can be answered with a single NP-oracle call, i. e., using a single query to a SAT-solver. In fact, it can be easily seen that δ = (β|α) is tolerated by ∆ if

is satisfiable. Given an appropriate encoding of Φδ,∆ in conjunctive normal form, its satisfiability can be decided by a single call to a SAT-solver. Following the algorithm sketch in the proof of Proposition 2, item 2, we can implement ComputeZ using at most |∆|(|∆| + 1)/2 calls to the SAT-solver. More concretely, we can check for each δ ∈ ∆, whether δ is tolerated by ∆, collect the positive instances in the first partition ∆0 , and recursively continue with the remaining conditionals. Moreover, we can also test consistency of ∆ while determining Z(∆): if at any point we cannot find a conditional that is tolerated by the remaining conditionals, we can cancel the computation as then ∆ is inconsistent.

We now turn to the encoding of SmallerModel which can be represented as a single satisfiability problem according to Proposition 3. In order to encode SmallerModel we require the use of cardinality constraints [Wynn, 2018; Bittner et al., 2019], in particular at-most-k-constraints. For a set of variables X and a natural number k ∈ N a constraint of the form at most(X, k) is true if and only if at most k variables of X have the truth value t. A constraint at most(X, k) can be naively represented through

For example, for X = {x1, x2, x3, x4} and k = 2 we have

Note that this naive encoding (also called binomial encoding) is inefficient in practice, since at most(X, k) grows in general exponentially. There exist other encodings that make use of auxiliary variables and only grow polynomially in size, e. g., the sequential counter encoding [Sinz, 2005] (which is polynomial in the number of variables and the parameter k) or the approach of [Bailleux et al., 2009] (which is only polynomial in the number of variables). We abstract from the concrete implementation of at most(X, k) and only assume that it can be represented in polynomial size wrt. the number of variables in the signature, see [Wynn, 2018; Bittner et al., 2019] for some more discussion. In our implementation (see Section 6), we used a variant of the totalizer [Bailleux and Boufkhad, 2003] cardinality constraint encoding called kmtotalizer [Morgado et al., 2014].

We consider first a query of the form SmallerModel(γ, ω′ , Z, ∆, ≺lex ∆ ) (see line 4 of Algorithm 1) for an arbitrary formula γ, the difference when considering ⪯lex ∆ instead of ≺lex ∆ (for line 7 of Algorithm 1) will be discussed afterwards. Let the Z-Partitioning of ∆ be given by Z(∆) = (∆0 , . . . ,∆k ). Observe first that given the interpretation ω′ , the numbers |ξ 0∆(ω′ )|, . . . , |ξ k∆(ω′ )| can be determined in polynomial time before encoding the problem.

Now our encoding Φγ,ω′ ,∆,Z for the sub-routine SmallerModel(γ, ω′ , Z, ∆, ≺lex ∆ ) consists of five components:

which we define in the following.

1. Φ1γ represents the fact that we seek a model of γ, i. e., γ must be evaluated to true: Φ1γ = γ
2. Φ2∆ encodes which conditionals are falsified by the model we are seeking. For that, let F1, . . . , Fm be auxiliary variables, where Fi denotes that the conditional δi ∈ ∆ is falsified by the model we are seeking, for i = 1, . . . ,m. Therefore, we encode

1. Φ3ω′ ,∆,Z counts the number of falsified conditionals in each layer of the Z-Partitioning and compares that number to the corresponding one for ω′ . For that, let LE0, . . . ,LEk be auxiliary variables, where LEj denotes that the model under consideration falsifies fewer or equally many conditionals in ∆i than ω′ . We write

1. Similarly, Φ4ω′ ,∆,Z checks for each layer of Z(∆) when the current model falsifies strictly fewer conditionals than ω′ . For that, let L0, . . . ,Lk be auxiliary variables, where Li denotes that the model under consideration falsifies strictly fewer conditionals in ∆i than ω′ . We write

1. Φ5Z finally encodes that the model we seek is lexicographically smaller than ω′ , i. e., there is h ∈ {0, . . . , k} such that Lh is true and LEi is true for all i = h + 1, . . . , k:

It should be clear that the size of Φγ,ω′ ,Z is polynomial in ∆, Z(∆), γ, and the size of the underlying signature (given that we use polynomial encodings for the at most-constraints).

The following theorem shows that Φγ,ω′ ,Z is a suitable SAT-encoding (given an appropriate transformation into conjunctive normal form) of the sub-routine SmallerModel.

Theorem 5. Φγ,ω′ ,∆,Z is satisfiable if and only if there is an interpretation ω with ω ∈ Mod(γ) and ω ≺lex ∆ ω′ .

Since in case of satisfiability, SAT-solvers can return a model (a witness) of the satisfiability, we can implement SmallerModel by either extracting that model (in the original signature) or return null. Also note that we can encode SmallerModel(γ, ω′ ,Z,∆,⪯lex ∆ ) instead of SmallerModel(γ, ω′ , Z, ∆, ≺lex ∆ ) by simply changing Φ5Z to

to accommodate the case that ω′ and the model we seek are lexicographically equivalent.

We now turn to the encoding of SmallestModel(γ, ∆, Z) from Algorithm 2, which we will encode as a weighted MaxSAT problem, i. e., a pair (Φ,Ψ) where Φ is a propositional formula encoding the hard constraints and Ψ = {w1 : l1, . . . , wk : lk} is a set of weighted propositional literals (the weight of literal li is wi ∈ N, for i = 1, . . . , k) that encodes the soft constraints (note that we only need this simple form of weighted MaxSAT problems). A solution to (Φ, Ψ) is then a propositional interpretation ω that satisfies Φ such that the value ∑ω|=li wi is maximal. Now our encoding Φ†γ,∆,Z of the hard constraints for SmallestModel(γ,∆,Z) is defined via Φ†γ,∆,Z = Φ1γ ∧Φ2∆ with Φ1γ and Φ2∆ as above. Define now Z(i) = j if δi ∈ ∆j for i = 1, . . . ,m. Then the encoding Ψ†∆,Z of the hard constraints for SmallestModel(γ,∆, Z) is defined via Ψ†∆,Z = {wZ(i) : ¬Fi | i = 1, . . . ,m} with w0 = 1 and wj = (|∆j-1 | + 1)wj-1 for j = 1, . . . , k. Be reminded that Fi is true if the model under consideration falsifies conditional δi. With the above definition, each nonfalsification of a conditional in ∆j is rewarded with weight wj, for j = 0, . . . , k. Furthermore, the weight of a conditional in ∆j is larger than the sum of all weights of conditionals in ∆0 , . . . ,∆j-1 , so not falsifying conditionals in higher "levels" of Z(∆) is more beneficial for obtaining a large value of the solution than not falsifying conditionals in lower "levels" of Z(∆). We obtain the following correctness result.

Theorem 6. If ˆω : At ∪ {F1, . . . , Fm} → {t, f} is a solution for (Φ†γ,∆,Z ,Ψ†∆,Z ) then for ω : At → {t, f} with ω(x) = ˆω(x) for all x ∈ At, we have ω ∈ Mod(γ) and there is no ω′ ∈ Mod(γ) with ω′ ≺lex ∆ ω.

6 Experimental Evaluation

In this section, we present the results of an experimental analysis comparing the performance of the two proposed algorithms, FastLexi and FastLexiMax, with LexInf from [Haldimann et al., 2025]. In their work, Haldimann et al. (2025) also compared their algorithm to a naive Java implementation of lexicographic inference named LexJ. However, as LexJ did not perform competitively, we refrain from including it in this evaluation.

The remainder of this section is structured as follows. In Section 6.1, the experimental setup is described, including the implementation, the used datasets, the performance metrics, and the experimental procedure. Subsequently, Section 6.2 presents the results of the experimental analysis.

6.1 Setup

Implementation We implemented the algorithms FastLexi and FastLexiMax in Python, using the SAT toolkit PySAT [Ignatiev et al., 2024]. FastLexi is parameterizable with different SAT solvers, including CaDiCal (rel-1.9.5) [Biere et al., 2024], Glucose (4.2.1) [Audemard and Simon, 2009], MapleLCMDistChronoBT [Kochemazov et al., 2019], and MiniSAT (2.2) [Sorensson and Een, 2005]. The MaxSAT version FastLexiMax uses the RC2 [Ignatiev et al., 2018] solver. The implementation is open source and available on GitHub 2 . For the LexInf solver, we implemented a wrapper that offers an identical solver interface to our solvers. We also replaced the LexInf parser for belief bases and queries with our implementation, as the original parser was unable to handle instances with a large number of conditionals.

Datasets In total, we used 3 different data sets for the evaluation: (1) CLKR-PS005, (2) CLKR-Buster, (3) AwAKB.

The CLKR-PS005 [Beierle et al., 2024] dataset contains 100 randomly generated belief bases and 1000 (10 per belief base) queries for each combination of signature size |Σ| (ranging from 6 to 120) and belief base size |∆| (ranging from 6 to 160), resulting in a total of 2700 belief bases and 27000 queries. The dataset CLKR-PS005 is the same dataset that was used in the evaluation of [Haldimann et al., 2025]. For more information on the random belief base generator see [von Berg et al., 2024]

The dataset CLKR-Buster was created using the same generator as the previous dataset, but with larger signatures (2003000) and a larger number of conditionals (200-3000). The data set consists of 270 belief bases, each with 10 queries, for a total of 2700 queries.

The AwAKB [Kuhlmann et al., 2022] comprises 1920 knowledge bases derived from the Animals with Attributes (AwA) dataset, a widely used benchmark in machine learning. AwA contains 50 animal categories described by 85 binary attributes. The authors applied the Apriori algorithm [Agrawal et al., 1993] to extract association rules from AwA and then treated each mined rule as a propositional implication (rules were restricted to contain only 4 literals). We adapted the data set by interpreting the implications as conditionals. Since the number of conditionals varies greatly, we have further grouped the dataset into 5 subsets based on the number of conditionals: (1) tiny, (2) small, (3) medium, (4) large, and (5) huge. All subsets contain 336 instances.

Metrics We compared the performance of all algorithms in terms of (1) Belief Base Coverage (Covb), (2) Query Coverage (Covq), and (3) Penalized Average Runtime 2 (PAR2).

The belief base coverage Covb is the ratio between completely solved belief bases and the total number of belief bases. A belief base is fully solved when all associated queries have been solved. Similarly, the query coverage Covq is defined as the ratio between solved queries and the total number of solved queries.

The PAR2 score is defined as the average runtime (in seconds) of solved instances, plus twice the timeout value, allowing runtime to be considered while still setting a strong focus

2 https://github.com/aig-hagen/Luthor

CLKR-Buster

on instance coverage. For example, for a 300-second timeout, the runtime of unsolved instances is counted as 2∗300 = 600 seconds.

Procedure In our experiments, we investigated 6 different algorithms, consisting of the SAT version of FastLexi, parameterized with four different SAT solvers (CaDiCaL, Glucose, MapleLCMDistChronoBT, and MiniSAT), as well as the MaxSAT version FastLexiMax and LexInf. Each algorithm was executed for each belief base and its 10 queries. We set a 5 minutes (300 seconds) timeout for each query. If an instance was not solved within this limit, it was terminated, marked as timed out, and its runtime set to the timeout value. In addition, we computed a virtual best solver (VBS) by selecting the best runtime for each query. All experiments were conducted on a machine running Ubuntu 20.04 with an Intel Xeon E5 3.4 GHz CPU and 192 GB of RAM.

6.2 Results

CLKR Table 2 shows the results in terms of belief base coverage (Covb), query coverage (Covq), and penalized average runtime (PAR2) on the CLKR-PS005 and CLKR-Buster benchmarks. Starting with the CLKRPS005 benchmark, the results show that all versions of FastLexi (FastLexiMax, FastLexiCaDicaL, FastLexiGlucose, FastLexiMaple, and FastLexiMiniSAT) achieve perfect query coverage and, therefore, perfect belief base coverage. Furthermore, the results show that all versions yield comparable PAR2 scores, with FastLexiGlucose achieving the best result of 0.707. The remaining FastLexi versions attain scores between 0.721 (FastLexiMiniSAT) and 0.743 (FastLexiCaDicaL). The LexInf solver achieves query coverage of 0.974 and belief base coverage of 0.919. LexInf also performs worse in terms of PAR2 with a score of 19.282.

For the CLKR-Buster benchmark, which has significantly more conditionals and a larger signature, only two algorithms achieve full coverage: FastLexiCaDicaL and FastLexiMax. The other FastLexi variants lie between 0.844 (FastLexiMiniSAT) and 0.989 (FastLexiMaple) for Covb and between 0.980 (FastLexiMiniSAT) and 0.999 (FastLexiMaple) in terms of Covq values. LexInf achieves the worst coverage values with a Covb value of 0.778 and a Covq value of 0.964. In terms of PAR2 scores, FastLexiMax achieves the best at 5.723 (on par with VBS), nearly twice as fast as the next best algorithm, FastLexiMaple (10.205), and closely followed by FastLexiCaDicaL (10.307). The LexInf algorithm shows the worst performance, with a PAR2 score of 34.444, which is noticeably worse than the worst of the FastLexi variants, FastLexiMiniSAT, with a score of 24.514.

AwAKB Table 3 summarizes belief base coverage (Covb), query coverage (Covq), and penalized average runtime (PAR2) on the AwAKB dataset, grouped into tiny, small, medium, large, and huge subsets by the number of conditionals. On the tiny (7-73 conditionals) subset, all algorithms achieve perfect query and belief base coverage and show very similar runtimes. The best PAR2 is obtained by FastLexiMaple with 0.436, while the remaining variants fall into a very narrow range between 0.441 (FastLexiMiniSAT) and 0.445 (FastLexiCaDicaL). The LexInf algorithm likewise attains complete coverage, with a comparable PAR2 score of 0.552.

For the small subset (73-465 conditionals), coverage remains perfect for FastLexiMax, FastLexiCaDicaL, FastLexiGlucose, and FastLexiMiniSAT, and is only marginally lower for FastLexiMaple with a Covb of 0.994 and a Covq value of 0.999. However, the results show a substantial decline in coverage for the LexInf algorithm, with a Covb value of 0.577 and a Covq value of 0.623. This fact is also reflected in the PAR2 scores: LexInf achieves a score of 227.254, which is significantly worse than all other algorithms. For comparison: The worst FastLexi version for this subset,FastLexiMaple, achieves a PAR2 score of 1.074 and the best version, FastLexiMax, achieves a value of 0.585.

The trend observed so far is continued with the medium and large subsets.

Finally, the huge (9535-96097 conditionals) subset is the only one where none of the algorithms is able to solve all queries. Here, FastLexiMax achieves the overall best performance, combining the highest coverage (Covb = 0.78, Covq = 0.79) with the lowest PAR2 (177.979), very similar to the VBS (177.841). The remaining SAT-backed variants show lower belief base coverage (0.679-0.702) and higher PAR2 values (approximately 210-215). FastLexiMaple performs worst of all FastLexi variants in this subset, with a Covb of 0.399 and a Covq of 0.738, and the highest PAR2 (231.602). Nevertheless, these results are still comparable than those of LexInf on the small subset which are on average 160 times smaller then the huge instances. The LexInf algorithm is not able to fully solve a single belief base, indicated by a Covb of 0 and a low Covq of 0.106. Accordingly, LexInf achieves the highest PAR2 score of 548.393, approaching the worst possible score of 600.

Summary All evaluated FastLexi variants consistently outperform LexInf across all benchmarks. Furthermore, the performance differences increase with growing instance size, indicating that the advantages of FastLexi become more pronounced on larger problem instances. For instance, even for very large instances, such as those in the AwAKB huge subset, FastLexi maintains competitive performance, highlighting its efficiency and scalability. Moreover, differences can also be observed between the MaxSAT and SAT variants. Specifically, the FastLexiMax solver achieves the best results on nearly all benchmarks, yielding results similar to those of the VBS. However, among the SAT-based FastLexi variants, no single version consistently outperforms the others, as their performance varies across benchmarks.

7 Discussion and Conclusion

We presented two new algorithms for lexicographic inference from conditional knowledge bases. Our algorithms are based on compact SAT encodings of the lexicographic comparison criterion and make effective use of SAT and MaxSAT solving technology. In our experimental evaluation we showed, that both algorithms significantly outperform the state of the art, while the MaxSAT approach shows even more superior performance.

For future work we intend to apply the developed ideas to other inference operators for conditional knowledge bases, such as (disjunctive) rational closure [Lehmann and Magidor, 1989; Booth and Varzinczak, 2025], c-representations [KernIsberner, 2001], System Z [Pearl, 1990], or System W [Komo and Beierle, 2022].

Ethical Statement

There are no ethical issues.