New complexity results for Łukasiewicz logic
 164 Downloads
Abstract
One aspect that has been poorly studied in multiplevalued logics, and in particular in Łukasiewicz logic, is the generation of instances of varying difficulty for evaluating, comparing and improving satisfiability solvers. With the ultimate goal of finding challenging benchmarks for Łukasiewicz satisfiability solvers, we start by defining a natural and intuitive class of clausal forms (simple Łclausal forms) and studying their complexity. Since we prove that the satisfiability problem of simple Łclausal forms can be solved in linear time, we then define two new classes of clausal forms (Łclausal forms and restricted Łclausal forms) that truly exploit the nonlattice operations of Łukasiewicz logic and whose satisfiability problems are NPcomplete when clauses have at least three literals, and admit lineartime algorithms when clauses have at most two literals. We also define an efficient satisfiability preserving translation of Łukasiewicz logic formulas into Łclausal forms. Finally, we describe a random generator of Łclausal forms and report on an empirical investigation in which we identify an easyhardeasy pattern and a phase transition phenomenon for Łclausal forms.
Keywords
Łukasiewicz logics Clausal forms Complexity Instance generator1 Introduction
The proof theory of multiplevalued logics, as well as its complexity, has been deeply studied for a wide variety of logics (Aguzzoli et al. 2005; Hájek 1998; Metcalfe et al. 2009, 2005). However, the development of satisfiability solvers has received less attention despite the fact that, without competitive solvers, it is extremely difficult to apply multiplevalued logics to solve realworld problems.
In the quest for developing fast satisfiability solvers, it is crucial to have both random and structured challenging instances for evaluating and comparing solvers, as happens in close areas such as Boolean satisfiability testing and constraint programming.
Given the recent development of satisfiability modulo theorybased (SMT based) SAT solvers for multiplevalued logics (Ansótegui et al. 2012, 2015, 2016; Vidal 2016; Vidal et al. 2012), as well as the need of empirically evaluating and comparing them with other existing approaches, the objective of this paper is to develop suitable benchmarks for satisfiability testing in Łukasiewicz logic, as well as analyze their complexity from both a theoretical and practical perspective.
More specifically, we begin this paper by analyzing how the conjunctive normal forms (CNFs) used by SAT solvers can be extended to Łukasiewicz logics by really making use of the nonlattice operations (while still being restricted to the logical language).^{1} In a first very natural attempt, we replace the classical disjunction in Boolean CNFs with Łukasiewicz strong disjunction and interpret negation using Łukasiewicz negation. Interestingly enough, it turns out that the satisfiability problem of these clausal forms can be solved in linear time in the length of the formula, regardless of the size of the clauses and the cardinality of the truth value set (assuming it is greater than two). Recall that, in contrast, deciding the satisfiability of Boolean CNFs is NPcomplete when there are clauses with at least three literals (Garey and Johnson 1979). In multiplevalued logics, it can be even NPcomplete when there are clauses with at least two literals (Beckert et al. 1999, 2000; Manyà 2000).
The focus is then moved to producing instances that are on the one hand computationally challenging, and so, rich enough to model complex notions, and on the other, generated in a simple and regular way that opens the door to a systematic study (complexity, resolution methods, etc). With this aim, we introduce a new class of clausal forms, called Łukasiewicz (Ł)clausal forms, that are CNFs in which, besides replacing classical disjunction with Łukasiewicz strong disjunction, we allow negations above the literal level, i.e., clauses are strong disjunctions of terms, and terms are either literals or negated strong disjunctions of literals. We show that, in this case, 3SAT is NPcomplete, while 2SAT has lineartime complexity.^{2} Hence, these problems have the same complexity as their Boolean counterparts. We also propose a Tseitinlike transformation (Tseitin 1968) that translates any Łukasiewicz logic formula into a satisfiability preserving Łclausal form, showing that Łclausal forms are in fact a normal form for Łukasiewicz logic. Moreover, we introduce a fragment of Łclausal forms, called restricted Łclausal forms, and show that their 3SAT problem is NPcomplete and their 2SAT problem admits lineartime algorithms.
Moreover, we report on an empirical investigation in which we identify—when testing the satisfiability of randomly generated Łclausal forms having a fixed number of literals per clause with SMT and mixed integer programming (MIP) solvers—an easyhardeasy pattern and a phase transition phenomenon as the clausetovariable ratio varies. It turns out that there is a point where the hardest instances occur. Such a point is between an underconstrained region where the instances are almost surely satisfiable, and an overconstrained region where the instances are almost surely unsatisfiable. In the transition region, there is a threshold where roughly half of the instances are satisfiable, and half of the instances are unsatisfiable. So, we have developed a generator that is able to produce both satisfiable and unsatisfiable instances of varying difficulty.
This paper is an extended and improved version of Bofill et al. (2015b). The new contributions are the introduction of restricted Łclausal forms and the complexity analysis of satisfiability problems, the satisfiability preserving translation of Łukasiewicz logic formulas into Łclausal forms, and a more extensive experimental investigation that considers both SMT and MIP solvers.
The paper is structured as follows. Section 2 defines basic concepts in Łukasiewicz logics. Section 3 defines three types of clausal forms with Łukasiewicz strong disjunction and Łukasiewicz negation. We show that the satisfiability problem is decidable in linear time for the first type of clausal forms but is NPcomplete for the other types. Section 4 defines an efficient satisfiability preserving translation of Łukasiewicz logic formulas into Łclausal forms. Section 5 describes the random generator of Łclausal forms and reports on the conducted empirical investigation. Section 6 concludes and points out future research directions.
2 Preliminaries
In this section, we introduce the theoretical basis necessary for the development of the rest of the paper. For a deeper insight into manyvalued logics, see, e.g., Cintula et al. (2011).
Definition 1
A propositional language is a pair \(\mathbb {L}=\langle \varTheta ,\alpha \rangle \), where \(\varTheta \) is a set of logical connectives and \(\alpha :\varTheta \rightarrow \mathbb {N}\) defines the arity of each connective. Connectives with arity 0 are called constants. A language \(\langle \varTheta ,\alpha \rangle \) with a finite set of connectives \(\varTheta =\{\theta _1, \ldots , \theta _r\}\) is denoted by \(\langle \theta _1/ \alpha (\theta _1), \ldots ,\theta _r/ \alpha (\theta _r) \rangle \).
Given a set of propositional variables \(\mathcal{V}\), the set \(L_\mathcal{V}\) of \(\mathbb {L}\)formulas over \(\mathcal{V}\) is inductively defined as the smallest set with the following properties: (i) \(\mathcal{V} \subseteq L_\mathcal{V}\); (ii) if \(\theta \in \varTheta \) and \(\alpha (\theta )=0\), then \(\theta \in L_\mathcal{V}\); and (iii) if \(\phi _1, \ldots , \phi _m \in L_\mathcal{V}\), \(\theta \in \varTheta \) and \(\alpha (\theta )=m\), then \(\theta (\phi _1, \ldots , \phi _m) \in L_\mathcal{V}\).
Definition 2
A manyvalued logic \(\mathcal{L}\) is a tuple \(\langle \mathbb {L}, N, A, D \rangle \) where \(\mathbb {L}=\langle \varTheta ,\alpha \rangle \) is a propositional language, N is a truth value set, A is an interpretation of the operation symbols that assigns to each \(\theta \in \varTheta \) a function \(A_{\theta }:N^{\alpha (\theta )} \rightarrow N\) and \(D \subset N\) is a set of designated truth values.
The set of designated truth values from the previous definition can be understood as those which affirm satisfaction.
Definition 3
 1.
If \(\phi \) is a logical constant, then \(I(\phi )=A_\phi \).
 2.
If \(\phi = \theta (\phi _1, \ldots , \phi _r)\), then \(I(\theta (\phi _1, \ldots , \phi _r))=A_{\theta }(I(\phi _1),\ldots , I(\phi _r))\).
Throughout this work, we focus on a particular family of manyvalued logics: the finitevalued and infinitelyvalued Łukasiewicz logics. These were born from the generalization of a threevalued logic proposed by J. Łukasiewicz in the early twentieth century and have been deeply studied both from theoretical and practical points of view. For a deeper study on these matters, see for instance (Cignoli et al. 2000; Hájek 1998).
Definition 4
The nvalued Łukasiewicz logic, denoted by \(\varvec{\L _n}\), is the logic defined from the infinitelyvalued Łukasiewicz logic by restricting the universe of evaluation to the set \(N_n = \{0, \frac{1}{n1},\ldots , \frac{n1}{n1}\}\). That is to say, \(\varvec{\L _n} = \langle \mathbb {L}_{{{\L }}uk}, N_n, A_{{\L }},\{1\} \rangle \). Note that the operations are well defined because \(N_n\) is a subalgebra of [0, 1] with the interpretation of the operation symbols \(A_{{\L }}\) (for any operation \(A_*\) and any value/pair of values of \(N_n\), the result of the \(A_*\) over this/these values also belongs to \(N_n\)).
The function interpreting negation is called Łukasiewicz negation, the function interpreting strong conjunction is called Łukasiewicz tnorm, the function interpreting implication is called its residuum, and the function interpreting strong disjunction is called Łukasiewicz tconorm.
We say that a logic \(\mathcal{L}\) is a Łukasiewicz logic if it is either \(\varvec{[0,1]_{{\L }}}\) or \(\varvec{\L _n}\) for some natural number n.
We say that two formulas \(\varphi , \psi \) are equivalent (and write \(\varphi \equiv \psi \)) if, for each interpretation I, \(I(\varphi ) = I(\psi )\).
It is worth mentioning that one of the reasons we focus on Łukasiewicz logics is because SAT\(^\mathrm{Bool} \subset {\text{ SAT }}^\mathcal{L}\). This is not the case for other relevant logics such as Gödel (G) and Product (\(\varPi \)), where SAT\(^{G}= \mathrm{SAT}^{\varPi }= \mathrm{SAT}^{\text{ Bool }}\) (Hájek 1998). So, while Boolean solvers suffice for deciding the satisfiability of propositional formulas of G and \(\varPi \), specific solvers are needed to decide the satisfiability of propositional formulas of \(\mathcal{L}\).
3 Łukasiewicz clausal forms
In Boolean satisfiability, benchmarks are commonly represented in conjunctive normal form (CNF), i.e., as a conjunction of clauses, where each clause is a disjunction of literals. This formalism is very convenient because stateoftheart Boolean SAT solvers implement variants of the Davis–Putnam–Logemann–Loveland (DPLL) procedure (Davis et al. 1962), and DPLL requires the input in CNF. Hence, it seems reasonable to ask how Boolean CNFs could be adapted to Łukasiewicz logic in order to define challenging benchmarks for evaluating and comparing Łukasiewicz SAT solvers, as well as in order to develop DPLLlike procedures for Łukasiewicz logic.
3.1 Simple Łclausal forms
In the following, we refer to these formulas as simple Łukasiewicz clausal forms (simple Łclausal forms) and denote by \(mc(\varphi )\) the length of the shortest clauses in a simple \(\L \)clausal form \(\varphi \). That is to say, if \(\varphi = \bigwedge _{1 \le i \le n} (\bigoplus _{1 \le j \le k_i} l_{ij})\), then \(mc(\varphi ) = \min \{k_i: 1 \le i \le n\}\). Throughout this work, we assume that simple \(\L \)clausal forms are interpreted using a truth value set with at least three elements.
Unfortunately, the expressive power of these clausal forms is quite limited. As Lemma 2 shows, the satisfiability problem for simple \(\L \)clausal forms has lineartime complexity, contrarily to what happens in Boolean SAT, which is NPcomplete when there are clauses with at least three literals. Hence, complex problems cannot be encoded using this formalism.
Example 1
The simple \(\L \)clausal form \(\varphi = (x_1 \oplus x_2) \wedge (\lnot x_1 \oplus x_2) \wedge (\lnot x_1 \oplus \lnot x_2) \wedge (x_1 \oplus x_3) \wedge (x_2 \oplus x_3) \wedge (x_1 \oplus \lnot x_2 \oplus \lnot x_3)\) is satisfiable in \({\L _4}\) because the Boolean 2SAT instance \((x_1 \vee x_2) \wedge (\lnot x_1 \vee x_2) \wedge (\lnot x_1 \vee \lnot x_2) \wedge (x_1 \vee x_3) \wedge (x_2 \vee x_3)\) is satisfiable. However, \(\varphi \) is unsatisfiable under Boolean semantics. Recall that SAT\(^{\text{ Bool }} \subset {\text{ SAT }}^\mathcal{L}\).
The treatment of formulas with unit clauses (i.e., containing exactly one literal) is done by applying unit propagation (\(\mathrm {UP}\)). \(\mathrm {UP}\) consists in applying the unit literal rule until the empty clause is derived or a saturation state is reached. Applying the unit literal rule to an \(\L \)clausal form \(\varphi \) containing the unit clause \(l_i\) amounts to removing from \(\varphi \) all the clauses containing \(l_i\), and removing in \(\varphi \) all the occurrences of \(\lnot l_i\). If we remove a literal from a unit clause, we obtain the bottom element \(\perp \). We denote by \(\mathrm {UP}(\varphi )\) the formula obtained after applying \(\mathrm {UP}\) to \(\varphi \). \(\mathrm {UP}(\varphi )\) is either empty (meaning that it is satisfiable), a formula containing the bottom element \(\perp \) (meaning that there exists a contradiction at the unitary level, and so, the formula is directly unsatisfiable) or \(mc(\mathrm {UP}(\varphi )) > 1\), and so we fall in one of the scenarios discussed above.
Formally, we can express the previous results as follows.
Lemma 1
 1.If \(mc(\varphi ) > 1\), \(\varphi \) belongs to SAT\(^\mathcal{L}\) if one of the following conditions hold:

\(\vert N \vert = 2 s +1\) for \(s \ge 1\) or \(\vert N \vert \ge \aleph _0\)

\(mc(\varphi ) \ge 3\)

 2.
If \(mc(\varphi ) = 2\) and \(\vert N \vert = 2 s +2\) for \(s \ge 1\), then \(\varphi \) belongs to SAT\(^\mathcal{L}\) iff \(B_2(\varphi )\) belongs to SAT\(^{\text{ Bool }}\).
 3.
If \(mc(\varphi ) = 1\), then \(\varphi \) belongs to SAT\(^\mathcal{L}\) iff \(\mathrm {UP}(\varphi )\) belongs to SAT\(^\mathcal{L}\).
Proof
 1.
It is easy to see that whenever \(\frac{1}{2}\) belongs to the universe of evaluation (i.e., whenever \(\vert N \vert = 2s +1\) or \(\mathcal{L}\) is the infinitelyvalued Łukasiewicz logic), the interpretation that assigns \(\frac{1}{2}\) to each variable satisfies any possible simple \(\L \)clausal form \(\varphi \) such that \(mc(\varphi ) \ge 2\). On the other hand, if \(mc(\varphi ) \ge 3\) and \(\vert N \vert = 2 s + 2\) for some \(s \ge 1\) (\(N = \{0, \frac{1}{2s+1},\dots ,\frac{2s+1}{2s+1}\}\)), the interpretation that assigns \(\frac{s+1}{2s+1}\) to each variable x satisfies any clause of \(\varphi \) in \(\mathcal{L}\). It is clear that \(s+1 < 2s+1\), so \(\frac{s+1}{2s+1} \in N\). On the other hand, by the definition of Łukasiewicz negation, the interpretation of \(\lnot x\) is \(1  \frac{s+1}{2s+1} = \frac{s}{2s+1}\), and it is routine to check that \(\frac{s+1}{2s+1} > \frac{s}{2s+1} \ge \frac{1}{3}\). Thus, for any clause \(l_1 \oplus \cdots \oplus l_k\) in \(\varphi \), the interpretation of each one of its literals is greater than or equal to \(\frac{1}{3}\). Since \(mc(\varphi ) \ge 3\), we have that the interpretation of each clause is always 1.
 2.First suppose there is an interpretation I on \(\mathcal{L}\) that satisfies \(\varphi \), and recall that \(\frac{1}{2} \not \in N\). We can then define a Boolean interpretation \(I'\) that satisfies \(B_2(\varphi )\) by letting For each binary clause \(l_1 \oplus l_2\) from \(\varphi \), at least one of the strict inequalities \(I(l_1) > \frac{1}{2}\) or \(I(l_2) > \frac{1}{2}\) must hold in order that I satisfies the clause. So, we can assume, without loss of generality, that \(I(l_1) > \frac{1}{2}\). If \(l_1\) is a positive literal (equal to a variable \(x_1\)), then by definition \(I'(x_1) = 1\), and so, \(I(x_1 \vee l_2) = 1\). Otherwise (\(l_1 = \lnot x_1\)), it holds that \(I(x_1) < \frac{1}{2}\). Then, by definition, \(I'(x_1) = 0\). So \(I'(\lnot x_1) = 1\), and thus \(I'(\lnot x_1 \vee l_2) = 1\). To prove the other direction, let \(\vert N \vert = 2 s +2\) for some \(s \ge 1\), and suppose I is an interpretation on \(\{0,1\}\) that satisfies \(B_2(\varphi )\). Then, let \(I'\) be the interpretation in \(\mathcal{L}\) defined by As was proven in 1, this interpretation satisfies all the clauses of length at least 3, so we just need to check that the binary clauses from \(\varphi \) are also satisfied. Let \(l_1 \oplus l_2\) be a binary clause of \(\varphi \). Then, \(l_1 \vee l_2\) is a clause from \(B_2(\varphi )\), and thus, \(I(l_1 \vee l_2) = 1\). Without loss of generality, assume that \(I(l_1) = 1\). If it is a positive literal (\(l_1 = x_1\)), then \(I'(x_1) = \frac{s+1}{2s+1}\) and \(I'(l_2) \ge 1  \frac{s+1}{2s+1}\), so \(I'(x_1 \oplus l_2) \ge \frac{s+1}{2s+1} + 1  \frac{s+1}{2s+1} = 1\). Otherwise, \(I(\lnot x_1) = 1\) implies that \(I(x_1) = 0\), and thus, \(I'(x_1) = 1  \frac{s+1}{2s+1}\). Then again, \(I'(\lnot x_1 \oplus l_2) \ge 1  (1 \frac{s+1}{2s+1}) + 1  \frac{s+1}{2s+1} = 1\).
 3.
\(\mathrm {UP}\) preserves the satisfiability when applied to a simple \(\L \)clausal form \(\varphi \). If \(\mathrm {UP}(\varphi )\) contains the empty clause, then \(\varphi \) is unsatisfiable. If \(\mathrm {UP}(\varphi )\) is the empty formula, then \(\varphi \) is satisfiable. In the rest of cases, since \(\mathrm {UP}(\varphi )\) contains no unit clauses, the satisfiability of \(\mathrm {UP}(\varphi )\) can be decided using either case 1 or case 2 of this lemma.
Lemma 2
The satisfiability of any simple \(\L \)clausal form is decidable in linear time.
Proof
Case 1 of Lemma 1 can be clearly solved in linear time because we only have to check whether the cardinality of the truth value set is either odd or even. In the latter case, we also have to check whether all the clauses contain at least three literals, and this can be achieved by traversing once the clausal form.
Case 2 of Lemma 1 can be also solved in linear time. Checking whether the cardinality of the truth value set is even, and identifying the binary clauses in the simple \(\L \)clausal form can be easily done in linear time. In addition, there are algorithms for solving the resulting Boolean 2SAT problem in linear time (Aspvall et al. 1979).
Case 3 of Lemma 1 can be solved using the same algorithms that are applied for Boolean unit propagation, which have lineartime complexity (Zhang and Stickel 1996). \(\square \)
3.2 Łclausal forms
To overcome the limitations of simple Łclausal forms explained above, we now define a new family of test instances, called Łukasiewicz clausal forms (Łclausal forms). These instances have a higher expressive power and are interesting from a practical point of view because they exhibit an easyhardeasy pattern and a phase transition phenomenon similar to the ones found in other combinatorial problems like Boolean 3SAT (Mitchell et al. 1992) and regular 3SAT (Béjar and Manyà 1999; Manyà et al. 1998). So, one can generate both satisfiable and unsatisfiable instances of varying difficulty by adjusting the clausetovariable ratio.
Definition 5

A literal is a propositional variable or a negated propositional variable.

A term is either a literal or an expression of the form \(\lnot (l_1 \oplus \cdots \oplus l_n),\) where \(l_1, \ldots , l_n\) are literals.

A Łukasiewicz clause (Łclause) is an expression of the form \(t_1 \oplus \cdots \oplus t_n \), where \(t_1, \ldots , t_n\) are terms.

A Łukasiewicz clausal form (Łclausal form) is a (weak) conjunction of Łclauses; i.e., it is an expression of the form \(\bigwedge _{i=1}^{k} C_i\), where \(C_i\) is an Łclause.
Definition 6
The SAT problem for an Łclausal form consists in finding an interpretation that satisfies all its Łclauses. If each Łclause contains exactly k literals, it is called the kSAT problem for Łclausal forms.
Example 2
The Łclausal form \(\lnot x_2 \wedge (x_1 \oplus x_3) \wedge (\lnot (x_1 \oplus x_2) \oplus \lnot x_3)\) is satisfied by the interpretation that assigns the value 0 to \(x_1\) and \(x_2\) and assigns the value 1 to \(x_3\).
Lemma 3
The 3SAT problem for Łclausal forms is NPcomplete.
Proof
We will show that (i) this problem belongs to NP and (ii) the Boolean 3SAT problem is polynomially reducible to the 3SAT problem for Łclausal forms.
The 3SAT problem for Łclausal forms clearly belongs to NP: Given a satisfiable Łclausal form, a nondeterministic algorithm can guess a satisfying interpretation and check that it satisfies the formula in polynomial time.
 1.
For every Boolean variable \(x_k\), \(1 \le k \le m\), we add the Łclause \(\lnot (x_k \oplus x_k) \oplus x_k\) in \(\phi '\).
 2.
For every clause \(l_{i1} \vee l_{i2}\vee l_{i3}\) in \(\phi \), we add the Łclause \(l_{i1} \oplus l_{i2} \oplus l_{i3}\) in \(\phi '\).
We now prove that \(\phi '\) is satisfiable iff \(\phi \) is satisfiable. Assume that \(\phi '\) is satisfiable. Then, every variable \(x_k\) must be evaluated to either 0 or 1. This is so because \(\lnot (x_k \oplus x_k) \oplus x_k\) evaluates to 1 iff \(x_k\) evaluates to either 0 or 1. Since the semantics of Łukasiewicz strong disjunction when restricted to 0 and 1 is identical to the semantics of Boolean disjunction, any model of \(\phi '\) is a model of \(\phi \). Therefore, \(\phi \) is satisfiable.
Assume that \(\phi \) is satisfiable. Any Boolean model of \(\phi \) can be transformed to a manyvalued model by assigning 0 to the variables that evaluate to false, and 1 to the variables that evaluate to true. If \(x_k\) evaluates either to 0 or 1, \(\lnot (x_k \oplus x_k) \oplus x_k\) evaluates to 1, and \(l_{i1} \oplus l_{i2} \oplus l_{i3}\) also evaluates to 1 because we assumed that every Boolean clause \(l_{i1} \vee l_{i2} \vee l_{i3}\) is satisfied. Therefore, \(\phi '\) is satisfiable. \(\square \)
These instances are interesting because the 3SAT problem for Łclausal forms is NPcomplete while it is decidable in linear time if negations are not allowed above the literal level; i.e., the 3SAT problem for simple Łclausal forms. Moreover, Łclausal forms are genuinely multiplevalued in the sense that there exist Łclausal forms that are satisfiable under Łukasiewicz semantics but are unsatisfiable under Boolean semantics.
Example 3
The formula \((x_1 \oplus x_2) \wedge (\lnot x_1 \oplus x_2) \wedge (x_1 \oplus \lnot x_2) \wedge (\lnot x_1 \oplus \lnot x_2)\) is satisfied in Łukasiewicz logic if \(x_1\) and \(x_2\) evaluate to \(\frac{1}{2}\), but \((x_1 \vee x_2) \wedge (\lnot x_1 \vee x_2) \wedge (x_1 \vee \lnot x_2) \wedge (\lnot x_1 \vee \lnot x_2)\) is unsatisfiable in the Boolean case.
We now prove that the 2SAT problem for Łclausal forms can be solved in linear time.
Lemma 4
The 2SAT problem for Łclausal forms is decidable in linear time.
Proof
The only Łclauses of 2SAT instances that are different from the clauses in simple Łclausal forms are of the form \(\lnot (l_i \oplus l_j)\), where \(l_i,l_j\) are literals. However, clauses of the form \(\lnot (l_i \oplus l_j)\) can be replaced with \(\lnot l_i \wedge \lnot l_j\) because \(\lnot (l_i \oplus l_j)\) is satisfiable iff \(l_i\) and \(l_j\) evaluate both to 0. Hence, replacing all the Łclauses \(\lnot (l_i \oplus l_j)\) with \(\lnot l_i \wedge \lnot l_j\) produces a simple Łclausal form, whose satisfiability can be decided in linear time according to Lemma 2. \(\square \)
3.3 Restricted Łclausal forms
In the proof of Lemma 3, we saw that the full expressive capacity of Łclausal forms is not necessary for checking the NPcompleteness of SAT over those formulas. Indeed, we can naturally provide an alternative clausal form for Łukasiewicz logic that still is NPcomplete, while it is possibly simpler in some aspects than the Łclausal forms introduced above.
Definition 7
Example 4
The \(\L \)clausal form \(\lnot x_2 \wedge (\lnot (x_1 \oplus x_1)\oplus x_3) \wedge (\lnot (\lnot x_2 \oplus \lnot x_2) \oplus \lnot x_3)\) corresponds to the restricted Łclausal form \(\lnot x_2 \wedge ((\lnot x_1)^2 \oplus x_3) \wedge ((x_2)^2 \oplus \lnot x_3)\).
Lemma 5
The 3SAT problem for restricted Łclausal forms is NPcomplete.
Proof
This can be proved in an analogous way to Lemma 3. Just observe that the formula \(\lnot (x \oplus x) \oplus x\) (added to the Łclausal form that reduces Boolean 3SAT) is in fact equivalent, by the definition of \(\oplus \) in Ł, to \((\lnot x)^2 \oplus x\), which is a restricted Łclause. Thus, the same proof of NPcompleteness is valid for restricted Łclausal forms. \(\square \)
Lemma 6
The 2SAT problem for restricted Łclausal form is decidable in linear time.
Proof
Similarly to the proof of Lemma 4, observe that the only clauses different from simple Łclauses are of the form \(l^2\), which simply imposes \(l = 1\), not adding any complexity to the solution search. \(\square \)
4 Reducing Łukasiewicz formulas to equivalent Łclausal forms
In a similar way as any Boolean propositional formula can be reduced to a polynomialsize CNF formula that preserves satisfiability (see, e.g., Tseitin 1968), we describe how we can polynomially reduce any formula \(\varphi \) in Łukasiewicz logic (with variables \(\mathcal {V}ar(\varphi )\)) to a satisfiability preserving Łclausal form \(\varphi ^*\) over \(\mathcal {V}ar(\varphi )\) and a set of auxiliary variables that abbreviate more complex formulas. The relevance of the translation in this context comes from the fact that the formulas encoding the equivalence between the new variables and the corresponding complex formulas can also be written as Łclauses.
Example 5
Let \(\varphi ^* \,{:=}\, \varphi ' \wedge \bigwedge \nolimits _{ \chi \in \varDelta (\varphi )}\chi \). Observe that the total number of conjuncts of \(\varphi ^*\) is bounded by \(1 + 2 (\vert {\textit{SFm}}(\varphi ) \vert  1  \vert \mathcal {V}(\varphi )\vert )\).
Proposition 1
 1.
\(\varphi ^*\) is a Łclausal form with at most three literals in each clause.
 2.For each interpretation, I into \(\L _{\infty }\), if \(I(\varDelta (\varphi )) \subseteq \{1\}\), then$$\begin{aligned} I(\varphi ) = I(\varphi '). \end{aligned}$$
Proof
 1.
By definition, \(\varphi '\) is a clause of a simple Łclausal form (and thus, a clause of a Łclausal form), that has at most two variables (one if \(\varphi \equiv \lnot \psi \) for some \(\psi \)). Also following the definition, each one of the formulas in \(\varDelta (\varphi )\) is a clause in Łclausal form with at most three literals (three for the clauses encoding the value of a variable of the form \(x_{\psi \rightarrow \chi }\), and two for the ones concerning \(x_{\lnot \psi }\)).
 2.We can prove by induction on \(\varphi \) that \(I(\varDelta (\varphi )) \subseteq \{1\}\) implies that \(I(\varphi ) = I(\varphi ')\). Observe before proceeding that if \(\psi \) is a subformula of \(\varphi \), then \(I(\varDelta (\varphi )) \subseteq \{1\}\) implies \(I(\varDelta (\psi )) \subseteq \{1\}\).

For propositional variables it is trivial, because \(\varphi \) and \(\varphi '\) are the same formula.

Assume \(\varphi \equiv \lnot \psi \). By definition, \(I(\varphi ') = I(\lnot x_\psi )\). Since \(I(\varDelta (\varphi )) \subseteq \{1\}\), in particular it holds that \(I(\lnot x_{\psi } \oplus \psi ') = 1\) and \(I(\lnot \psi ' \oplus x_{\psi }) = 1\). By interpretation of the Ł connectives, we get that \(I(x_\psi ) = I(\psi ')\), and so \(I(\varphi ') = I(\lnot \psi ') = \lnot I(\psi ')\). Now, from the observation above, we can apply the induction hypothesis and get \(\lnot I(\psi ') = \lnot I(\psi )\), and so conclude \(I(\varphi ') = I(\lnot \psi ) = I(\varphi )\).

If \(\varphi \equiv \psi _1 \rightarrow \psi _2\), so \(I(\varphi ') = I(\lnot x_{\psi _1} \oplus \psi _2')\). As before, it is immediate that \(I(\varphi ') = \lnot I(\psi _1') \oplus I(\psi _2')\). By the induction hypothesis, this equals to \(\lnot I(\psi _1) \oplus I(\psi _2) = I(\varphi )\), concluding the proof.

An immediate corollary of the previous translation, together with Lemma 3, is a new proof of the already known result of NPcompleteness of SAT in Łukasiewicz logic (e.g., Mundici 1987).
It seems, however, not clear whether it is possible to do a reduction from arbitrary Łukasiewicz formulas to Łclausal forms preserving the set of variables and allowing longer clauses (which is easy in classical logic although the derived formula can have exponential size). In contrast to what happens in classical logic (with the lattice operators), in Łukasiewicz logic \(\odot \) does not distribute over \(\oplus \).
5 Experimental results
We first describe the generator of Łclausal forms that we have developed and then report on the empirical investigation conducted to identify challenging benchmarks.
The generator of Łclausal form 3SAT instances used works as follows: given n variables and k clauses, each of the k clauses is constructed from three variables \((x_{i_1},x_{i_2},x_{i_3})\) which are drawn uniformly at random. Then, one of the following eleven possible Łclauses \(x_{i_1} \oplus x_{i_2} \oplus x_{i_3}\), \(\lnot x_{i_1} \oplus x_{i_2} \oplus x_{i_3}\), \(x_{i_1} \oplus \lnot x_{i_2} \oplus x_{i_3}\), \(x_{i_1} \oplus x_{i_2} \oplus \lnot x_{i_3}\), \(\lnot x_{i_1} \oplus \lnot x_{i_2} \oplus x_{i_3}\), \(\lnot x_{i_1} \oplus x_{i_2} \oplus \lnot x_{i_3}\), \(x_{i_1} \oplus \lnot x_{i_2} \oplus \lnot x_{i_3}\), \( \lnot x_{i_1} \oplus \lnot x_{i_2} \oplus \lnot x_{i_3}\), \(\lnot (x_{i_1} \oplus x_{i_2}) \oplus x_{i_3}\), \(\lnot (x_{i_1} \oplus x_{i_3} )\oplus x_{i_2}\), and \(x_{i_1} \oplus \lnot (x_{i_2} \oplus x_{i_3})\) is selected with the same probability. We consider this set of clauses because it can be observed in the reduction from Boolean 3SAT to Łclausal forms that these types of negations suffice to get NPhardness.
In the experiments, we solved sets of 100 Łclausal form 3SAT instances with 1500 variables, and a number of variables ranging from 100 to 6000 with steps of 100. We considered the 3valued, 5valued and 7valued Łukasiewicz logics, as well as the infinitelyvalued Łukasiewicz logic. Instances were solved with the SMT solver Yices (Dutertre 2014) (version 2.5.1), with a theorem prover similar to those described in Ansótegui et al. (2012), as well as with the exact MIP solver SCIP (Cook et al. 2013) (version 3.0.0) linked with the linear programming solver CPLEX (version 12.6). The experiments were run on an Intel^{®} Xeon^{®} E31220v2 machine at 3.10 GHz with Turbo Boost disabled.
We start by depicting the results obtained with the SMT solver. Figure 1 shows the results for the finitelyvalued case. We observe a phase transition between satisfiability and unsatisfiability similar to that of Boolean random 3SAT, as well as an easyhardeasy pattern in the median difficulty of the problems around the phase transition. Prob(sat) indicates the probability that an instance has to be satisfiable. In the threshold point of the phase transition, roughly half of the instances are satisfiable; on its left, most of the instances are satisfiable; and on its right, most of the instances are unsatisfiable. Moreover, we observe that the difficulty increases with the cardinality of the truth value set, especially in the hardest instances.
We have also considered solving the generated formulas with a mixed integer programming (MIP) solver; in particular, using the MIP solver SCIP, which allows to solve MIPs exactly over the rational numbers. Note that all standard MIP solvers work with finite precision (floating point) arithmetic. This allows efficient computations but also introduces rounding errors, which cannot be neglected in our setting, as they could lead to incorrect results. On the other side, all SMT solvers, as well as the exact version of the MIP solver SCIP, work with arbitrary precision arithmetic, typically using the GNU Multiple Precision Arithmetic Library (GMP).
For the MIP experiments, we use the encodings to MIP defined in Hähnle (1994). They are summarized in the following lemmas.
Lemma 7
 1.
\(I(\lnot \phi ) \ge i\) iff \(I(\phi ) \le 1i\).
 2.
\(I(\lnot \phi ) \le i\) iff \(I(\phi ) \ge 1i\).
 3.\(I(\phi \oplus \psi ) \ge i\) iff there are \(i_1, i_2 \in [0,1]\) such that$$\begin{aligned} \begin{array}{l} I(\phi ) \ge i_1\\ I(\psi ) \ge i_2\\ i_1 + i_2 = i \end{array} \end{aligned}$$
 4.\(I(\phi \oplus \psi ) \le i\) iff there are \(i_1, i_2 \in [0,1]\) and \(v_\mathrm{aux} \in \{0,1\}\) such that$$\begin{aligned} \begin{array}{l} I(\phi ) \le i_1\\ yI(\psi ) \le i_2\\ v_\mathrm{aux} \le i\\ v_\mathrm{aux} \le i_1\\ v_\mathrm{aux} \le i_2\\ v_\mathrm{aux} +i = i_1 + i_2 \end{array} \end{aligned}$$
Note that \(I(\phi \oplus \psi ) \le i\) will hold either if \(I(\phi ) + I(\psi ) \le i\) or \(i = 1\). If \(v_\mathrm{aux} = 0\), then the constraint system simplifies to \(I(\phi ) \le i_1, I(\psi ) \le i_2, 0 \le i, 0 \le i_1, 0 \le i_2, i = i_1 + i_2\), where \(0 \le i\), \(0 \le i_1\), and \(0 \le i_2\) are redundant. If \(v_\mathrm{aux} = 1\), then the constraint system simplifies to \(I(\phi ) \le i_1, I(\psi ) \le i_2, 1 \le i, 1 \le i_1, 1 \le i_2, 1 + i = i_1 + i_2\), which implies \(i = 1, i_1 = 1, i_2 = 1\), making the system to become trivially satisfiable.
We consider now the finitelyvalued case with \(N=\{0,1, \ldots , n1\}\) and \(D=\{n1\}\).^{4}
Lemma 8
 1.
\(I(\lnot \phi ) \ge i\) iff \(I(\phi ) \le n1i\).
 2.
\(I(\lnot \phi ) \le i\) iff \(I(\phi ) \ge n1i\).
 3.\(I(\phi \oplus \psi ) \ge i\) iff there are \(i_1, i_2 \in \{0,1, \ldots , n1\}\) such that$$\begin{aligned} \begin{array}{l} yI(\phi ) \ge i_1\\ I(\psi ) \ge i_2\\ i_1 + i_2 = i \end{array} \end{aligned}$$
 4.\(I(\phi \oplus \psi ) \le i\) iff there are \(i_1, i_2 \in \{0,1, \ldots , n1\}\) and \(v_\mathrm{aux} \in \{0,1\}\) such that$$\begin{aligned} \begin{array}{l} I(\phi ) \le i_1\\ I(\psi ) \le i_2\\ (n1) \times v_\mathrm{aux} \le i\\ (n1) \times v_\mathrm{aux} \le i_1\\ y(n1) \times v_\mathrm{aux} \le i_2\\ (n1) \times v_\mathrm{aux} +i = i_1 + i_2 \end{array} \end{aligned}$$
We have identified the same phase transition phenomenon and easyhardeasy pattern for Łclausal form 3SAT instances also with other SMT solvers, as well as with other MIP solvers. Hence, it becomes apparent that our results are independent from the encoding and the solver used and provide a challenging benchmark. The results also suggest that the SMTbased approach is more suitable in the finitelyvalued case, whereas the MIPbased approach is more suitable in the infinitelyvalued case.
6 Concluding remarks
We have defined three new clausal forms for Łukasiewicz logic (simple Łclausal forms, Łclausal forms and restricted Łclausal forms), analyzed the complexity of different satisfiability problems for these clausal forms, and proposed a method for translating any Łukasiewicz formula into a satisfiability preserving Łclausal form. We have also described a generator that produces Łclausal forms of varying difficulty to test Łukasiewicz SAT solvers and conducted an empirical investigation with SMT and MIP solvers to identify an easyhardeasy pattern and a phase transition phenomenon. As future work, we plan to analytically derive tight lower and upper bounds of the threshold point and find suitable encodings of combinatorial problems using the formalism of Łclausal forms.
Finally, we would like to mention the existence of two related works (Borgwardt et al. 2014; Bofill et al. 2015a) that show the NPcompleteness of the satisfiability problem of Łukasiewicz rules, which are a fragment of Łclausal forms. Borgwardt et al. (2014) proved the NPcompleteness of Łukasiewicz rules when the cardinality of the truth value set is greater than three. We then proved in Bofill et al. (2015a) that the problem remains NPcomplete when the truth value set has three elements, and that it can be solved in polynomial time when the rules have almost one literal in the consequent of the rule.
Footnotes
 1.
 2.
When the number of literals per clause is fixed to k, the corresponding SAT problem is called kSAT. In the following, when we say lineartime complexity we mean that the complexity is linear in the size of the formula.
 3.
Recall that any Łukasiewicz formula can be written using only \(\lnot \) and \(\rightarrow \) operators (see, e.g., Cignoli et al. 2000), and that \(\varphi \rightarrow \psi \equiv \lnot \varphi \oplus \psi \) in Łukasiewicz logic.
 4.
The set \(\{0,1, \ldots , n1\}\) is isomorphic to the set \(\{0,\frac{1}{n1}, \frac{2}{n1}, \ldots , 1\}\) through the isomorphism \(i_n: \{0,1, \ldots , n1\} \rightarrow \{0,\frac{1}{n1}, \frac{2}{n1}, \ldots , 1\}\), \(i_n(x)=\frac{x}{n1}\).
Notes
Acknowledgements
The authors would like to thank the anonymous reviewer for their valuable comments and suggestions. This work was supported by Project LOGISTAR from the EU H2020 Research and Innovation Programme under Grant Agreement No. 769142, MINECOFEDER Projects RASO (TIN201571799C21P) and LoCos (TIN201566293R), and the UdG Project MPCUdG2016/055. Vidal acknowledges the support from the Project GA1704630S of the Czech Science Foundation (GAČR).
Compliance with ethical standards
Conflict of interest
Authors declare that they have no conflict of interest.
Ethical approval
This article does not contain any studies with human participants performed by any of the authors.
References
 Aguzzoli S, Gerla B, Haniková Z (2005) Complexity issues in basic logic. Soft Comput 9(12):919–934CrossRefzbMATHGoogle Scholar
 Ansótegui C, Bofill M, Manyà F, Villaret M (2012) Building automated theorem provers for infinitelyvalued logics with satisfiability modulo theory solvers. In: Proceedings, 42nd international symposium on multiplevalued logics (ISMVL), Victoria, BC, Canada. IEEE CS Press, pp 25–30Google Scholar
 Ansótegui C, Bofill M, Manyà F, Villaret M (2015) SAT and SMT technology for manyvalued logics. Mult Valued Logic Soft Comput 24(1–4):151–172MathSciNetGoogle Scholar
 Ansótegui C, Bofill M, Manyà F, Villaret M (2016) Automated theorem provers for multiplevalued logics with satisfiability modulo theory solvers. Fuzzy Sets Syst 292:32–48MathSciNetCrossRefzbMATHGoogle Scholar
 Aspvall R, Plass M, Tarjan R (1979) A linear time algorithm for testing the truth of certain quantified boolean formulae. Inf Process Lett 8(3):121–123CrossRefzbMATHGoogle Scholar
 Beckert B, Hähnle R, Manyà F (1999) Transformations between signed and classical clause logic. In: Proceedings, international symposium on multiplevalued logics, ISMVL’99, Freiburg, Germany. IEEE Press, Los Alamitos, pp 248–255Google Scholar
 Beckert B, Hähnle R, Manyà F (2000) The 2SAT problem of regular signed CNF formulas. In: Proceedings. 30th international symposium on multiplevalued logics (ISMVL), Portland/OR, USA. IEEE CS Press, Los Alamitos, pp 331–336Google Scholar
 Béjar R, Manyà F (1999) Phase transitions in the regular random 3SAT problem. In: Proceedings of the 11th international symposium on methodologies for intelligent systems, ISMIS’99, Warsaw, Poland. Springer LNAI 1609, pp 292–300Google Scholar
 Bofill M, Manyà F, Vidal A, Villaret M (2015a) The complexity of 3valued łukasiewicz rules. In: Proceedings, 12th international conference on modeling decisions for artificial intelligence, MDAI, Skövde, Sweden. Springer LNCS 9321, pp 221–229Google Scholar
 Bofill M, Manyà F, Vidal A, Villaret M (2015b) Finding hard instances of satisfiability in Łukasiewicz logics. In: Proceedings, 45th international symposium on multiplevalued logics (ISMVL), Waterloo, Canada. IEEE CS Press, pp 30–35Google Scholar
 Borgwardt S, Cerami M, Peñaloza R (2014) Manyvalued Horn logic is hard. In: Proceedings of the first workshop on logics for reasoning about preferences, uncertainty, and vagueness, PRUV 2014, colocated with IJCAR 2014, Vienna, Austria, pp 52–58Google Scholar
 Cignoli R, D’Ottaviano IML, Mundici D (2000) Algebraic foundations of manyvalued reasoning, trends in logicstudia logica library, vol 7. Kluwer Academic Publishers, DordrechtzbMATHGoogle Scholar
 Cintula P, Hájek P, Noguera C (eds) (2011) Handbook of mathematical fuzzy logic, 3 volumes, studies in logic. mathematical logic and foundation, vols 37, 38 and 58. College PublicationsGoogle Scholar
 Cook W, Koch T, Steffy DE, Wolter K (2013) A hybrid branchandbound approach for exact rational mixedinteger programming. Math Program Comput 5(3):305–344MathSciNetCrossRefzbMATHGoogle Scholar
 Crawford JM, Auton LD (1993) Experimental results on the crossover point in satisfiability problems. In: Proceedings of the 11th national conference on artificial intelligence, AAAI’93, Washington, DC, USA. AAAI Press, pp 21–27Google Scholar
 Davis M, Logemann G, Loveland D (1962) A machine program for theoremproving. Commun ACM 5:394–397MathSciNetCrossRefzbMATHGoogle Scholar
 Dutertre B (2014) Yices 2.2. In: Proceedings of the 26th international conference on computer aided verification, CAV 2014, Lecture Notes in Computer Science, vol 8559. Springer, pp 737–744Google Scholar
 Garey MR, Johnson DS (1979) Computers and intractability: a guide to the theory of NPcompleteness. Freeman, San FranciscozbMATHGoogle Scholar
 Hähnle R (1994) Short conjunctive normal forms in finitelyvalued logics. J Log Comput 4(6):905–927MathSciNetCrossRefzbMATHGoogle Scholar
 Hájek P (1998) Metamathematics of fuzzy logic. Kluwer, DordrechtCrossRefzbMATHGoogle Scholar
 Li CM, Manyà F (2009) MaxSAT, hard and soft constraints. In: Biere A, van Maaren H, Walsh T (eds) Handbook of satisfiability. IOS Press, Amsterdam, pp 613–631Google Scholar
 Manyà F (2000) The 2SAT problem in signed CNF formulas. Mult Valued Log Int J 5(4):307–325MathSciNetzbMATHGoogle Scholar
 Manyà F, Béjar R, EscaladaImaz G (1998) The satisfiability problem in regular CNFformulas. Soft Comput 2(3):116–123CrossRefGoogle Scholar
 Metcalfe G, Olivetti N, Gabbay D (2005) Lukasiewicz logic: From proof systems to logic programming. Log J IGPL 12(5):561–585CrossRefzbMATHGoogle Scholar
 Metcalfe G, Olivetti N, Gabbay DM (2009) Proof theory of fuzzy logics, applied logic series, vol 36. Springer, BerlinzbMATHGoogle Scholar
 Mitchell D, Selman B, Levesque H (1992) Hard and easy distributions of SAT problems. In: Proceedings of the 10th national conference on artificial intelligence, AAAI’92, San Jose, CA, USA. AAAI Press, pp 459–465Google Scholar
 Mundici D (1987) Satisfiability in manyvalued sentential logic is NPcomplete. Theor Comput Sci 52:145–153MathSciNetCrossRefzbMATHGoogle Scholar
 Mundici D, Olivetti N (1998) Resolution and model building in the infinitelyvalued calculus of Łukasiewicz. Theor Comput Sci 200(1–2):335–366CrossRefzbMATHGoogle Scholar
 Tseitin G (1968) Studies in constructive mathematics and mathematical logic, part II, chap. In: On the complexity of derivations in the propositional calculus. Steklov Mathematical Institute, pp 115–125Google Scholar
 Vidal A (2016) MNiBLoS: a SMTbased solver for continuous tnorm based logics and some of their modal expansions. Inf Sci 372:709–730CrossRefGoogle Scholar
 Vidal A, Bou F, Godo L (2012) An SMTbased solver for continuous tnorm based logics. In: Proceedings of the 6th international conference on scalable uncertainty management, SUM 2012, Marburg, Germany. Springer LNCS 7520, pp 633–640Google Scholar
 Wagner H (1998) A new resolution calculus for the infinitevalued propositional logic of lukasiewicz. In: FTP (LNCS selection). Technical Report E1852GS981, TU Wien, pp 234–243Google Scholar
 Zhang H, Stickel ME (1996) An efficient algorithm for unit propagation. In: In Proceedings of the fourth international symposium on artificial intelligence and mathematics (AIMATH’96), Fort Lauderdale (Florida), USA, pp 166–169Google Scholar
Copyright information
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.