**Definition 7 (Individual Language-Based MIS Measure).** Let $M \in MI$ be a minimal inconsistent subset over activity set A and fixed trace length n. The individual language-based MIS measure is defined as:

$$I_{lang}^{MIS}(M) = \sum_{c \in M} \left( 1 - \frac{|L(c)|}{|A|^n} \right)$$

**Example 2.** Consider the set of activities $A = \{a, b, c\}$ and the trace length $n = 3$, resulting in $|L(c)| = 27$. Then, the individual language-based MIS measure for $M_2$ and $M_5$ can be calculated as follows:

$$I_{lang}^{MIS}(M_2) = \frac{18}{27} + \frac{15}{27} + \frac{6}{27} \approx 1.44$$

$$I_{lang}^{MIS}(M_5) = \frac{18}{27} + \frac{15}{27} + \frac{7}{27} \approx 1.48$$

Every MIS is minimal, so removing any one constraint yields a consistent subset. Therefore, similarly to the previously defined measure, we now consider the languages after all possible minimal repair operations based on element deletion.

**Definition 8 (Repair-Based Language MIS Measure).** Let $M \in MI$, with $k = |M|$. For each $i = 1, ..., k$, let $c_i \in M$ and define $M'_i = M \setminus \{c_i\}$, with $L(M'_i) \subseteq A^n$ denoting its language. We then define the following repair-based language MIS measure:

$$I_{lang-repair}^{MIS}(M) = \sum_{i=1}^{k} \left( 1 - \frac{|L(M'_i)|}{|A|^n} \right)$$

**Example 3.** Consider again the set of activities $A = \{a, b, c\}$ and the trace length $n = 3$, resulting in $|L(c)| = 27$. Then, the repair-based language MIS measure for $M_2$ and $M_5$ can be calculated as follows:

$$I_{lang-repair}^{MIS}(M_2) = \frac{19}{27} + \frac{25}{27} + \frac{22}{27} \approx 2.4$$

$$I_{lang-repair}^{MIS}(M_5) = \frac{19}{27} + \frac{23}{27} + \frac{25}{27} \approx 2.48$$

### 3.3. Structural Complexity MIS Measures

While temporal and language-based measures capture behavioral aspects of inconsistency, we also consider structural properties. Basic element-counting measures, such as the number of constraints ($I_p$) or the number of activities involved ($I_{at}$, adapted from the atom count in [8]), can be applied directly at the MIS level. To combine these aspects, we introduce two additional structural complexity measures inspired by [12]: a size measure and a density measure. These measures help distinguish structurally different MISes that are otherwise identical in temporal or semantic terms. For example, $M_2$ and $M_6$ (cf. Table 2) involve similar constraints and have comparable behavior, but $M_6$ references an additional activity c. This structural difference is captured by activity-based and density-based metrics, which makes them useful for prioritizing MISes based on modeling complexity. Other structural metrics, such as constraint variability and separability (cf. [12]), are excluded here, as they do not satisfy the required *Dominance* property.

**Definition 9 (Structural Complexity MIS Measures).** Let $M \in MI$ be a minimal inconsistent subset and let $A_M \subseteq A$ denote the set of activities that appear in any constraint in M. Then:

$$I_p^{MIS}(M) = |M|$$

$$I_a^{MIS}(M) = |A_M|$$

$$I_{size}^{MIS}(M) = |M| + |A_M|$$

$$I_{density}^{MIS}(M) = \frac{|M|}{|A_M|}$$

**Example 4.** Independent of the set of activities A and the trace length n, the different structural complexity MIS measures for $M_2$ and $M_6$ can be calculated as follows:

$$I_p^{MIS}(M_2) = 3$$

$$I_a^{MIS}(M_2) = 2$$

$$I_{size}^{MIS}(M_2) = 5$$

$$I_{density}^{MIS}(M_2) = 1.5$$

$$I_p^{MIS}(M_6) = 3$$

$$I_a^{MIS}(M_6) = 3$$

$$I_{size}^{MIS}(M_6) = 6$$

$$I_{density}^{MIS}(M_6) = 1$$
## 4. Conclusion

This paper takes an initial step toward a more fine-grained perspective on inconsistencies in DPMs by proposing the idea of MIS-level inconsistency measures. Rather than evaluating entire constraint sets, these measures aim to quantify inconsistency at the level of individual MISes. Specifically, we suggest three categories of MIS measures (temporal, language-based, and structural) and present illustrative examples for each. These measures are intended to demonstrate the potential of MIS-level evaluation, while their theoretical grounding, formal validation, and empirical testing remain important directions for future work. First, suitable rationality postulates must be developed to formally underpin the concept of MIS-level measures and guide their design. Second, the proposed measures require refinement and extension to better capture domain-specific properties. Third, a broader evaluation across varied constraint sets, model sizes, and real-world scenarios is needed to assess scalability and relevance. Nonetheless, this work provides a foundational step toward a general framework for measuring and reasoning about MISes, and ultimately, toward interpretable and actionable inconsistency management.

## Acknowledgments

This paper was funded by the Deutsche Forschungsgemeinschaft (grant number DE 1983/9-3).

## Declaration on Generative AI

The authors used gpt-4o for grammar and spelling check, as well as formatting assistance.

## References

[1] C. Di Ciccio, M. Montali, Declarative Process Specifications: Reasoning, Discovery, Monitoring, in: Process Mining Handbook, volume 448, Springer Int. Publishing, 2022, pp. 108–152.

[2] C. Di Ciccio, F. M. Maggi, M. Montali, J. Mendling, Resolving Inconsistencies and Redundancies in Declarative Process Models, Information Systems 64 (2017) 425–446.

[3] C. Corea, I. Kuhlmann, M. Thimm, J. Grant, Paraconsistent reasoning for inconsistency measurement in declarative process specifications, Information Systems 122 (2024) 102347.

[4] M. Thimm, On the Evaluation of Inconsistency Measures, in: Measuring Inconsistency in Information, volume 73 of *Studies in Logic*, College Publications, 2018, p. 42.

[5] S. Nagel, P. Delfmann, Interactive Resolution of Inconsistencies in Declarative Process Models, in: Proceedings der 19. Internationalen Tagung der Wirtschaftsinformatik (WI 2024), 2024.

[6] S. Nagel, P. Delfmann, Exploring Cognitive Effects of Inconsistency Characteristics on Understanding Inconsistencies in Declarative Process Models, in: Proceedings of the 57th Hawaii International Conference on System Sciences (HICSS), 2024.

[7] M. Thimm, Inconsistency Measurement, in: Proceedings of the 13th International Conference on Scalable Uncertainty Management, 2019, pp. 9–23.

[8] C. Corea, J. Grant, M. Thimm, Measuring Inconsistency in Declarative Process Specifications, volume 13420, Springer, 2022, pp. 289–306.

[9] C. Corea, M. Thimm, Towards Inconsistency Measurement in Business Rule Bases, in: Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020), 2020.

[10] A. Hunter, S. Konieczny, Measuring Inconsistency through Minimal Inconsistent Sets, AAAI Press, Sydney, Australia, 2008, pp. 358–366.

[11] A. Hunter, S. Konieczny, On the measure of conflicts: Shapley Inconsistency Values, Artificial Intelligence 174 (2010) 1007–1026.

[12] A. A. Andaloussi, A. Burattin, T. Slaats, E. Kindler, B. Weber, Complexity in declarative process models: Metrics and multi-modal assessment of cognitive load, Expert Systems with Applications 233 (2023).
# A MaxSAT-Based Approach for Computing Inconsistency Degrees in Linear Temporal Logic on Fixed Traces

Isabelle Kuhlmann

University of Hagen, Germany

**Abstract**

We present an algorithmic approach for computing inconsistency values in linear temporal logic on fixed traces (i. e., finite traces of fixed length). In an experimental evaluation, we demonstrate that our approach, which is based on Maximum satisfiability (MaxSAT) solving, can overall outperform the current state-of-the-art approaches based on answer set programming.

**Keywords**

Inconsistency measurement, MaxSAT solving, linear temporal logic

## 1. Introduction

The development of applications in Artificial Intelligence is highly data- and information-dependent. However, it is hardly possible to avoid the occurrence of conflicting (in other words, *inconsistent*) information—think, e. g., of contradictory expert assessments or conflicting statements mined by a rule mining algorithm. The field of *inconsistency measurement* [1, 2] offers a quantitative perspective on this matter by providing numerical values that evaluate the level of inconsistency of a given knowledge base. Thus, inconsistency measures are analytical tools that can, e. g., aid the comparison of alternative formalizations or assist automated reasoning mechanisms.

Inconsistency measures have been developed for a wide range of formalisms and application domains. In this work, we focus on inconsistency measurement within the framework of *linear temporal logic on fixed traces (LTL<sub>ff</sub>)* (see Section 2.1 for a formal definition). Specifically, we examine the measures introduced by Corea et al. [3], which were designed with applications in business process management (more specifically, declarative process specifications) in mind. A distinctive feature of these measures is their time-sensitive nature, meaning they take into account the specific temporal states in which conflicts occur. Our work builds directly upon the foundation laid by Corea et al., who proposed an algorithmic approach based on Answer Set Programming (ASP) and showed that they are practically feasible. However, prior research on inconsistency measurement in propositional logic has shown that approaches based on maximum satisfiability (MaxSAT) solving tend to outperform ASP-based methods in practice [4]. Moreover, Xiao et al. [5] also make use of MaxSAT to compute several inconsistency measures for propositional logic, which are based on multi-valued semantics. Motivated by these findings, our goal is to investigate whether such performance advantages as indicated by Niskanen et al. [4] can also be observed when applying MaxSAT techniques to LTL<sub>ff</sub> inconsistency measures.

Thus, our main contribution consists of a MaxSAT-based approach for computing the two inconsistency measures for LTL<sub>ff</sub> proposed by Corea et al. [3]. In addition, we implemented our approach and provide an experimental evaluation, in which we demonstrate that our newly proposed approach can overall outperform the current state-of-the-art ASP-based method [6].

In the remainder of this paper, we provide a basic overview of inconsistency measurement in LTL<sub>ff</sub> and MaxSAT solving in Section 2, introduce our MaxSAT-based approach in Section 3, conduct an experimental evaluation in Section 4, and conclude in Section 5.

IM'25@ECSQARU: 1st International Workshop on Inconsistency Measurement, September 23, 2025, Hagen, Germany

<figure><img src="image_26.png" /></figure>

isabelle.kuhlmann@fernuni-hagen.de (I. Kuhlmann)

<figure><img src="image_27.png" /></figure>

0000-0001-9636-122X (I. Kuhlmann)

<figure><img src="image_28.png" /></figure>

© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
## 2. Preliminaries

In this section, we describe the basic concepts this work is based on. More specifically, we cover linear temporal logic on fixed traces (LTL<sub>ff</sub>) in Section 2.1, define the inconsistency measures for LTL<sub>ff</sub> introduced by Corea et al. [3] in Section 2.2, and briefly address MaxSAT solving in Section 2.3.

### 2.1. Linear Temporal Logic on Fixed Traces

Let At be a set of propositional symbols, and $t_0, ..., t_m$ a linear sequence of temporal states. In this work we consider sequences of finite [7] and fixed length, and refer to the corresponding fragment of LTL as *linear temporal logic on fixed traces* (LTL<sub>ff</sub>) [3]. Formulas are closed under the unary operator **X** (*next*) and the binary operator **U** (*until*), in addition to the classical operators **∧** (conjunction), **∇** (disjunction), and **¬** (negation). We can construct any LTL<sub>ff</sub> formula $\phi$ using the grammar rule $\phi ::= a | (\neg\phi) | (\phi_1 \land \phi_2) | (\phi_1 \lor \phi_2) | (\mathbf{X}\phi) | (\phi_1 \mathbf{U}\phi_2)$, with $a \in \text{At}$. A formula $\mathbf{X}\phi$ evaluates to true if $\phi$ holds in the next state, and a formula $\phi_1 \mathbf{U}\phi_2$ evaluates to true if $\phi_1$ holds until a state in which $\phi_2$ holds. We also consider the auxiliary operators **F** (*eventually*) and **G** (*globally*). A formula $\mathbf{F}\phi$ can be understood as “$\mathbf{F}\phi$ evaluates to true if $\phi$ evaluates to true eventually”, i. e., if $\phi$ becomes true in the current or at least one of the following states. A formula $\mathbf{G}\phi$ represents that $\phi$ must be true in the current and all following states. Formally, we define $\mathbf{F}\phi$ as $\top\mathbf{U}\phi$, and $\mathbf{G}\phi$ as $\neg\mathbf{F}\neg\phi$. We denote a finite set $\mathcal{K}$ of LTL<sub>ff</sub> formulas as an (LTL<sub>ff</sub>) *knowledge base*, and the set of all LTL<sub>ff</sub> knowledge bases as $\mathcal{K}$.

Furthermore, let $\mathcal{T} := \{t_0, ..., t_m\}$. An LTL<sub>ff</sub> interpretation $\omega$ w.r.t. a set of atoms At is a function mapping each state $t$ and atom $a$ to $T$ (true) or $F$ (false), denoted as $\omega(t, a) = T$, or $\omega(t, a) = F$, respectively. Thus, formally, we have $\omega : \mathcal{T} \times \text{At} \to \{T, F\}$. A formula $\phi$ is *satisfied* by an interpretation $\omega$, denoted $\omega \models \phi$, if and only if $\omega, t_0 \models \phi$. Further, $\omega, t_i \models \phi$ is inductively defined as

$$
\begin{align*}
\omega, t_i \models a \text{ if and only if } \omega(t_i, a) = T \text{ for } a \in \text{At} \\
\omega, t_i \models \neg\phi \text{ if and only if } \omega, t_i \not\models \phi \\
\omega, t_i \models \phi_1 \land \phi_2 \text{ if and only if } \omega, t_i \models \phi_1 \text{ and } \omega, t_i \models \phi_2 \\
\omega, t_i \models \phi_1 \lor \phi_2 \text{ if and only if } \omega, t_i \models \phi_1 \text{ or } \omega, t_i \models \phi_2 \\
\omega, t_i \models \mathbf{X}\phi \text{ if and only if } i < m \text{ and } \omega, t_{i+1} \models \phi \\
\omega, t_i \models \phi_1 \mathbf{U}\phi_2 \text{ if and only if either } \omega, t_i \models \phi_1 \text{ and } \omega, t_i \models \phi_2 \text{ or} \\
\qquad \omega, t_j \models \phi_2 \text{ and } \omega, t_k \models \phi_1 \quad \forall k \in \{i, ..., j-1\} \text{ with } j \in \{i+1, ..., m\}
\end{align*}
$$

w.r.t. any interpretation $\omega$, and $i \in \{0, ..., m\}$. We extend this concept to LTL<sub>ff</sub> knowledge bases, and define that an interpretation $\omega$ satisfies a knowledge base $\mathcal{K} \in \mathcal{K}$ if and only if $\forall \phi \in \mathcal{K} : \omega \models \phi$. An interpretation that satisfies a formula $\phi$ (or knowledge base $\mathcal{K}$) is also referred to as a *model of* $\phi$ (or $\mathcal{K}$), and the set of all models of $\phi$ (or $\mathcal{K}$) is called Mod($\phi$) (resp. Mod($\mathcal{K}$)). We also refer to a satisfiable formula or knowledge base as *consistent*, and to an unsatisfiable formula or knowledge base as *inconsistent*.

### 2.2. Inconsistency Measurement in LTL<sub>ff</sub>

As in the context of propositional logic, an *inconsistency measure* for LTL<sub>ff</sub> is simply a function that maps a knowledge base to a numerical value. Note that, however, in the LTL<sub>ff</sub> case, we have the index $m$ of the final state as an additional input parameter.

**Definition 1.** An LTL<sub>ff</sub> inconsistency measure is a function $\mathcal{I} : \mathcal{K} \times \mathbb{N}_0 \to \mathbb{R}_{\ge 0}^\infty$.

Corea et al. [3] define a Priest-inspired [8] three-valued semantics for LTL<sub>ff</sub> as a basis for their LTL<sub>ff</sub> inconsistency measures. Given a signature At, a three-valued interpretation $\omega^3$ for LTL<sub>ff</sub> is a function that maps each state $t$ and atom $a \in \text{At}$ to one of the truth values $T$, $F$ or $B$. Thus, formally, $\omega^3 : \mathcal{T} \times \text{At} \to \{T, F, B\}$ with $T$ and $F$ corresponding to the classical truth values *true* and *false*,
respectively, and B (indicating both) denoting a conflict. Corea et al. [3] assign $\omega^3(\phi) = \omega^3(t_0, \phi)$ with $\omega^3(t_i, \phi)$ being inductively defined as follows for any interpretation $\omega^3$ and state $t_i \in \{t_0, \dots, t_m\}$:

$$
\begin{align*}
\omega^3(t_i, a) &= \omega^3(t_i, a) \text{ for } a \in \text{At} \\
\omega^3(t_i, \neg\phi) &= \begin{cases} T & \text{if } \omega^3(t_i, \phi) = F \\ F & \text{if } \omega^3(t_i, \phi) = T \\ B & \text{if } \omega^3(t_i, \phi) = B \end{cases} \\
\omega^3(t_i, \phi_1 \wedge \phi_2) &= \begin{cases} T & \text{if } \omega^3(t_i, \phi_1) = \omega^3(t_i, \phi_2) = T \\ F & \text{if } \omega^3(t_i, \phi_1) = F \text{ or } \omega^3(t_i, \phi_2) = F \\ B & \text{otherwise} \end{cases} \\
\omega^3(t_i, \phi_1 \vee \phi_2) &= \begin{cases} T & \text{if } \omega^3(t_i, \phi_1) = T \text{ or } \omega^3(t_i, \phi_2) = T \\ F & \text{if } \omega^3(t_i, \phi_1) = \omega^3(t_i, \phi_2) = F \\ B & \text{otherwise} \end{cases} \\
\omega^3(t_i, \mathbf{X}\phi) &= \begin{cases} \omega^3(t_{i+1}, \phi) & \text{if } i < m \\ F & \text{otherwise} \end{cases} \\
\omega^3(t_i, \phi_1 \mathbf{U}\phi_2) &= \begin{cases} T & \text{if } \omega^3(t_i, \phi_1 \wedge \phi_2) = T \text{ or if there exists } j \in \{i+1, \dots, m\} \\ B & \text{if } \omega^3(t_i, \phi_1 \wedge \phi_2) = B \text{ or if there exists } j \in \{i+1, \dots, m\} \\ F & \text{otherwise} \end{cases}
\end{align*}
$$

A three-valued LTL<sub>ff</sub> interpretation $\omega^3$ satisfies a formula $\phi$, denoted by $\omega^3 \Vdash^3 \phi$, if and only if $\omega^3(\phi, t_0) \in \{T, B\}$. A three-valued interpretation $\omega^3$ satisfies a knowledge base $\mathcal{K}$ (i. e., $\omega^3$ is a model of $\mathcal{K}$) if and only if $\omega^3 \Vdash^3 \phi \forall \phi \in \mathcal{K}$. We denote the set of all three-valued models of $\mathcal{K}$ as Mod<sup>3</sup>(<sup>*K*</sup>).

**Example 1.** Consider the knowledge base $\mathcal{H}_1 = \{\mathbf{X}x, \mathbf{X}\neg x\}$, and let $m = 1$. Clearly, $\mathcal{H}_1$ is inconsistent under classical LTL<sub>ff</sub> semantics, as $x$ would have to evaluate to $T$ in $t_1$ in order to satisfy $\mathbf{X}x$, however it would have to evaluate to $F$ in $t_1$ to satisfy $\mathbf{X}\neg x$. Consider now the three-valued interpretation $\omega^3$ with $\omega^3(t_0, x) = T$ and $\omega^3(t_1, x) = B$. Consequently, $\omega^3(t_0, \mathbf{X}x) = B$, as $x$ evaluates to $B$ in the next state (i. e., $t_1$), and likewise $\omega^3(t_0, \mathbf{X}\neg x) = B$. Thus, each formula in $\mathcal{H}_1$ is satisfied under the previously defined three-valued semantics, and therefore $\omega^3 \Vdash^3 \mathcal{H}_1$. In other words, $\mathcal{H}_1$ is consistent under three-valued semantics for LTL<sub>ff</sub>.

The idea behind the LTL time inconsistency measure [3] is to count the number of states affected by inconsistency. This approach is inspired by the *drastic* inconsistency measure [9] for propositional logic, which evaluates to 0 if the given knowledge base is consistent and 1 otherwise. We define the set of states affected by inconsistency as the set of states in which at least one atom is assigned truth value $B$ under a given three-valued interpretation $\omega^3$. Formally, we denote this set as AffectedStates($\omega^3$) = $\{t \mid \exists a : \omega^3(t, a) = B\}$. Based on this notion, we can now define the LTL time inconsistency measure.

**Definition 2.** The LTL time inconsistency measure $\mathcal{I}_t^{\text{LTL}} : \mathbb{K} \times \mathbb{N}_0 \to \mathbb{N}_0$ is defined as

$$
\mathcal{I}_t^{\text{LTL}}(\mathcal{K}, m) = \min\{|\text{AffectedStates}(\omega^3)| \mid \omega^3 \in \text{Mod}^3(\mathcal{K})\}
$$

for any $\mathcal{H} \in \mathbb{K}$ and $m \in \mathbb{N}_0$, if there exists $\omega^3$ with $\omega^3 \Vdash^3 \mathcal{H}$, and $\mathcal{I}_t^{\text{LTL}}(\mathcal{H}, m) = \infty$ otherwise.

The LTL contension inconsistency measure [3] is, as the name suggests, inspired by the contension inconsistency measure for propositional logic [10], and, in essence, aims to find the minimum number of atoms that have to be assigned $B$ across all states, in order render a given knowledge base consistent. Let $\mathcal{H} \in \mathbb{K}$, let $\mathcal{T} = \{t_0, \dots, t_m\}$ be the given sequence of states, and let At($\mathcal{H}$) denote the signature of $\mathcal{H}$. For a given three-valued interpretation $\omega^3$, we define Conflictbase($\omega^3$) = $\{(t, a) \mid \omega^3(t, a) = B\}$ with $t \in \mathcal{T}$, and $a \in \text{At}(\mathcal{H})$.
**Definition 3.** The LTL contension inconsistency measure $\mathcal{I}_c^{\text{LTL}}: K \times \mathbb{N}_0 \to \mathbb{N}_0$ is defined as

$$ \mathcal{I}_c^{\text{LTL}}(\mathcal{K}, m) = \min\{|\text{Conflictbase}(\omega^3)| \mid \omega^3 \in \text{Mod}^3(\mathcal{K})\} $$

for any $\mathcal{K} \in K$ and $m \in \mathbb{N}_0$, if there is $\omega^3$ with $\omega^3 \nleq^3 \mathcal{K}$ and $\mathcal{I}_c^{\text{LTL}}(\mathcal{K}, m) = \infty$ otherwise.

**Example 2.** Consider the knowledge base $\mathcal{K}_2 = \{\mathbf{G}x, \mathbf{G} \neg x, \mathbf{X}y, \mathbf{X} \neg y\}$, and let $m = 2$ be the index of the final state. As each state $t_0, t_1, t_2$ is affected by the conflict between the first two formulas, we have AffectedStates = $\{t_0, t_1, t_2\}$, and we get $\mathcal{I}_t^{\text{LTL}}(\mathcal{K}_2) = |\{t_0, t_1, t_2\}| = 3$. Further, $t_1$ is affected by the conflict between $\mathbf{G}x$ and $\mathbf{G} \neg x$ on the one hand, and by the conflict between $\mathbf{X}y$ and $\mathbf{X} \neg y$ on the other hand. Thus, for an interpretation $\omega^3$ satisfying $\mathcal{K}_2$ under three-valued semantics, Conflictbase($\omega^3$) has to contain at least $\{(t_0, x), (t_1, x), (t_2, x), (t_1, y)\}$. Thus, $\mathcal{I}_c^{\text{LTL}}(\mathcal{K}_2) = |\{(t_0, x), (t_1, x), (t_2, x), (t_1, y)\}| = 4$.

## 2.3. Maximum Satisfiability Solving

While the Boolean satisfiability (SAT) problem is the problem of deciding whether a given CNF formula is satisfiable, the motivation behind the maximum satisfiability problem is to gain more insight into unsatisfiable cases. More precisely, it is the optimization problem of finding an assignment of truth values that satisfies a maximum number of clauses of given a formula in CNF (for an overview on this topic, see, e. g., [11]). A further generalization of MaxSAT is partial MaxSAT [12]. Instead of having only one formula (i. e., one set of clauses) of which we aim to satisfy as many clauses as possible, we have two separate sets, namely a set of hard clauses, denoted HC, and a set of soft clauses, denoted SC. The objective of partial MaxSAT is to find an interpretation that satisfies all hard clauses and a maximum number of soft clauses. Conversely, partial MaxSAT can also be viewed as the problem of finding an interpretation such that all hard clauses are satisfied and only a minimum number of soft clauses are falsified. We also refer to the number of (soft) clauses that are falsified as the cost of the given (partial) MaxSAT instance (HC, SC). A partial MaxSAT instance may have multiple feasible solutions, which are solutions in which all hard clauses are satisfied. An optimal solution, on the other hand, is one in which all hard clauses are satisfied and a maximum number of soft clauses is satisfied (or, respectively, a minimum number of soft clauses is falsified, i. e., the cost is minimal). We denote the optimal cost, i. e., the cost of this optimal solution (the number of falsified soft clauses) as cost(HC, SC). If HC is unsatisfiable, we define cost(HC, SC) = $\infty$.

Note that there exist numerous high-performance MaxSAT solvers in the literature. For an overview, see, e. g., the most recent results of the annual MaxSAT evaluation [13].<fnref n="1" />

## 3. MaxSAT Encodings

We now show how we encoded the problems of computing $\mathcal{I}_t^{\text{LTL}}(\mathcal{K}, m)$ and $\mathcal{I}_c^{\text{LTL}}(\mathcal{K}, m)$ w.r.t. a given knowledge base $\mathcal{K}$ and a final state $t_m$ as MaxSAT problems. More precisely, for $\mathcal{I}_t^{\text{LTL}}$ we show how to define a set of hard clauses $\text{HC}_t^{\text{LTL}}(\mathcal{K}, m)$ and a set of soft clauses $\text{SC}_t^{\text{LTL}}(\mathcal{K}, m)$, which make up the MaxSAT instance $(\text{HC}_t^{\text{LTL}}(\mathcal{K}, m), \text{SC}_t^{\text{LTL}}(\mathcal{K}, m))$. In the same fashion, for $\mathcal{I}_c^{\text{LTL}}$, we have $(\text{HC}_c^{\text{LTL}}(\mathcal{K}, m), \text{SC}_c^{\text{LTL}}(\mathcal{K}, m))$.

First, since a MaxSAT solver requires its input formulas to be in propositional logic CNF, but we are dealing with LTL$_{ff}$ formulas of arbitrary form, we apply an intermediate step, in which we inductively transform each LTL$_{ff}$ formula $\phi \in \mathcal{K}$ to a propositional logic formula $\phi^{\text{PL}}$. The idea behind this transformation is to model the temporal component by introducing atoms $a_i$ for each state $t_i$ (with $i \in \{0, ..., m\}$) for all atoms $a \in \text{At}(\mathcal{K})$, and to represent the temporal operators by means of classical operators only.

Let $\mathcal{K}$ be the given LTL$_{ff}$ knowledge base, let $m \in \mathbb{N}_0$ be the index of the final state, and let $K^{\text{PL}}$ be the set of all propositional knowledge bases. We denote the transformation of $\mathcal{K}$ to a propositional knowledge base $\mathcal{K}^{\text{PL}}$ as a function $\lambda: K \times \mathbb{N}_0 \to K^{\text{PL}}$ that satisfies $\lambda(\mathcal{K}, m) = \mathcal{K}^{\text{PL}}$ via the subsequent rules:

<footnote n="1">¹https://maxsat-evaluations.github.io/</footnote>
1. For each atom a we introduce $m+1$ new variables. To be precise, for each a, we introduce variables $a_i$, with $i \in \{0, ..., m\}$.

2. By $\langle\phi\rangle_t$, we denote the initial state $t$ of a formula $\phi$. For each $\phi \in \mathcal{K}$, we set $t = 0$.

3. If a (sub-)formula $\phi$ consists of an atom $a$, we have $\lambda(\langle a \rangle_t) = a_t$.

4. If a (sub-)formula is a negation $\neg\phi$, we set $\lambda(\langle\neg\phi\rangle_t) = \neg\lambda(\langle\phi\rangle_t)$.

5. If a (sub-)formula is of the form $\phi_1 \bowtie \phi_2$ with $\bowtie \in \{\wedge, \vee, \rightarrow, \leftrightarrow\}$, we set $\lambda(\langle\phi_1 \bowtie \phi_2\rangle_t) = \lambda(\langle\phi_1\rangle_t) \bowtie \lambda(\langle\phi_2\rangle_t)$.

6. If a (sub-)formula is of the form $\mathbf{X}\phi$ and $t < m$, we set $\lambda(\langle\mathbf{X}\phi\rangle_t) = \lambda(\langle\phi\rangle_{t+1})$, and if $t \ge m$, we set $\lambda(\langle\mathbf{X}\phi\rangle_t) = \perp$.

7. If a (sub-)formula is of the form $\phi_1\mathbf{U}\phi_2$, we set

$$ \lambda(\langle\phi_1\mathbf{U}\phi_2\rangle_t) = (\lambda(\langle\phi_1\rangle_t) \wedge \lambda(\langle\phi_2\rangle_t)) \vee \bigvee_{i=t}^{m-1} \left( \left( \bigwedge_{j=t}^{i} \lambda(\langle\phi_1\rangle_j) \right) \wedge \lambda(\langle\phi_2\rangle_{i+1}) \right). $$

8. If a (sub-)formula is of the form $\mathbf{G}\phi$, we set

$$ \lambda(\langle\mathbf{G}\phi\rangle_t) = \bigwedge_{i=t}^{m} \lambda(\langle\phi\rangle_i). $$

9. If a (sub-)formula is of the form $\mathbf{F}\phi$, we set

$$ \lambda(\langle\mathbf{F}\phi\rangle_t) = \bigvee_{i=t}^{m} \lambda(\langle\phi\rangle_i). $$

**Example 3.** Consider the knowledge base $\mathcal{H}_3 = \{\overbrace{x \wedge y, \quad \mathbf{X}y, \quad \overbrace{F(x \to (y\mathbf{U}z))}^{\phi_1}}^{\phi_1}, \overbrace{\phi_2}^{\phi_2}, \overbrace{\phi_3}^{\phi_3}\}$, and let $m = 3$.

We transform $\mathcal{H}_3$ to $\mathcal{H}_3^{\text{PL}}$ by applying $\lambda$ via rules 1-9 as described above to each formula. Thus, we initially set each formula's state to 0 and get $\mathcal{H}_3^{\text{PL}} = \{\lambda(\langle x \wedge y \rangle_0), \lambda(\langle \mathbf{X}y \rangle_0), \lambda(\langle \mathbf{F}(x \to (y\mathbf{U}z)) \rangle_0)\}$. We now proceed by replacing each atom $a \in \text{At}(\mathcal{H}_3)$ with variables $a_i$, $i \in \{0, ..., m\}$, according to the aforementioned rules. Since $\phi_1$ is a conjunction and does not contain any LTL-specific operators, we apply rule 5 and get $\lambda(\langle x \wedge y \rangle_0) = \lambda(\langle x \rangle_0) \wedge \lambda(\langle y \rangle_0)$. We subsequently apply rule 3 and get $\lambda(\langle x \rangle_0) \wedge \lambda(\langle y \rangle_0) = x_0 \wedge y_0$.

As for $\phi_2$, we apply rule 6, and get $\lambda(\langle \mathbf{X}y \rangle_0) = \lambda(\langle y \rangle_{0+1}) = \lambda(\langle y \rangle_1)$. We then apply rule 3 again and obtain $\lambda(\langle y \rangle_1) = y_1$.

Lastly, for $\phi_3$, we use rule 9 (and subsequently rules 5 and 3) to remove the $\mathbf{F}$ operator and get

$$ \lambda(\langle\mathbf{F}(x \to (y\mathbf{U}z))\rangle_0) = \bigvee_{i=0}^{3} \lambda(\langle x \to (y\mathbf{U}z)\rangle_i) = \bigvee_{i=0}^{3} (\lambda(\langle x \rangle_i) \to \lambda(\langle y\mathbf{U}z \rangle_i)) = \bigvee_{i=0}^{3} (x_i \to \lambda(\langle y\mathbf{U}z \rangle_i)). $$

We then apply rule 7 to deal with the $\mathbf{U}$ operator (and subsequently apply rule 3), which finally yields

$$ \lambda(\langle\phi_3\rangle_0) = \bigvee_{i=0}^{3} \left( x_i \to \left( (y_i \wedge z_i) \vee \bigvee_{j=i}^{2} \left( \left( \bigwedge_{k=i}^{j} y_k \right) \wedge z_{j+1} \right) \right) \right). $$

As a first step towards the actual MaxSAT encodings for $\mathcal{I}_t^{\text{LTL}}$ and $\mathcal{I}_c^{\text{LTL}}$, given a knowledge base $\mathcal{K} \in \mathcal{K}$ and an index $m$ of the final state, we compute $\phi_t^{\text{PL}} = \lambda(\phi, m)$ according to the procedure described above w.r.t. each $\phi \in \mathcal{K}$, and therefore obtain $\mathcal{H}_3^{\text{PL}} = \lambda(\mathcal{K})$. We replace each occurrence of $a_i \in \text{At}(\mathcal{H}_3^{\text{PL}})$ (with $i \in \{0, ..., m\}$) by the corresponding $a_i^j$, with $j \in \{1, ..., \#\text{occ}(a_i, \mathcal{H}_3^{\text{PL}})\}$ and denote the resulting knowledge base as $\mathcal{H}_3^{\text{PL}'}$. Now we can use the Tseitin transformation [14] in order to transform $\mathcal{H}_3^{\text{PL}'}$ to CNF. We denote the resulting knowledge base as $\mathcal{H}_3^{\text{PL}'}_T$, and the formulas contained in it as $\phi_T^{\text{PL}'}$. Each $\phi_T^{\text{PL}'}$ is then added as a hard clause to $\text{HC}_T^{\text{LTL}}(\mathcal{K}, m)$, or $\text{HC}_c^{\text{LTL}}(\mathcal{K}, m)$, respectively.

Note that the overall idea of the encodings (aside from the previously described computation of propositional formulas corresponding to the input LTL$_{ff}$ formulas) is inspired by the work by Niskanen et al. [4], who developed MaxSAT encodings for a range of inconsistency measures in propositional
logic. Specifically, we also adopt their characterization of the contension measure [10] for propositional logic and adapt it to the LTL<sub>ff</sub> variant. To be precise, the propositional contension inconsistency measure, which calculates the minimum number of atoms in the signature that need to be set to truth value *B* under Priest's three-valued logic in order to render the given knowledge base consistent under three-valued semantics, can also be viewed as the minimum number of atoms, of which at least one occurrence needs to be replaced by either ⊤ or ⊥ (i. e., which needs to be *forgotten*; see also the work on the forgetting-based inconsistency measure by Besnard [15]) in order to make the knowledge base consistent under classical propositional semantics. Likewise, we can view the LTL contension measure as the minimal number of atoms *across all states*, of which at least one occurrence is forgotten, while it holds that *K* is consistent under classical LTL<sub>ff</sub> semantics. Similarly, we view *I*<sub>t</sub><sup>LTL</sup> as the number of states in which at least one atom occurrence needs to be forgotten in order to make *K* consistent (under classical LTL<sub>ff</sub> semantics).

In order to compute $\mathcal{I}_t^{\text{LTL}}(\mathcal{K}, m)$, we add variables $e_i$ for each $i \in \{0, \dots, m\}$, which can only be set to true if each $a_i^j$ (with $j \in \{1, \dots, \#\text{occ}(a_i, \mathcal{K}^{\text{PL}})\}$) has the same truth value as the corresponding $a_i$. Thus, intuitively, $e_i$ can only become true if no occurrence of any atom is forgotten in state $i$. Formally, for each $i \in \{0, \dots, m\}$, we add the following hard clause to $\text{HC}_t^{\text{LTL}}(\mathcal{K}, m)$:

$$e_i \rightarrow \bigwedge_{a \in \text{At}(\mathcal{K})} \bigwedge_{j=1}^{\#\text{occ}(a_i, \mathcal{K}^{\text{PL}})} (a_i^j \leftrightarrow a_i)$$

Hence, the set of hard clauses is defined as:

$$\text{HC}_t^{\text{LTL}}(\mathcal{K}, m) = \bigwedge_{\phi \in \mathcal{K}} \phi_T^{\text{PL}'} \wedge \bigwedge_{i=0}^{m} \left( e_i \rightarrow \bigwedge_{a \in \text{At}(\mathcal{K})} \bigwedge_{j=1}^{\#\text{occ}(a_i, \mathcal{K}^{\text{PL}})} (a_i^j \leftrightarrow a_i) \right)$$

Now we can minimize the number of states in which at least one atom occurrence is forgotten by adding each $e_i$ as a unit soft clause. Hence, for each $i \in \{0, \dots, m\}$, we add $e_i$ to $\text{SC}_t^{\text{LTL}}(\mathcal{K}, m)$. Thus, the set of soft clauses is defined as:

$$\text{SC}_t^{\text{LTL}}(\mathcal{K}, m) = \bigwedge_{i=0}^{m} e_i$$

According to the definition of $\mathcal{I}_t^{\text{LTL}}$ (see Definition 2), $\mathcal{I}_t^{\text{LTL}}(\mathcal{K}, m) = \infty$ if there exists no three-valued interpretation $\omega^3$ with $\omega^3 \vDash^3 \mathcal{K}$. This can only happen if a formula $\phi$ contains (nested) $\mathbf{X}$ operators, such that the number of required states exceeds $m$, i. e., if the depth $\delta$ of $\phi$ is greater than $m$. E. g., the formula $\mathbf{X}(\mathbf{X}a)$, with $\delta(\mathbf{X}(\mathbf{X}a)) = 2$, is not satisfiable under three-valued semantics if $m = 1$. In our encoding, we handle this via rule 6 as described above, and insert $\perp$ whenever such a situation occurs. Thus, the transformed formula, and, by extension, the knowledge base $\mathcal{K}^{\text{PL}}$, becomes unsatisfiable. Consequently, the MaxSAT instance $(\text{HC}_t^{\text{LTL}}(\mathcal{K}, m), \text{SC}_t^{\text{LTL}}(\mathcal{K}, m))$ is unsatisfiable as well, and cost$(\text{HC}_t^{\text{LTL}}(\mathcal{K}, m), \text{SC}_t^{\text{LTL}}(\mathcal{K}, m)) = \infty$.

To compute $\mathcal{I}_c^{\text{LTL}}$, we add variables $e_{a,i}$ for each atom $a \in \text{At}(\mathcal{K})$ and each $i \in \{0, \dots, m\}$, that can only be set to $T$ if each $a_i^j$ (with $j \in \{1, \dots, \#\text{occ}(a_i, \mathcal{K}^{\text{PL}})\}$) has the same truth value as $a_i$. The idea behind this is that $e_{a,i}$ can only be set to $T$ if no occurrence of atom $a$ is forgotten in state $i$. Hence, for each $i$ we add

$$\bigwedge_{a \in \text{At}(\mathcal{K})} \left( e_{a,i} \rightarrow \bigwedge_{j=1}^{\#\text{occ}(a_i, \mathcal{K}^{\text{PL}})} (a_i^j \leftrightarrow a_i) \right)$$

to $\text{HC}_c^{\text{LTL}}(\mathcal{K}, m)$. Thus, the set of hard clauses is determined as follows:

$$\text{HC}_c^{\text{LTL}}(\mathcal{K}, m) = \bigwedge_{\phi \in \mathcal{K}} \phi_T^{\text{PL}'} \wedge \bigwedge_{i=0}^{m} \left( e_{a,i} \rightarrow \bigwedge_{a \in \text{At}(\mathcal{K})} \bigwedge_{j=1}^{\#\text{occ}(a_i, \mathcal{K}^{\text{PL}})} (a_i^j \leftrightarrow a_i) \right)$$

<footnote n="2">²For any formula $\phi$, $\delta(\phi)$ is inductively defined via $\delta(a) = 0$ for $a \in \text{At}$, $\delta(\neg\phi) = \delta(\phi)$, $\delta(\phi_1 \wedge \phi_2) = \delta(\phi_1 \vee \phi_2) = \max\{\delta(\phi_1), \delta(\phi_2)\}$, $\delta(\mathbf{X}\phi) = 1 + \delta(\phi)$, and $\delta(\phi_1 \mathbf{U} \phi_2) = 1 + \max\{\delta(\phi_1), \delta(\phi_2)\}$. See the work by Corea et al. [3] for further information.</footnote>
Finally, for each $a \in \text{At}(\mathcal{K})$ in combination with each $i \in \{0, ..., m\}$, we add $e_{a,i}$ to the set of soft clauses $\text{SC}_c^{\text{LTL}}(\mathcal{K}, m)$. Consequently, the set of soft clauses is defined as:

$$ \text{SC}_c^{\text{LTL}}(\mathcal{K}, m) = \bigwedge_{a \in \text{At}(\mathcal{K})} \bigwedge_{i=0}^{m} e_{a,i} $$

These clauses ensure that a maximum number of $e_{a,i}$ are set to true, thus implicitly minimizing the number of atoms $a \in \text{At}(\mathcal{K})$ for which at least one occurrence has to be forgotten with regard to a state $t_i$. As described for $\mathcal{I}_t^{\text{LTL}}$, we return $\infty$ if the instance $(\text{HC}_c^{\text{LTL}}(\mathcal{K}, m), \text{SC}_c^{\text{LTL}}(\mathcal{K}, m))$ is unsatisfiable.

# 4. Experimental Evaluation

The goal of our experimental evaluation is to compare our newly developed MaxSAT-based approaches to the existing ASP-based ones in terms of runtime. In the following, we present an overview of the data sets we used (Section 4.1), the experimental setup (Section 4.2), and finally discuss our findings (Section 4.3).

## 4.1. Data Sets

In order to evaluate the algorithmic approaches described in this work, we use three different data sets. To be precise, we use data from the *Business Process Intelligence Challenge* [6, 16], we newly introduce a set of randomly generated LTL$_{ff}$ knowledge bases, and we use data that has previously been used in the context of computing unsatisfiable cores [17]. In the following, each data set is described in detail.

**BPIC** The BPIC data set, which was also used by Corea et al. [6] to evaluate their ASP-based approaches, was created using data from the *Business Process Intelligence Challenge*<fnref n="3" />, which is an international scientific challenge series where real-world process data from various domains is provided. The process data is available in the form of *event logs*, which are (multi-)sets of activity sequences. To harness this data for inconsistency measurement, the state-of-the-art tool MINERFUL [18] is used to mine LTL formulas that represent temporal rules for the behavior that can be observed from the event logs. As the data set only contains 10 instances, we augmented it by (i) including event logs that were omitted in [6] and (ii) by mining rules with an additional set of mining parameters. Thus, we have two sets of mining parameters; the first setting consists of a support factor of 75% (i. e., the minimum number of cases a rule has to be fulfilled in) and confidence and interest factors of 12.5% (i. e., the support scaled by the ratio of cases in which the activation occurs, and the support scaled by the ratio of cases where both the activation and reaction occur, respectively)—this is the setting used by Corea et al. [6]. The second setting includes a support factor of 75% as well, and confidence and interest factors of 95% (see the work by Di Ciccio et al. [19] for details on mining parameter selection). Thus, in total, we used 17 event logs and two sets of mining parameters, resulting in a total of 34 knowledge bases.

Since a significant number of knowledge bases produced using the second parameter setting were consistent, we added constraints to increase the probability of the knowledge bases being inconsistent (note that this technique has been applied before [16]). To be precise, for each consistent knowledge base $\mathcal{K}$ we randomly selected an atom $a \in \text{At}(\mathcal{K})$ and added a formula of the form $G(\neg a)$ to $\mathcal{K}$.

**LRS** We newly introduce the LRS data set, which is essentially an LTL$_{ff}$ version of the SRS data set [20, 4, 21, 22] used for inconsistency measurement in propositional logic. More specifically, we used the approach of Tweetyproject's *SyntacticRandom Sampler*<fnref n="4" /> and extended it such that temporal operators are included as well. Thus, an LTL$_{ff}$ formula $\phi$ is produced based on input parameters $p_d, p_c, p_n, p_x, p_u, p_g, p_f \in [0, 1]$ with $p_d + p_c + p_n + p_x + p_u + p_g + p_f \le 1$ and $d \in (0, 1)$. The sampler randomly selects one of the following options for $\phi$:

<footnote n="3">³https://www.tf-pm.org/newsletter/newsletter-stream-2-05-2020/bpi-challenges-10-years-of-real-life-datasets</footnote>

<footnote n="4">⁴http://tweetyproject.org/api/1.19/org/tweetyproject/logics/pl/util/SyntacticRandom Sampler.html</footnote>
**Table 1**

Overview of some properties of the LTL<sub>ff</sub> data sets used in the evaluation, which include (from left to right) the total number of knowledge bases, the number of formulas per knowledge base (mean and standard deviation), the signature size per knowledge base (mean and standard deviation), the number of connectives per formula (mean and standard deviation), and the maximum depth per knowledge base (mean and standard deviation across the entire data set).

<table><thead><tr><th rowspan="2">Name</th><th rowspan="2">#KBs</th><th colspan="2">#Formulas</th><th colspan="2">Sig. size</th><th colspan="2">#Con./formula</th><th colspan="2">Max. depth</th></tr><tr><th>Mean</th><th>Std.</th><th>Mean</th><th>Std.</th><th>Mean</th><th>Std.</th><th>Mean</th><th>Std.</th></tr></thead><tbody><tr><td>BPIC</td><td>34</td><td>718.7</td><td>1647.8</td><td>16.2</td><td>24.3</td><td>7.0</td><td>2.0</td><td>2.2</td><td>0.6</td></tr><tr><td>LRS</td><td>180</td><td>35.9</td><td>23.6</td><td>15.8</td><td>8.6</td><td>1.7</td><td>1.1</td><td>2.6</td><td>0.6</td></tr><tr><td>UC</td><td>125</td><td>82.0</td><td>155.0</td><td>54.8</td><td>206.6</td><td>9.8</td><td>52.6</td><td>5.4</td><td>4.8</td></tr></tbody></table>

• $\phi = \phi_1 \wedge \phi_2$ (with probability $p_c$)

• $\phi = \phi_1 \vee \phi_2$ (with probability $p_d$)

• $\phi = \neg \phi_1$ (with probability $p_n$)

• $\phi = X\phi_1$ (with probability $p_x$)

• $\phi = \phi_1 U \phi_2$ (with probability $p_u$)

• $\phi = G\phi_1$ (with probability $p_g$)

• $\phi = F\phi_1$ (with probability $p_f$)

• $\phi = a$ (with $a$ being an atom chosen uniformly at random from a given signature, and with probability $1 - p_c - p_d - p_n - p_x - p_u - p_g - p_f$)

If $\phi$ is not an atom, we repeat the above process for $\phi_1$ (and $\phi_2$, if applicable). The probabilities $p_d, p_c, p_n, p_x, p_u, p_g, p_f$ are each multiplied by the discount parameter $d$ in order to ensure termination of the process. We set each probability $p_d, p_c, p_n, p_x, p_u, p_g, p_f$ to 0.129 and $d = 0.5$, and set the number of formulas and the signature size to different values in order to create a total of 180 knowledge bases (we selected the same values as for the SRS data set [20]).

**UC** The UC data set is based on knowledge bases used by Roveri et al. [17] for the purpose of computing unsatisfiable cores (i. e., unsatisfiable sets of formulas) in LTL on finite traces (LTL<sub>f</sub>). As the evaluation of approaches for computing unsatisfiable cores requires inconsistent knowledge bases, the data set compiled by Roveri et al. [17] is also useful for evaluating our approaches for inconsistency measurement. The authors selected unsatisfiable instances from the data set introduced by Li et al. [23] for evaluating a method for satisfiability checking in LTL<sub>f</sub>. The knowledge bases in this data set can be divided into seven different categories, some of which contain additional subcategories—amounting to a total of 25 categories. The data set, as presented by Roveri et al. [17], contains more than 1300 knowledge bases, with greatly varying numbers of instances per category. In order to obtain a number of knowledge bases that is more in line with the other data sets, and to align the representation of each (sub)category, we select 5 knowledge bases from each (sub)category. Consequently, the UC data set contains a total of 125 knowledge bases. For further details on the data, we refer the reader to the works by Roveri et al. [17] and Li et al. [23].

Table 1 provides an overview of some basic statistics of all three data sets.<fnref n="5" />

## 4.2. Experimental Setup

The implementation<fnref n="6" /> of our MaxSAT-based approach is based on a framework<fnref n="7" /> for inconsistency measurement in propositional logic provided by Niskanen et al. [4]. Following their work, we also apply UWRMaxSAT [24] (version 1.4) as the MaxSAT solver. With regard to the ASP-based algorithms,

<footnote n="5">⁵Data sets available under https://github.com/aig-hagen/datasets-for-inconsistency-measurement/tree/master/LTLff</footnote>

<footnote n="6">⁶Code available under https://github.com/aig-hagen/SAT-based-algorithms-for-inconsistency-measurement-LTL</footnote>

<footnote n="7">⁷https://bitbucket.org/coreo-group/sat4im/</footnote>
<caption>**Table 2**</caption>

Number of solved instances and cumulative runtime (CRT) w.r.t. the ASP and the MaxSAT approaches for $\mathcal{I}_t^{\text{LTL}}$ and $\mathcal{I}_c^{\text{LTL}}$. The index of the final state ($m$) was set to the maximum depth across all knowledge bases of the data set. Timeout: 600 seconds.

<table><thead><tr><th rowspan="2">Data set</th><th rowspan="2">#KBs</th><th rowspan="2">m</th><th rowspan="2">Approach</th><th colspan="2">$\mathcal{I}_t^{\text{LTL}}$</th><th colspan="2">$\mathcal{I}_c^{\text{LTL}}$</th></tr><tr><th>#solved</th><th>CRT (s)</th><th>#solved</th><th>CRT (s)</th></tr></thead><tbody><tr><td rowspan="2">BPIC</td><td rowspan="2">34</td><td rowspan="2">3</td><td>ASP</td><td>34</td><td>121.29</td><td>31</td><td>370.48</td></tr><tr><td>MaxSAT</td><td>34</td><td>7.84</td><td><b>34</b></td><td>7.85</td></tr><tr><td rowspan="2">LRS</td><td rowspan="2">180</td><td rowspan="2">4</td><td>ASP</td><td>180</td><td>6.73</td><td>180</td><td>34.81</td></tr><tr><td>MaxSAT</td><td>180</td><td>11.03</td><td>180</td><td>11.72</td></tr><tr><td rowspan="2">UC</td><td rowspan="2">125</td><td rowspan="2">30</td><td>ASP</td><td><b>123</b></td><td>1087.55</td><td>91</td><td>4612.91</td></tr><tr><td>MaxSAT</td><td>122</td><td>6552.84</td><td><b>122</b></td><td>7251.94</td></tr></tbody></table>

we use the implementation by Corea et al. [6] and apply Clingo [25] (version 5.5.1) as the ASP solver. All experiments were run on Intel Xeon E5-2643 v3 3.40-GHz CPUs with 192 GB RAM under Ubuntu 20.04.5 using a time limit of 600 s per instance.

We run our experiments on the three data sets described in the previous section (i. e., BPIC, LRS, and UC), and we set the index of the final state to the maximum depth across all knowledge bases w.r.t. each data set, in order to get meaningful results.

## 4.3. Results

An overview of the results of our experimental evaluation is presented in Table 2 and Figure 1.<fnref n="8" />

For the BPIC data set, w.r.t. $\mathcal{I}_t^{\text{LTL}}$, both approaches are able to solve all instances; however, the MaxSAT approach is significantly faster compared to the ASP method. Further, w.r.t. $\mathcal{I}_c^{\text{LTL}}$, the MaxSAT variant solves all 34 instances, while its ASP counterpart can only solve 31. In addition, the cumulative runtime (CRT) of the ASP approach is again significantly higher, despite solving fewer instances.

Regarding the LRS data set, both approaches are capable of solving all instances (for both $\mathcal{I}_t^{\text{LTL}}$ and $\mathcal{I}_c^{\text{LTL}}$), with overall quite low runtimes. For $\mathcal{I}_t^{\text{LTL}}$, ASP is slightly faster with a CRT of 6.73 s compared to MaxSAT (11.03 s). Conversely, for $\mathcal{I}_c^{\text{LTL}}$, the MaxSAT approach outperforms the ASP version with a CRT of 11.72 s vs. 34.81 s. Interestingly, the runtime of the MaxSAT approaches remains nearly constant regardless of whether we are calculating $\mathcal{I}_t^{\text{LTL}}$ or $\mathcal{I}_c^{\text{LTL}}$, despite $\mathcal{I}_c^{\text{LTL}}$ having a larger search space. This suggests that this approach scales better in comparison to the ASP methods, where the approach for $\mathcal{I}_c^{\text{LTL}}$ exhibits significantly higher runtimes than the one for $\mathcal{I}_t^{\text{LTL}}$. The slightly higher runtime observed for MaxSAT w.r.t. $\mathcal{I}_t^{\text{LTL}}$ compared to ASP might be attributed to overhead caused by computing the propositional logic representations of the given LTL<sub>ff</sub> formulas.

For the UC data set, the results are a bit more mixed—while the ASP approach for $\mathcal{I}_t^{\text{LTL}}$ solves one more instance than its MaxSAT-based counterpart (123 vs. 122), the ASP method for $\mathcal{I}_c^{\text{LTL}}$ is clearly outperformed by the MaxSAT variant (91 vs. 122). Once again, this highlights that the MaxSAT approach appears to scale better overall and performs particularly well in scenarios involving larger search spaces (Table 1 shows that the UC data set has the largest mean signature size out of the three considered data sets, which directly increases the potential maximum value of $\mathcal{I}_c^{\text{LTL}}$).

Thus, overall, the two approaches for $\mathcal{I}_t^{\text{LTL}}$ perform rather similarly well, however, with regard to $\mathcal{I}_c^{\text{LTL}}$, the MaxSAT approach clearly outperforms its ASP counterpart. The fact that w.r.t. $\mathcal{I}_c^{\text{LTL}}$, compared to $\mathcal{I}_t^{\text{LTL}}$, a larger search space has to be examined, indicates that the MaxSAT approaches generally scale better than the ASP approaches. This also complies with the findings from [4].

<footnote n="8">⁸Figure 1 consists of cactus plots, i. e., plots comprised of time measurements ordered from low to high. More precisely, we measure the runtime of an algorithm w.r.t. each knowledge base of a given data set, and subsequently order the measurements from low to high. If an inconsistency value could not be computed within the given time limit, the corresponding runtime is not plotted.</footnote>
<figure><img src="image_29.png" /><figcaption>**Figure 1:** Runtime comparison of the ASP and the MaxSAT approaches for $\mathcal{I}_t^{\text{LTL}}$ and $\mathcal{I}_c^{\text{LTL}}$. Timeout: 600 seconds.</figcaption></figure>

# 5. Conclusions

In this work, we introduced MaxSAT-based approaches for computing the two inconsistency measures for LTL$_{ff}$ that were proposed by Corea et al. [3]; namely, these are the LTL time inconsistency measure $\mathcal{I}_t^{\text{LTL}}$ and the LTL contension inconsistency measure $\mathcal{I}_c^{\text{LTL}}$. Our experimental evaluation demonstrated that these approaches, particularly for $\mathcal{I}_c^{\text{LTL}}$, exhibit better scalability and overall solve more instances compared to the current state-of-the-art ASP approach [6]. These findings are in line with results from inconsistency measurement for propositional logic [4] and underline the potential of MaxSAT solving for addressing challenges in measuring inconsistency in formalisms other than propositional logic.

Several directions remain open for future research. First, the development of additional inconsistency measures tailored to LTL$_{ff}$, along with corresponding algorithmic approaches, could further extend the applicability of our approach. Note that, to the best of our knowledge, the only other inconsistency measures for finite LTL were introduced by Kuhlmann and Corea [16], which are direct (and not time-sensitive) adaptations of measures for propositional logic based on the notion of minimal inconsistent subsets; further, these measures are computationally on a higher complexity level, which prohibits a direct application of MaxSAT methods. Second, exploring alternative algorithmic paradigms, such as techniques based on quantified Boolean formulas (QBF), may provide valuable insights into solving related problems. Additionally, testing various MaxSAT solvers could help identify improved configurations and enhance performance further. Finally, transferring these approaches to other domains—given the existence of numerous inconsistency measures across diverse formalisms—represents another promising avenue.

# References

[1] J. Grant, Classifications for inconsistent theories, Notre Dame J. of Formal Logic 19 (1978) 435–444.

[2] J. Grant, M. V. Martinez (Eds.), Measuring Inconsistency in Information, volume 73 of *Studies in Logic*, College Publications, 2018.

[3] C. Corea, J. Grant, M. Thimm, Measuring inconsistency in declarative process specifications, in: 20th International Conference on Business Process Management, Springer, 2022, pp. 289–306.
[4] A. Niskanen, I. Kuhlmann, M. Thimm, M. Järvisalo, MaxSAT-based inconsistency measurement, in: Proceedings of ECAI, IOS Press, 2023, pp. 1779–1786.

[5] G. Xiao, Z. Lin, Y. Ma, G. Qi, Computing inconsistency measurements under multi-valued semantics by partial max-sat solvers., in: KR, 2010, pp. 340–349.

[6] C. Corea, I. Kuhlmann, M. Thimm, J. Grant, Paraconsistent reasoning for inconsistency measurement in declarative process specifications, Information Systems 122 (2024) 102347.

[7] G. D. Giacomo, M. Y. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in: Proceedings of IJCAI’13, IJCAI/AAAI, 2013, pp. 854–860.

[8] G. Priest, The logic of paradox, Journal of Philosophical Logic 8 (1979) 219–241.

[9] A. Hunter, S. Konieczny, et al., Measuring inconsistency through minimal inconsistent sets, in: Proceedings of KR, 2008, pp. 358–366.

[10] J. Grant, A. Hunter, Measuring consistency gain and information loss in stepwise inconsistency resolution, in: Proceedings of ECSQARU, Springer, 2011, pp. 362–373.

[11] F. Bacchus, M. Järvisalo, R. Martins, Maximum satisfiability, in: Handbook of Satisfiability, IOS Press, 2021, pp. 929–991.

[12] B. Cha, K. Iwama, Y. Kambayashi, S. Miyazaki, Local search algorithms for partial MaxSAT, in: Proceedings of AAAI/IAAI’97, AAAI Press / The MIT Press, 1997, pp. 263–268.

[13] J. Berg, M. Järvisalo, R. Martins, A. Niskanen, T. Paxian, MaxSAT Evaluation 2024: Solver and Benchmark Descriptions, Department of Computer Science, University of Helsinki, 2024.

[14] G. S. Tseitin, On the complexity of derivation in propositional calculus, Structures in Constructive Mathematics and Mathematical Logic (1968) 115–125.

[15] P. Besnard, Forgetting-based inconsistency measure, Proceedings of the 10th International Conference on Scalable Uncertainty Management (SUM’16) (2016) 331–337.

[16] I. Kuhlmann, C. Corea, Inconsistency measurement in LTLf based on minimal inconsistent sets and minimal correction sets, in: Proceedings of SUM, Springer, 2024, pp. 217–232.

[17] M. Roveri, C. Di Ciccio, C. Di Francescomarino, C. Ghidini, Computing unsatisfiable cores for LTLf specifications, Journal of Artificial Intelligence Research 80 (2024) 517–558.

[18] C. Di Ciccio, M. Schouten, M. de Leoni, J. Mendling, Declarative process discovery with MINERful in ProM, in: Proceedings of the Demo Session of BPM, CEUR Workshop Proc., 2015, pp. 60–64.

[19] C. Di Ciccio, F. M. Maggi, M. Montali, J. Mendling, Resolving inconsistencies and redundancies in declarative process models, Information Systems 64 (2017) 425–446.

[20] I. Kuhlmann, A. Gessler, V. Laszlo, M. Thimm, A comparison of ASP-based and SAT-based algorithms for the extension inconsistency measure, in: Proc. SUM, Springer, 2022, pp. 139–153.

[21] I. Kuhlmann, A. Niskanen, M. Järvisalo, Computing MUS-based inconsistency measures, in: Proceedings of JELIA, Lecture Notes in Computer Science, Springer, 2023, pp. 745–755.

[22] I. Kuhlmann, A. Gessler, V. Laszlo, M. Thimm, Comparison of SAT-based and ASP-based algorithms for inconsistency measurement, Journal of Artificial Intelligence Research 82 (2025) 563–685.

[23] J. Li, G. Pu, Y. Zhang, M. Y. Vardi, K. Y. Rozier, SAT-based explicit LTLf satisfiability checking, Artificial Intelligence 289 (2020) 103369.

[24] M. Piotrów, UWrMaxSat: Efficient solver for MaxSAT and pseudo-boolean problems, in: International Conference on Tools with Artificial Intelligence (ICTAI), IEEE, 2020, pp. 132–136.

[25] M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, P. Wanko, Theory solving made easy with Clingo 5, in: Technical Communications of ICLP, 2016, pp. 2:1–2:15.
# Part III

## Tutorials
# StaRAI: From a Probabilistic Propositional Model to a Highly Compressed Probabilistic Relational Model (Extended Abstract)

Marcel Gehrke<fnref n="1" />, Malte Luttermann<fnref n="2" />

## Abstract

This extended abstract summarises the content of our tutorial titled "StaRAI: From a Probabilistic Propositional Model to a Highly Compressed Probabilistic Relational Model" presented at the 18th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2025) held on September 23-26, 2025, in Hagen, Germany.

## 1. Introduction

Our surrounding world is inherently uncertain and relational. The field of Statistical Relational AI (StaRAI) has emerged to account for both uncertainty and relational modelling, for example in probabilistic graphical models [1]. In StaRAI, probabilistic models explicitly encode objects and relations, which enables algorithms to exploit repeated structures, i.e., subgraphs with matching associated probability functions as well as identical graph structure, for efficiency gains during inference [2, 3, 4]. To exploit repeated structures, they first have to be identified. While such repeated structures frequently occur in many practical applications, they are generally not explicitly represented in a learned model and thus cannot be exploited by inference algorithms. By identifying and compactifying repeated structures, the size of a model can be significantly reduced, resulting in inference algorithms no longer running in time exponential, but only polynomial, with respect to so-called domain sizes [5, 6, 7]. It is therefore crucial to efficiently identify and compactify repeated structures to enable efficient inference.

## 2. Compression of Probabilistic Relational Models

Our tutorial provides a look at recent advances in the field of computing a highly compressed probabilistic relational model from a given probabilistic propositional model. In the past, it has been shown that a colour passing procedure based on a belief propagation scheme can be used to identify repeated structures in a propositional probabilistic model [4, 8]. Identified repeated structures can then be exploited to compress the model, which results in a significant reduction in storage requirements and drastically increases the efficiency of inference algorithms while at the same time maintaining exact inference results [7]. The current state-of-the-art algorithm to identify and compress repeated structures in a propositional probabilistic model is the Advanced Colour Passing (ACP) algorithm [9], which builds on the CompressFactorGraph algorithm introduced by Kersting et al. [8]. ACP compresses repeated structures by introducing so-called logical variables such that the resulting compressed model allows for efficient inference independent of a specific inference algorithm, whereas the CompressFactorGraph algorithm is tied to the belief propagation inference algorithm. Additional major advancements of ACP compared to its predecessor are that ACP is able to handle (i) commutative functions (i.e., associated

*The 18th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2025), September 23-26, 2025, Hagen, Germany*

<figure><img src="image_30.png" /></figure>

marcel.gehrke@uni-hamburg.de (M. Gehrke); malte.luttermann@dfki.de (M. Luttermann)

<figure><img src="image_31.png" /></figure>

0000-0001-9056-7673 (M. Gehrke); 0009-0005-8591-6839 (M. Luttermann)

<figure><img src="image_32.png" /></figure>

© 2025 This work is licensed under a "CC BY 4.0" license.

<footnote n="1">¹Institute for Humanities-Centered Artificial Intelligence, University of Hamburg, Germany</footnote>

<footnote n="2">²German Research Center for Artificial Intelligence (DFKI), Lübeck, Germany</footnote>
probability functions that map to a unique output value regardless of the order of some input values) and (ii) arbitrary orders of arguments in associated probability functions. By tackling both (i) and (ii), ACP solves significant practical limitations, as commutative functions frequently occur in practical applications and no specific order of arguments can be guaranteed in a learned model. Accounting for commutative functions and arbitrary orders of arguments requires additional offline computations, which have been efficiently implemented by using histograms that count the occurrences of specific input values for a (sub)set of a function's arguments [10, 11]. By deploying histograms within the ACP algorithm, ACP is able to efficiently identify and compress a given probabilistic propositional model while at the same time ensuring exact inference results when applying the resulting compressed model.

The ACP algorithm requires the associated probability functions to exactly match in order to identify and group repeated structures. However, in practical applications, associated probability functions slightly differ even if they should be considered equal due to inaccurate estimates, e.g., when learning the functions from data. To solve the problem of constructing a compressed representation from a given probabilistic propositional model taking inaccurate estimates of associated probability functions into account, the ε-Advanced Colour Passing (ε-ACP) algorithm has been introduced as a generalisation of the ACP algorithm [12]. The ε-ACP algorithm allows for a deviation between functions depending on a hyperparameter ε in order for functions to be considered equivalent. By doing so, ε-ACP efficiently identifies and compresses repeated structures that are not exactly identical. It has been proven that the change in query results induced by ε-ACP is strictly bounded and empirical experiments have shown that the change in query results is even close to zero in practice, validating that the compressed model returned by ε-ACP is an eligible approximation of the original model. Speller et al. [13] have further extended the ε-ACP algorithm to obtain a hierarchic version called Hierarchical Advanced Colour Passing (HACP) that efficiently computes a hierarchy of ε values, thereby yielding a hyperparameter-free approach with known error bounds on the change in query results. The HACP algorithm ensures that repeated structures that have been grouped for a specific choice of ε remain grouped for a larger value of ε as well, thus enhancing interpretability. Moreover, HACP allows to control the trade-off between compression and accuracy of query results by specifying an acceptable error bound on the change in query results, from which the corresponding value for ε is automatically derived (such that no value for ε has to be chosen manually).

To allow for the compression of a probabilistic propositional model containing functions whose function definitions are unknown, another extension of ACP has been proposed [14, 15]. By analysing the graph structure of the model, repeated structures are identified and known function definitions of associated probability functions are transferred to associated probability functions with the same surrounding graph structure but unknown function definitions. The equivalence of associated probability functions can also be determined by representing their function definitions as vectors and checking for the collinearity of these vectors, which allows to identify equivalent functions whose range (codomain) values lie on different scales without having to apply any normalisation step to the functions [16].

Obtaining a compressed probabilistic relational model is not only relevant to perform efficient probabilistic inference but also opens up new possibilities to efficiently perform causal inference efficiently. A compressed model computed by ACP that is enriched by causal knowledge can be used to perform efficient causal inference [17], even if only partial causal knowledge is available [18].

### 3. Conclusion

In the field of StaRAI, probabilistic models explicitly encode objects and relations, thereby allowing inference algorithms to exploit repeated structures for efficiency gains. Identifying and compressing these structures are thus fundamental problems that must be solved to enable efficient inference. Recently, there have been significant advancements in the field of computing a highly compressed probabilistic relational model from a given probabilistic propositional model. Specifically, the ACP algorithm and its variants have emerged to identify and compress repeated structures. This work provides an overview of recent advancements in the field of compressing probabilistic models.
# Acknowledgements

This work was supported by the BMBF project AnoMed 16KISA057.

# References

[1] D. Koller, N. Friedman, Probabilistic Graphical Models: Principles and Techniques, MIT Press, 2009.

[2] D. Poole, First-Order Probabilistic Inference, in: Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI-2003), Morgan Kaufmann Publishers Inc., 2003, pp. 985–991.

[3] G. Van Den Broeck, N. Taghipour, W. Meert, J. Davis, L. De Raedt, Lifted Probabilistic Inference by First-Order Knowledge Compilation, in: Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-2011), AAAI Press, 2011, pp. 2178–2185.

[4] B. Ahmadi, K. Kersting, M. Mladenov, S. Natarajan, Exploiting Symmetries for Scaling Loopy Belief Propagation and Relational Training, Machine Learning 92 (2013) 91–132.

[5] G. Van den Broeck, On the Completeness of First-Order Knowledge Compilation for Lifted Probabilistic Inference, in: Advances in Neural Information Processing Systems 24 (NIPS-2011), Curran Associates, Inc., 2011, pp. 1386–1394.

[6] N. Taghipour, D. Fierens, G. Van den Broeck, J. Davis, H. Blockeel, Completeness Results for Lifted Variable Elimination, in: Proceedings of the Sixteenth International Conference on Artificial Intelligence and Statistics (AISTATS-2013), PMLR, 2013, pp. 572–580.

[7] M. Niepert, G. Van den Broeck, Tractability through Exchangeability: A New Perspective on Efficient Probabilistic Inference, in: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence (AAAI-2014), AAAI Press, 2014, pp. 2467–2475.

[8] K. Kersting, B. Ahmadi, S. Natarajan, Counting Belief Propagation, in: Proceedings of the Twenty-Fifth Conference on Uncertainty in Artificial Intelligence (UAI-2009), AUAI Press, 2009, pp. 277–284.

[9] M. Luttermann, T. Braun, R. Möller, M. Gehrke, Colour Passing Revisited: Lifted Model Construction with Commutative Factors, in: Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-2024), AAAI Press, 2024, pp. 20500–20507.

[10] M. Luttermann, J. Machemer, M. Gehrke, Efficient Detection of Exchangeable Factors in Factor Graphs, in: Proceedings of the Thirty-Seventh International Florida Artificial Intelligence Research Society Conference (FLAIRS-2024), Florida Online Journals, 2024.

[11] M. Luttermann, J. Machemer, M. Gehrke, Efficient Detection of Commutative Factors in Factor Graphs, in: Proceedings of the Twelfth International Conference on Probabilistic Graphical Models (PGM-2024), PMLR, 2024, pp. 38–56.

[12] M. Luttermann, J. Speller, M. Gehrke, T. Braun, R. Möller, M. Hartwig, Approximate Lifted Model Construction, in: Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence (IJCAI-2025), IJCAI Organization, 2025.

[13] J. Speller, M. Luttermann, M. Gehrke, T. Braun, Compression versus Accuracy: A Hierarchy of Lifted Models, in: Proceedings of the Twenty-Eighth European Conference on Artificial Intelligence (ECAI-2025), IOS Press, 2025.

[14] M. Luttermann, R. Möller, M. Gehrke, Lifting Factor Graphs with Some Unknown Factors, in: Proceedings of the Seventeenth European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU-2023), Springer, 2023, pp. 337–347.

[15] M. Luttermann, R. Möller, M. Gehrke, Lifting Factor Graphs with Some Unknown Factors for New Individuals, International Journal of Approximate Reasoning 179 (2025) 109371.

[16] M. Luttermann, R. Möller, M. Gehrke, Lifted Model Construction without Normalisation: A Vectorised Approach to Exploit Symmetries in Factor Graphs, in: Proceedings of the Third Learning on Graphs Conference (LoG-2024), PMLR, 2025, pp. 46:1–46:17.
[17] M. Luttermann, M. Hartwig, T. Braun, R. Möller, M. Gehrke, Lifted Causal Inference in Relational Domains, in: Proceedings of the Third Conference on Causal Learning and Reasoning (CLeaR-2024), PMLR, 2024, pp. 827–842.

[18] M. Luttermann, T. Braun, R. Möller, M. Gehrke, Estimating Causal Effects in Partially Directed Parametric Causal Factor Graphs, in: Proceedings of the Sixteenth International Conference on Scalable Uncertainty Management (SUM-2024), Springer, 2024, pp. 265–280.