We explore the use of ordered binary decision diagrams (OBDDs) and multi-terminal binary decision diagrams (MTBDDs) for compiling and executing defeasible reasoning, focusing on System Z, also known as rational closure. We introduce an OBDD-based algorithm for System Z inference that parallels traditional SAT-based approaches. Additionally, we investigate the use of MTBDDs for encoding ordinal conditional functions (OCFs), providing a more general and unified knowledge compilation framework for defeasible reasoning tasks involving ranking functions. While our primary focus is on System Z, the proposed techniques are applicable to other forms of defeasible reasoning and conditional logic more broadly. Experimental results demonstrate that OBDDs can significantly accelerate inference. However, our evaluation is limited to synthetically generated belief bases, and further research is needed to validate benefits in real-world scenarios. Overall, our findings suggest that binary decision diagrams ofer a promising alternative to SAT -based methods for defeasible reasoning, and warrant further investigation.
Preliminary results. On synthetically generated belief bases with up to 20 variables, our OBDD solver answers queries up to 100× faster than a SAT baseline, while the MTBDD version is up to 50× faster. The speed-up decreases with input size because random formulas lack the regularities that BDDs exploit for compactness, and real-world datasets for conditional logic are still rare. Nonetheless, the gains confirm that decision diagrams are a credible alternative to SAT.
We summarize the main contributions of this paper as follows: • An OBDD-based re-implementation of SAT-style System inference. • An ADD compilation that directly encodes the System ranking function. • An empirical comparison of SAT, OBDD, and ADD engines on synthetic data.
In this section, we survey the necessary preliminaries on propositional logic (Sec. 2.1), conditional logic (Sec. 2.2), ordinal conditional functions (Sec. 2.3) and inductive inference (Sec. 2.4). Lastly, we provide the necessary preliminaries on ordered binary decision diagrams and diagram synthesis (Sec. 2.5).
Assuming a finite set of boolean variables Σ, we fix a variable ordering 0, 1, . . . , − 1. This ordering remains fixed for all formulas in our propositional language ℒΣ (abbreviated to ℒ), which is constructed using the usual connectives of propositional logic. A classical interpretation or possible world is a mapping : Σ ↦→ {⊤, ⊥}. The set of all such interpretations is Ω. We write |= if satisfies , and ̸|= otherwise. The set of models of a formula is Mods( ) = { ∈ Ω | |= }. For clarity, we sometimes write (0, 1, . . . , − 1) to denote the formula obtained by replacing each instance of in with ∈ {⊤, ⊥, }. If the assignment is clear or not relevant, we simply write () to denote the formula resulting when every instance of is replaced by its truth assignment in . Definition 1 (conditioning). The conditioning of on a variable and constant ∈ {⊤, ⊥} is the formula obtained by replacing all instances of in with . We denote this by
= = (0, . . . , − 1, , +1, . . . , − 1).
In the literature, =⊤ and =⊥ are often referred to the positive and negative cofactors of with respect to .
Propositional logic is extended to conditional logic by introducing conditionals, statements of the form ( | ). The language of propositional conditional logic is given by (ℒ | ℒ) = {( | ) | , ∈ ℒ}. For a world , it is useful to define the semantics of conditionals as generalized indicator functions [12]: ( | )() = ⎪⎧⊤, if ( ∧ )() = ⊤, ⎨
⊥, if ( ∧ ¬ )() = ⊤, ⎪⎩× , otherwise.
⎧⎪⊤, if ∀ ∈ Δ, () = ⊤, Δ() = ⎨⊥, if ∃ ∈ Δ, () = ⊥,
⎪⎩× , otherwise.
A world verifies a conditional if () = ⊤, falsifies it if () = ⊥, and is irrelevant otherwise (i.e. when |= ¬ , denoted () = × ). For a belief base Δ (a finite set of conditionals), we write: Intuitively, the value × marks worlds where the antecedent of a conditional is false—so the statement is irrelevant—and, for a belief base Δ, it indicates that no conditional is falsified and at least one is irrelevant. To use classical reasoning tools, one often uses materialization ℳ( | ) = → , where ( → ) is considered only to check falsifications. We extend this to a belief base Δ such that ℳ(Δ) = ⋀︀{ℳ( ) | ∈ Δ}.
Ordinal conditional functions (OCFs) or ranking functions are a well- known semantics for conditional logic introduced by Spohn [1988]. They assign to each world a non-negative integer reflecting its degree of surprise. Higher values indicate less plausibility, and ∞ impossibility.
Definition 2 (Ranking Function). A ranking function is a mapping : Ω → N ∪ {∞}. It extends to formulas by
( ) = min{ () | |= }, with ∅ = ∞. We say accepts ( | ) if ( ∧ ) < ( ∧ ¬ ). In other words, a ranking function accepts ( | ) if all the most plausible worlds satisfying also satisfy . Also, | | denotes |{ | ∃ ∈ Ω, () = }| for < ∞.
Inductive inference, or defeasible inference, involves the use of inference relations |∼ Δ derived from a conditional belief base Δ, known as inductive inference operators. Ranking functions ofer a common basis for generating a relation |∼ , where |∼ holds if accepts ( | ). Notable examples of such inference relations generated from ranking functions include System Z [2] (equivalent to rational closure [4]), lexicographic closure [10], and c-representations [11]. This paper focuses on System Z.
System Z partitions a finite belief base Δ into groups of conditionals (a Z-partitioning) such that each group collects conditionals mutually “tolerable.” A conditional is tolerated by Δ if there is some for which () = ⊤ and Δ() ̸= ⊥. Classical formulas can also be included in Δ by representing them as conditionals (⊥ | ¬ ). Such conditionals are inherently intolerable and are assigned to Δ∞. The System Z ranking function Δ is then defined through this partitioning.
Definition 3 (Z-partitioning and Z-Ranking). Let Δ = (Δ0, Δ1, . . . , Δ∞) be the Z-partitioning of Δ, where Δ0 = { ∈ Δ | Δ tolerates } and (Δ1, . . . , Δ∞) is the Z-partitioning of Δ ∖ Δ0. The System Z ranking Δ is given by Δ () = min{ | (︀ ⋃︁ Δ )︀ () ̸= ⊥} ≥ (min ∅ = ∞).
Intuitively, the Z-ranking orders worlds by how badly they violate the belief base: worlds satisfying all high-priority (more tolerable) conditionals get lower ranks, while those that break less tolerable ones are pushed to higher ranks, with classically impossible worlds assigned rank ∞. Classical formulas thus establish an initial distinction between worlds with finite ranks ∈ N and those deemed classically impossible (assigned rank ∞). Once the ranking function Δ has been generated for a given belief base Δ, it can then be used to perform inference under System Z.
Definition 4 (Z-inference). Given a belief base Δ, the inference relation |∼ Δ corresponding to System Z inference is defined according to Δ such that |∼ Δ if Δ accepts ( | ).
Example 1. Let Δ = {︀ ( | ), ( | ), (¬ | ), (⊥ | ¬(→ ))}︀ , with = bird, = penguin, = has wings, and = can fly. System Z yields the partition The induced ranking function Δ assigns: Δ0 = {( | ), ( | )}, Δ1 = {(¬ | )}, Δ∞ = {(⊥ | ¬(→ ))}.
Δ ( ∧ ∧ ) = 2, Δ ( ∧ ∧ ¬ ) = 1,
Δ ( ∧ ¬) = ∞, Δ (¬ ∧ ∧ ∧ ) = 0, Δ (¬ ∧ ∧ ∧ ¬) = 1, Δ (¬ ∧ ∧ ¬ ) = 1,
Δ (¬ ∧ ¬) = 0.
From this we infer, for instance:
∧ ¬ ̸ |∼ Δ , ∧ ¬ ̸ |∼ Δ ¬, ̸ |∼ Δ .
Knowledge compilation seeks to address the computational dificulty inherent in general propositional reasoning by dividing the task of query answering into two distinct phases: Of-line Compile a general propositional formula ∈ ℒ into a logically equivalent representation ∈ , for a more computationally tractable target language . Although this compilation step may be exponentially expensive in the worst case, it is performed only once.
On-line Eficiently answer queries, typically in polynomial time, using the previously compiled representation .
The underlying rationale is that an initial, computationally intensive compilation phase significantly reduces the complexity of subsequent queries, efectively amortizing the initial compilation cost over multiple queries. A query (e.g., satisfiability, entailment, or model counting) is considered tractable on a target language if there exists an algorithm that, for every formula ∈ , determines ( ) within polynomial time relative to the size | | of its representation in . In this paper, the primary query under consideration is entailment checking. Consequently, our analysis will focus on two prominent target languages: CNF (Conjunctive Normal Form), the standard input format for most SAT solvers, and OBDD (Ordered Binary Decision Diagrams), commonly used for tractable and eficient entailment checking.
Definition 5 (CNF). A formula is in the language CNF if it can be expressed as:
= ⋀︁ , = ⋁︁ ℓ ,
=1 =1 where each literal ℓ is either or ¬ for some variable ∈ Σ. The size | | is defined as the total number of literal occurrences in .
SAT solving on general CNF formulas is a well-known problem in NP, and thus CNF does not qualify as a tractable target language for entailment checking. The next target language we consider, OBDD, is in fact tractable for many key queries—most notably entailment checking. Ordered Binary Decision Diagrams were first proposed by Bryant [ 7], building on earlier work by Lee [13] and Akers [14], and remain the most prominent tractable representation in the literature.
Definition 6 (OBDD-structure). A graph Ψ is in the language OBDD if it is a rooted, directed acyclic graph with two types of nodes: • Variable nodes: Each has an index I( ) < and two child nodes T( ) and F( ) satisfying
I( ) < I(T( )) and I( ) < I(F( )).
• Sink nodes: Each has a value V( ) ∈ {⊤, ⊥}.
Each variable node corresponds to a variable where I( ) = . Any world traces a unique path from the root: going to T( ) if |= , and to F( ) if |= ¬, until a sink node is reached. Therefore, an OBDD is a graphical representation of the semantic behavior of all Boolean formulas equivalent to some formula , defined recursively as follows.
Definition 7 (OBDD-representation). An OBDD Ψ with root represents all formulas equivalent to , where is defined as follows: • If is a sink node, then ≡ ⊤ if V( ) = ⊤, or ≡ ⊥ if V( ) = ⊥. • If is a variable node with I( ) = , then ≡
︀( ∧ =⊤︀) ∨ ︀( ¬ ∧ =⊥︀) , with T( ) and F( ) representing formulas equivalent to =⊤ and =⊥, respectively. This relies on Shannon expansion [15] (also known as Boole’s expansion theorem [16]), where a formula is recursively decomposed into positive and negative cofactors for each variable in the ordering. Definition 8 (Isomorphic). Two OBDDs, Ψ1 and Ψ2, are isomorphic provided there exists a bijection between their nodes such that for every node 1 in Ψ1 with ( 1) = 2 in Ψ2, one of the following holds: • Both 1 and 2 are sink nodes with V( 1) = V( 2). • Both 1 and 2 are variable nodes with I( 1) = I( 2), and the bijection preserves their children: (T( 1)) = T( 2) and (F( 1)) = F( 2).
Definition 9 (Reduced). An OBDD is fully reduced if it contains no redundant nodes such that T( ) = F( ) and no pair of isomorphic subgraphs.
In practice, an “OBDD” refers by default to a fully reduced diagram. This complete reduction yields a unique, canonical form for each Boolean function, making equivalence checking a straightforward graph-isomorphism test. Moreover, when compiling multiple functions, it is standard to embed them in a single shared DAG: identical subgraphs are factored out and reused, resulting in a very compact representation that exploits redundancy across formulas, an example of this is shown in Figure 4.
Most OBDD transformations rely on Bryant’s apply algorithm [7], which performs Boolean operations (e.g. ∧, ∨, ⊕ ) by simultaneously traversing two operand diagrams and at the same time producing the diagram resulting from the operation. In practice, one compiles a complex formula by recursively descending its parse tree and invoking apply at each connective—this “recursive-descent parsing” makes apply the workhorse of OBDD construction.
A crucial feature is that each reduced subgraph is assigned a unique numeric ID. Whenever apply
produces a new subgraph, it checks whether an identical one (i.e. isomorphic) has been seen before; if
so, it reuses that existing ID. This scheme means that two OBDDs represent the same function precisely
when their root IDs coincide—equivalence checking reduces to a single ID comparison in (
Memoization further accelerates apply by caching every computed result for a given pair of operand
IDs and operator. If the same operation is requested again, apply simply looks up the cached outcome
instead of re-descending the diagrams. Together, these ideas guarantee that apply runs in (|Ψ1| · | Ψ2|)
time in the worst case, while trivializing equivalence tests and leaving other queries—satisfiability
in (
Operation Satisfiability apply Equivalence checking Model counting Model evaluation (assignment)
(
The succinctness of an OBDD depends critically on the variable ordering chosen—a problem that is NP-hard in the worst case [17]. Thankfully, a range of efective heuristics (such as sifting, dynamic reordering, and even genetic-algorithm approaches) typically find good orders in practice. Even so, most arbitrary Boolean functions admit no compact OBDD representation, and exponential blow-up remains possible. The practical power of OBDDs, therefore, derives largely from the fact that meaningful, realworld formulas often exhibit substantial structural regularity and redundancy, which these diagrams can exploit to remain tractable.
Constructing the –partition of a conditional belief base is FPNP-complete, and performing –inference ‖ once this partition is known is PNP-complete [18, 5]. In the absence of an NP-oracle, the standard remedy is to reduce the relevant sub-tasks to instances of propositional satisfiability and to rely on a modern SAT solver—typically a conflict-driven clause-learning (CDCL) engine [19, 20, 21]—to answer ‖ each query. is obtained by
Definition 10 (Z-vector). Let (Δ0, Δ1, . . . , Δ∞) be the –partition of Δ. The -vector ( 0 , . . . , ) = ℳ ︁( ⋃︁ Δ ,
︁) ≥ = ⎧ ⎨min{ | Δ = ∅} ⎩max{ | Δ ̸= ∅} if Δ∞ ̸= ∅, otherwise. where ℳ materialises every conditional as an implication and is the largest index that actually occurs:
Each component is translated once into CNF and handed to the SAT solver as a separate formula.
Freund’s original SAT-based procedure [22], refined by Casini et al. [23], is reproduced in Algorithm 1. The routine scans the -vector from the lowest to the highest rank, searching for the first level whose conjunction with the antecedent is satisfiable. Once such a level is found, a second SAT call decides whether some world of the same rank also violates the consequent . giving a bound of (| Δ | · 2|Σ|).
Complexity. In the worst case the loop invokes the solver | Δ | times; each call can take (2|Σ|), Input: –vector (CNF( 0 ), . . . , CNF( )); conditional ( | ) Output: true if Δ accepts ( | ) ← CNF( ) ¬ ← CNF(¬ ) ←
0 while ≤ do ← ∧ if SAT( ) then
return ¬SAT( ∧ ¬ )
Lemma 1. For the -vector ( 0 , . . . , ) of Δ, and for every > 0,
{ | Δ () = 0} = Mods( 0 ), { | Δ () = } = Mods( ) ∖ Mods( − 1).
Proof. Straightforward induction on , using Δ () = min{ | (⋃︀≥ Δ)() ̸= ⊥}. Theorem 2. For any belief base Δ with -vector ( 0 , . . . , ) and any conditional ( | ), ZinfSAT terminates and returns true exactly when Δ accepts ( | ).
Proof. Termination follows from the bounded loop over . For soundness, let = Δ ( ). By Lemma 1, ∧ is satisfiable and ∧ is unsatisfiable for < , so the loop stops at the correct level. Acceptance then hinges on the (un)satisfiability of ∧ ∧ ¬ , which equals Δ ( ∧ ¬ ) = . Completeness is the converse argument.
Binary decision diagrams are a natural alternative to the SAT encoding of Sect. 3: equivalence checking is constant-time, Boolean operations are handled by a single apply routine. We therefore compile each level of the –partition into an OBDD, obtaining the OBDD -vector (Ψ0 , . . . , Ψ ), and answer queries by a short sweep through that vector. An example of the optimal shared DAG representing the OBDD Z-vector for the belief base in Example 1 is illustrated in Figure 1.
Let Ψ and Ψ be the OBDDs for and . Algorithm 2 (ZinfOBDD) tests successive ranks until it finds the first such that Ψ ∧ Ψ is satisfiable; a second test then checks whether any world of that same rank falsifies .
Complexity. An apply call on two diagrams of size |Ψ | and |Ψ | runs in (|Ψ | · | Ψ |). In the worst case the loop iterates | Δ | times, giving ︀( |Ψ | · ∑︀| Δ | =0 |Ψ |)︀ , which improves on the SAT bound (| Δ | · 2|Σ|) whenever the diagrams are compact. Ψ ← ¬Ψ ← ← 0 while ≤ do Ψ ← Ψ ∧ Ψ if Ψ ̸= ⊥ then
return (︀ Ψ ∧ ¬Ψ )︀ = ⊥ end ← + 1 end return false
Algorithm 2: ZinfOBDD
Theorem 3. Given the OBDD -vector (Ψ0 , . . . , Ψ ) and an OBDD conditional (Ψ | Ψ ), ZinfOBDD terminates and returns true exactly when Δ accepts ( | ).
Proof. Termination is immediate from the bounded loop. By Lemma 1, Ψ ∧ Ψ ̸= ⊥ holds precisely when Δ ( ) = . The additional test Ψ ∧ ¬Ψ = ⊥ is therefore equivalent to Δ ( ∧ ¬ ) > Δ ( ), i.e. to the acceptance criterion for ( | ) under System Z.
An algebraic decision diagram (ADD) [9, 8] is a rooted, directed acyclic graph analogous to an OBDD, except that its sink nodes may carry values from an arbitrary finite domain rather than just ⊤, ⊥. ADDs inherit the eficient reduce and apply algorithms of OBDDs, making them a powerful compilation target for a wide range of reasoning tasks. By generalizing this compilation target to encompass arbitrary ranking functions, we obtain a single, coherent knowledge-compilation framework for all defeasible-reasoning formalisms based on ordinal conditional functions. In particular, this unified approach subsumes not only System Z but also other ranking-based inference mechanisms such as lexicographic closure [10] and c-representations [11]. Because the compiled structure directly encodes the ranking function, it additionally permits eficient execution of model-centric operations—including model checking, model enumeration, and model counting—without resorting to costly SAT-based procedures. We therefore refer to any multi-terminal BDD over N ∪ {∞} that represents a ranking function as a ranked binary decision diagram (RBDD).
Definition 11 (RBDD). A reduced ADD Ψ whose sinks are labelled by non-negative integers or ∞ is an RBDD. Every variable node (index I( )) has high and low children T( ) and F( ) consistent with the variable ordering. Additionally, we record at every node the set of reachable ranks
R( ) = {︃{V( )}
sink,
R(T( )) ∪ R(F( )) otherwise,
which later allows (
We say any graph adhereing to these requirements is in the language RBDD. Before giving the recursive semantics of an RBDD, we must introduce the notion of conditioning, which captures how a ranking function behaves when one variable is fixed. Conditioning yields sub -ranking functions corresponding to each truth value of the chosen variable, and will serve as the basis for the node-wise interpretation of the diagram.
Definition 12 (Conditioning / cofactor of a ranking function). Let : Ω → N ∪ {∞} be a ranking function over the set of worlds Ω, and let ∈ Σ be a propositional variable. For ∈ {⊤, ⊥}, the conditioning (or cofactor) of with respect to = is the function
=() = (︀ [ ↦→ ])︀ , ∈ {⊤, ⊥}, where [ ↦→ ] denotes the world obtained from by fixing the value of to while leaving all other variables unchanged.
Conditioned on diferent values of , each sub-ranking function = restricts to a simpler domain, capturing its behavior when is permanently fixed. By iterating this process over successive variables, we generate a hierarchy of increasingly specialized ranking functions. An RBDD compactly represents this entire hierarchy: each internal node corresponds to one such conditioning step, and its outgoing edges lead to the sub-ranking functions that arise when the node’s variable is set to ⊤ or ⊥. Definition 13 (Recursive semantics of an RBDD). Let be the root of Ψ . The ranking function represented by the diagram is defined recursively: • Sink node. If is a sink, then () = V( ) for all worlds . • Variable node. If I( ) = , denote by + = =⊤ the function represented by T( ) and by − = =⊥ the function represented by F( ). Then for every world
⎧ +() if |= , () = ⎨
⎩ − () otherwise.
The optimal RBDD for the belief base in Example 1 is shown in Figure 2.
The usual OBDD reduction rules—eliminating redundant nodes and merging isomorphic sub-graphs—carry over unchanged, and we henceforth treat every RBDD as fully reduced unless noted otherwise. As argued earlier, the practical construction of large decision diagrams proceeds by successive applications of the apply algorithm: complex structures are built from a collection of smaller, already-compiled components. For System Z we first compile each level of the Z -partitioning into an OBDD, obtaining the Z-vector (Ψ0 , . . . , Ψ ) such that Ψ = OBDD( ). These OBDDs can then be relabelled and combined to yield a single RBDD encoding the entire System Z ranking function, as stated next. Ψ by the integer and every sink label ⊥ by ∞. Then Theorem 4. Let (Ψ0 , . . . , Ψ ) be the OBDD Z-vector of a belief base Δ. Replace every sink label ⊤ in Ψ = min(︀ Ψ0 , Ψ1 , . . . , Ψ )︀
is an RBDD that represents the System Z ranking function Δ .
Proof. By Lemma 1, the OBDD Ψ (after relabelling) evaluates to a finite rank ≤ precisely on those worlds whose System Z rank is at most , and to ∞ otherwise. Taking the pointwise minimum of these diagrams therefore assigns to each world the smallest for which Δ () = ; if no such exists, every operand contributes ∞ and the minimum is ∞. Consequently the resulting diagram encodes exactly Δ . ( |
We now show how a constant number of apply operations sufices to decide whether a conditional ) is accepted by a ranking function represented as an RBDD Ψ . The key is an operator that restricts a rank to cases in which a Boolean formula holds and maps all other cases to ∞. Definition 14 (Restriction operator ∝). For 1 ∈ N ∪ {∞} and 2 ∈ {⊤, ⊥} define 1 ∝ 2 = {︃1 if 2 = ⊤ ∞ if 2 = ⊥ , . () = {︃ () if |= , ∞
Given an RBDD Ψ and an OBDD Ψ , the diagram Ψ ∝ Ψ is obtained by applying this operator node-wise via the standard apply algorithm. The result is an RBDD that represents the restricted ranking function
Let Ψ and Ψ be the OBDDs for and , respectively, and set 1 = root(Ψ ∝ Ψ ),
2 = root(︀ (Ψ ∝ Ψ ) ∝ ¬Ψ )︀ .
Theorem 5. The ranking function accepts the conditional ( | ) if
min R( 1) < min R( 2).
Proof. If ( ) = ∞ then Ψ ∝ Ψ is a single sink labelled ∞, and the second synthesis yields the same; the inequality fails and the conditional is rejected. Otherwise min R( 1) = ( ) and min R( 2) = ( ∧ ¬ ). Hence min R( 1) < min R( 2) ⇐⇒ ( ) < ( ∧ ¬ ), which is equivalent to the acceptance condition ( ∧ ) < ( ∧ ¬ ).
Consequently, a single entailment check requires just three apply operations—two applications of the restriction operator and one final rank comparison—yielding a worst-case time complexity of (︀ |Ψ | · | Ψ | · | Ψ |︀) , which is typically governed by the size of Ψ . In contrast to the OBDD-based method, which may invoke apply up to | | times, our RBDD approach bounds calls to a constant.
Recall that each node stores the set of reachable ranks R( ). This additional cache—absent from a plain ADD—lets us answer several rank-specific questions without exploring the whole diagram: for instance, testing whether any world has rank is just the membership check ∈ R(root), and generating a witness of rank requires at most one edge choice per variable. Combined with the canonical reduce/apply machinery inherited from OBDDs, these cached rank sets yield the bounds in Table 2. As usual, |Ψ | and |Ψ | are assumed to be tiny compared with |Ψ |.
Operation on RBDDs Rank lookup () Existence of rank ( ∈ R(root)) Diagram equivalence (root ID comparison) Binary synthesis (apply) Conditioning by formula Entailment ( | ) Model counting () =
Time complexity
()
(
) (|Ψ |
System- inference can be driven by a direct SAT encoding, by per-level OBDDs, or by a single ranked ADD. The SAT route is parameter-free and benefits from decades of solver engineering, but every query incurs several solver calls whose worst-case time remains exponential. OBDDs move most work of -line: once the -vector is compiled, an inference requires at most | | apply calls, yielding large speed-ups when the diagram stays compact. Replacing the -vector by one ADD folds all ranks into one structure, cutting each query to three apply calls and enabling richer model-level questions. Because a fully reduced ADD is canonical for its variable ordering, two belief bases induce the same diagram if they are equivalent under the chosen OCF semantics; a single root -ID comparison thus gives the first tractable equivalence test for ranking-based formalisms. Neither decision-diagram method dominates the other—for some variable orderings an ADD can grow larger than the sum of its OBDD components—but in the worst case, where a query must examine every rank, the ADD per-query cost is likely to be much lower.
Aspect Compile efort Ordering sens.
Per-query cost Model queries
SAT 122.22
We evaluated ZinfOBDD, ZinfSAT, and inference with RBDDs on the synthetically generated CLKRPS004 dataset [24], which contains 100 belief bases with 10 queries each, spanning various (|Δ|, |Σ|) pairs. We used the CaDiCal solver for SAT [25], which uses CDCL, and CUDD for OBDD and ADD operations [26]. All were implemented in C++. Correctness of our implementation was also verified against the implementation used in [27]. The evaluation was run on an M1 Pro with 16GB of RAM. We used CUDD’s built in dynamic variable ordering algorithm to find a good variable ordering for representing the OBDDs and ADDs. For our small-scale preliminary analysis we restricted our experiments to belief bases with |Σ| ≤ 20. For fairness, the time required to construct each (Ψ | Ψ ) using diagram synthesis was included in the total inference time for each query.
Table 3 summarizes the average runtimes (in microseconds) over 1000 queries per setting. At smaller problem sizes, the OBDD and RBDD approaches are up to three orders of magnitude faster than the SAT based approach, demonstrating that, when OBDDs and RBDDs are relatively compact, they can significantly speed up inference. As |Δ| and |Σ| grow, however, the speedup narrows in both cases. This behavior is expected in synthetic data, as purely synthetic belief bases often lack the redundancies and symmetries OBDDs exploit for eficiency with real-world data. It is well-known that almost all formulas require at least 2/2 nodes even for the optimal ordering [28]. We also observe that the RBDD approach is consistently approximately half as eficient as the OBDD approach. This is likely because the queries generated for the dataset were not designed to enforce the worst case, where all ranks must be checked until a result is achieved. In most instances, both ZinfSAT and ZinfOBDD only needed to evaluate the lower ranks.
Nonetheless, our results indicate that both OBDDs and RBDDs could ofer significant performance advantages over SAT-based methods. Since large-scale, real-world conditional logic datasets remain rare, the exact gains are dificult to quantify and will depend on the specific application. At the very least, these findings demonstrate that these techniques warrant further investigation in real-world applications.
Decision diagrams represent a promising alternative to SAT-based methods for performing inference in System-Z reasoning. Using per-rank OBDDs significantly reduces query time, while employing a single MTBDD further restricts the worst-case computational cost to three apply operations, irrespective of the number of ranks. Our empirical evaluation on synthetic datasets demonstrates notable performance improvements, achieving of up to two orders of magnitude.
Two main factors currently influence the practical adoption of these methods: • Variable ordering: Existing heuristics are general-purpose and may not exploit characteristics unique to conditional logic. Tailoring these heuristics specifically for conditional logic could further reduce diagram sizes or prevent significant size growth. • Benchmarks: Real-world knowledge bases, such as regulatory rules or semantic-web ontologies, frequently contain structural redundancies absent in synthetic datasets. Developing and releasing comprehensive benchmark datasets is crucial for objectively evaluating these methods. Future work will focus on several key directions: 1. Developing structure-aware reordering methods to optimize variable ordering. 2. Investigating incremental compilation techniques to eficiently update diagrams in response to changes in the underlying belief base without complete reconstruction. 3. Extending the MTBDD framework to support more expressive ranking-based reasoning formalisms. 4. Conducting extensive experiments using large-scale, realistic datasets as they become available. 5. Exploring a broader range of knowledge compilation targets, including sentential decision diagrams (SDDs).
Overall, our findings indicate that decision-diagram approaches ofer reliable and eficient inference for defeasible reasoning, with considerable potential for further optimization and expansion to alternative knowledge compilation representations.
This work is based on the research supported in part by the National Research Foundation of South Africa (REFERENCE NO: SAI240823262612, AHPMDS250623326170).
During the preparation of this work, the authors used GPT-5 in order to: Improve writing style. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.