The Incremental Satisfiability Problem for a Two Conjunctive Normal Form Guillermo De Ita1 , J. Raymundo Marcial-Romero2 and J. A. Hernández2 1 Faculty of Computer Sciences, BUAP 2 Facultad de Ingenierı́a, UAEM deita@cs.buap.mx, jrmarcialr@uaemex.mx, xoseahernandez@gmail.com.mx Abstract. We propose a novel method to review K ` φ when K and φ are both in Conjunctive Normal Forms (CF). We extend our method to solve the incremental satisfiablity problem (ISAT), and we present different cases where ISAT can be solved in polynomial time. Keyword: Satisfiability Problem, Incremental Satisfiability Problem, 2- SAT, Entail Propositional Problem, Efficient Satisfiability Instances. 1 Introduction The primary goal of complexity theory is to classify computational problems ac- cording to their inherent computational complexity. A central issue in determin- ing these frontiers has been the satisfiability problem (SAT) in the propositional calculus. The case 2-SAT, to determine the satisfiability of propositional two Conjunctive Normal Forms (2-CF), is an important tractable case of SAT. Vari- ations of the 2-SAT problem, e.g. in the optimization and counting area, have been key for establishing frontiers between tractable and intractable problems. One of the fundamental problems in automatic reasoning is the propositional entail problem which is a relevant task in many other issues such as estimating the degree of belief, to review or update beliefs, the abductive explanation, logical diagnosis, and many other procedures in Artificial Intelligence (AI) applications. It is known that logic entail problem is a hard challenge in automatic rea- soning due to it is co-NP-Hard even in the propositional case [8]. However, some fragments of propositional logic allow efficient reasoning methods [3]. One of the most relevant cases of efficient reasoning is the fragment of Horn Formulas. We present a novel method to solve the entail problem between conjunctive forms and how to apply it for solving the incremental satisfiability problem (ISAT). Hooker [7] presented an algorithm for the ISAT problem, in which the main contribution was the speed-up for solving a single formula by solving a growing subset of its constraints. Whittemore et al. [11] defined the incremental satisfia- bility problem as the solving of each formula in a finite sequence of subformulas. Wieringa [12] presented an incremental satisfiability solver and some of its ap- plications. Finally, Nadel [10] presented a variation of ISAT problem under assumptions that are modeled as first decision variables; all inferred clauses that depend on some of the assumptions include their negation. 25 We present here an algorithm for solving the 2-ISAT problem, and we es- tablish an upper bound for the time-complexity of 2-ISAT, as well as, we show some efficient cases for the ISAT and the 2-ISAT problems. 2 Preliminaries Let X = {x1 , . . . , xn } be a set of n Boolean variables. A literal is either a variable xi or a negated variable xi . As usual, for each x ∈ X, x0 = x and x1 = x. A clause is a disjunction of different and non-complementary literals. Notice that we discard the case of tautological clauses. For k ∈ IN , a k-clause is a clause consisting of exactly k literals, and a (≤ k)-clause is a clause with at most k literals. A phrase is a conjunction of literals, a k-phrase is a phrase with exactly k literals. A conjunctive normal form (CNF, or CF) F is a conjunction of clauses. We say that F is a monotone positive CF if all of its variables appear in unnegated form. A k-CF is a CF containing only k-clauses. (≤ k)-CF denotes a CF con- taining clauses with at most k literals. A 2-CF formula F is said to be strict only if each clause of F consists of two literals. A disjunctive normal form (DF) is a disjunction of phrases, and a k-DF is a DF containing only k-phrases. A variable x ∈ X appears in a formula F if either x or x is an element of F . We use υ(X) to represent the variables involved in the object X; where X can be a literal, a clause, or a CF. Lit(F ) is the set of literals involved in F , i.e. if X = υ(F ), then Lit(F ) = X ∪ X = {x1 , x1 , ..., xn , xn }. Also we used ¬Y as the negation operator on the object Y . We denote {1, 2, ..., n} by [[n]], and the cardinality of a set A by |A|. An assignment s for a formula F is a function s : υ(F ) → {0, 1}. An assign- ment s can also be considered as a set of literals without a complementary pair of literals, e.g., if l ∈ s, then l 6∈ s. Let c be a clause and s an assignment, c is satisfied by s if and only if c ∩ s 6= ∅. On the other hand, if for all l ∈ c, l ∈ s, then s falsifies c. Let F be a CF, F is satisfied by an assignment s if each clause in F is satisfied by s. F is contradicted by s if any clause in F is falsified by s. A model of F is an assignment for υ(F ) that satisfies F . A falsifying assignment of F is an assignment for υ(F ) that contradicts F . A DF F is satisfied by s if any phrase is satisfied by s. F is contradicted by s if all of its phrases are contradicted by s. If n = |υ(F )|, then there are 2n possible assignments defined over υ(F ). Let S(F ) be the set of 2n assignments defined over υ(F ). s ` F denotes that the assignment s is a model of F . s 6` F denotes that s is a falsifying assignment of F . If F1 ⊂ F is a formula consisting of some clauses from F , and υ(F1 ) ⊂ υ(F ), an assignment over υ(F1 ) is a partial assignment over υ(F ). If s has logical values determined for each variable in F then s is a total assignment of F . The SAT problem consists on determining whether F has a model. SAT(F ) denotes the set of models of F , then SAT(F ) ⊆ S(F ). The set FAL(F ) = S(F ) \ SAT (F ) consists of the assignments from S(F ) that falsify F . Clearly, for any propositional formula F , S(F ) = SAT (F ) ∪ F AL(F ). 26 A Knowledge Base (KB) is a set K of formulas. Given a KB K and a propo- sitional formula φ, we say that K implies φ, and we write K ` φ, if φ is satisfied for each model of K, i.e., if SAT (K) ⊆ SAT (φ). This last problem is known as the propositional entail problem. The incremental satisfiability problem (ISAT) consists in deciding if an initial knowledge Base K keeps its satisfiability anytime a conjunction of new clauses φ is added. 3 Computing falsifying assignments of CF’s Vm Assume a KB K in CF, K = i=1 Ci , where each Ci is a clause, i ∈ [[m]]. For each clause Ci , i ∈ [[m]], the assignment s(Ci ) = 1 contains at least one literal in Ci . It is easy to build F AL(K) since each clause Ci ∈ K determines a subset of falsifying assignments of K. The following lemma expresses how to form the falsifying set of assignments of a CF. Vm Sm Lemma 1 Given a CF K = i=1 Ci , it holds that F AL(K) = i=1 {σ ∈ S(K) | F AL(Ci ) ⊆ σ} Lemma 2 If a CF K is satisfiable, then ∀K 0 ⊆ K, K 0 is a satisfiable CF. Corollary 1 If a CF K is unsatisfiable, then ∀ CF K 0 such that K ⊆ K 0 , K 0 remains unsatisfiable. Now, let us consider the propositional entail problem: K ` φ, where K and φ are CF’s. The decision problem K ` φ is a classical Co-NP-Complete problem for CF’s in general, since this problem is logically equivalent to the tautology problem for any DF, which is a classic co-NP-complete problem. On the other hand, K ` φ iff SAT (K) ⊆ SAT (φ), and this last goal is equivalent to prove F AL(φ) ⊆ F AL(K), due to basic properties on sets that are closed under complementation. Lemma 3 F AL(φ) ⊆ F AL(K) if and only if K ` φ. The best known case of an efficient method for the inference K ` φ between CF’s is when both K and φ are Horn formulas. In this case, the application of SLD-resolution leads to a linear-time process for deciding K ` φ. The appli- cation of SLD-resolution has been the mechanism most commonly used in the development of logic programming languages [5]. However, including 2-CF’s as extensions of a Horn formula and continue applying SLD-resolution method as the inference engine, gives an exponential- time complexity process on the number of Horn inferences to perform. Despite of the refutation methods commonly used in the Horn inference, Vm we consider here another method to determine whether K ` φ. When K = i=1 Ci Vk and φ = i=1 ϕi , our method focuses on checking that F AL(φ) ⊆ F AL(K) in order to prove K ` φ. Each set F AL(Ci ) can be represented in a succinct way via a string Ai of length n = |υ(K)|. Given a clause Ci = (xi1 ∨. . .∨xik ), the value at each position 27 from i1 -th to ik -th of the string Ai is fixed with the truth value falsifying each literal of Ci . E.g., if xij ∈ Ci , the ij -th element of Ai is set to 0. On the other hand, if xij ∈ Ci , then the ij -th element is set to 1. The variables in υ(K) which do not appear in Ci are represented by the symbol ’*’ meaning that they could take any logical value in the set {0, 1}. In this way, the string Ai of length n = |υ(K)| represents the set of assignments falsifying the clause Ci . We call falsifying string to the string Ai representing the set of falsifying assignments of a clause Ci . We denote by F al String(Ci ), the string (with n symbols), that is the falsifying string for the clause Ci . As K and φ are CF’s, the falsifying strings of their clauses allow us to denote F AL(φ) and F AL(K). If K 6` φ ≡ F AL(φ) 6⊂ F AL(K) implies that there exists a set of assignments S such that S ⊆ F AL(φ) and S 6⊂ F AL(K). A reviewing procedure for K ` φ consists on taking each falsifying string representing F AL(φ) and reviewing if it is a subset of F AL(K), e.g:S  m Vm Vk ∀i ∈ [[k]] : F AL(ϕi ) ⊆ j=1 F AL(Cj ) where K = i=1 Ci , φ = i=1 ϕi 4 An exact algorithm for K ` φ, when K and φ are CF’s We present a method for checking K ` φ, with K and φ CF’s. Definition 1 Given two clauses C1 and C2 , if they have at least one comple- mentary literal, it is said that they have the independence property. Otherwise, we say that the clauses are dependent. Notice that falsifying strings for independent clauses have complementary values (0 and 1) in at least one of their fixed values. Let F = {C1 , C2 , · · · , Cm } be a CF, n = |υ(F )|. Let Ci , i ∈ [[m]] be a clause in F and x ∈ υ(F ) \ υ(Ci ) be any variable, we have that Ci ≡ (Ci ∨ ¬x) ∧ (Ci ∨ x) Definition 2 Given a pair of dependent clauses C1 and C2 , if Lit(C1 ) ⊆ Lit(C2 ) we say that C2 is subsumed by C1 . If C1 subsumes C2 then F AL(C2 ) ⊆ F AL(C1 ). On the other hand, if C2 is not subsumed by C1 and they are dependents, there is a set of indices I = {1, . . . , p} ⊆ {1, . . . , n} such that for each i ∈ I, xi ∈ C1 but xi 6∈ C2 . There exists a reduction to transform C2 to become independent from C1 , we call this transformation as the independent reduction between two clauses that works as follows: let C1 and C2 be two dependent clauses. Let {x1 , x2 , . . . , xp } = Lit(C1 )\ Lit(C2 ). Thus, C1 ∧ C2 ≡ C1 ∧ (C2 ∨ ¬x1 ) ∧ (C2 ∨ x1 ). Now C1 and (C2 ∨ ¬x1 ) are independent. Then, C1 ∧ C2 ≡ C1 ∧ (C2 ∨ ¬x1 ) ∧ (C2 ∨ x1 ∨ ¬x2 ) ∧ (C2 ∨ x1 ∨ x2 ) The first three clauses are independent. Repeating the process of making the last clause independent with the previous ones, until xp is considered; we have that C1 ∧ C2 can be written as: C1 ∧(C2 ∨¬x1 )∧(C2 ∨x1 ∨¬x2 )∧. . .∧(C2 ∨x1 ∨x2 ∨...∨¬xp )∧(C2 ∨x1 ∨x2 ∨...∨xp ). 28 The last clause contains all literals of C1 , so it is subsumed by C1 , and then C1 ∧ C2 ≡ C1 ∧ (C2 ∨ ¬x1 ) ∧ (C2 ∨ x1 ∨ ¬x2 ) ∧ . . . ∧ (C2 ∨ x1 ∨ x2 ∨ ... ∨ ¬xp ) (1) We obtain on the right hand side of (1) an independent set of p + 1 clauses which we denote as indep reduction(C1 , C2 ). We use the independent reduction between two clauses C and ϕ to define:  ϕ if ϕ and C are independent Ind(C, ϕ) = ∅ if Lit(C) \ Lit(ϕ) = ∅ indep reduction(C, ϕ) − C Otherwise  The operation Ind(C, ϕ) forms a conjunction of clauses whose falsifying as- signments are exactly F AL(ϕ) − F AL(C). Theorem 1 If ϕ and C are two clauses, then F AL(Ind(C, ϕ)) = F AL(ϕ) − F AL(C) Vm Let K = j=1 Cj be a CF and ϕ be a clause. If we apply the Ind operator between each Cj ∈ K and ϕ, we get as a result a set S such that S ⊆ F AL(ϕ) and S 6⊂ F AL(K). In order to generate a minimum set of independent clauses as a result of Ind(K, ϕ), it is crucial to sort the clauses Cj ∈ K according to the length |Sj | = |Lit(Cj ) \ Lit(ϕ)| in ascending order, because the number of literals in Cj , different to the literals in ϕ, determines the number of independent clauses to be generated. The operator Ind applied on the clause ϕ and each one of the clauses Cj ∈ K, allow us to build the space F AL(ϕ) − F AL(K). Thus, the following recurrence is defined as: A1 = ϕ, Aj+1 = Ind(Cj , Aj )), j = 1, . . . , m. In order to perform Ind(Cj , Aj ), the remaining clauses in Cl ∈ K, l = j + 1, . . . , m, those which are not reduced independently with Aj , are sorted again in ascendent order according to the number of common literals with the literals represented by Aj . This process can be extended to each ϕi ∈ φ, i = 1, . . . , k, as: Ai,1 = ϕi ; Ai,j+1 = Ind(Cj , Ai,j ), j = 1, . . . , m, and i = 1, . . . , k being so Sk constructed clauses Ai,m+1 such that i=1 (Ai,m+1 ) = F AL(φ)−F AL(K). These strings Ai,j , i = 1, . . . , k, j = 1, . . . , m form a matrix of strings. Notice that if Ai,j = ∅ then Ai,l = ∅, for l = j + 1, . . . , m. 5 Incremental Satisfiability Problem Definition 3 Let F be a 2-CF and L its set of literals. The relation →R ⊂ L×L is defined as follows: x →R y if and only if x → y. The transitive closure of →R , denoted by ”⇒” allows to define T (x) = {x} ∪ {y : x ⇒ y}. Definition 4 Let F be a 2-CF, for any literal x ∈ F , it is said that T (x) is inconsistent if x ∈ T (x) or ⊥ ∈ T (x), otherwise T (x) is said to be consistent. 29 Definition 5 A base for the set of models of a 2-CF F , denoted as S(F ), is a partial assignment s of F which consists of the variables with a fixed truth value. The incremental satisfiability problem (ISAT) involves checking whether sat- isfiability is maintained when new clauses are added to an initial satisfiable knowledge base K. ISAT is considered as a generalization of SAT since it allows changes of the input formula over the time, and also, it can be considered as a prototypical Dynamic Constraint Satisfaction Problem (DCSP) [9]. Different methods have been applied to solve ISAT, among them, branch and bounds procedures as variants of the classical Davis-Putnam-Loveland (DPL) method, denoted as IDPL methods. In IDPL procedures, when adding new clauses, those procedures maintain the search tree generated previously for the set of clauses K. IDPL performs substantially faster than DPL for a large set of SAT problems [7]. As a generalization of SAT, ISAT has been considered as an NP Prob- lem, although until now, we have not seen complexity theory studies about the complexity-time differences between SAT and ISAT. For example, it is known that 2-SAT is in the complexity class P, however it is not known the computa- tional complexity of 2-ISAT. It is clear that a set of changes over a satisfiable KB K in 2-CF could change K into a general CF, in whose case, it turns in a general CF K 0 , K ⊂ K 0 , and where the SAT problem on K 0 is a classic NP-complete problem. Rather than solving related formulas separately, modern solvers attempt to solve them incrementally since many practical applications require solving a sequence of related SAT formulas [2, 4]. We present in this section, a study about the threshold for the 2-ISAT problem that could be relevant to understand the border between P and NP complexity classes. Assuming an initial KB K, and a new CF φ to be added, both are satisfiable CF’s, let us consider some cases where ISAT can be determined directly. 1. If K and φ are 2-CF’s then (K ∧ φ) is a 2-CF that is the input of ISAT, and in this case, 2-ISAT is solvable in linear-time by applying the well known algorithms for 2-SAT [6, 1] 2. If φ consists of one clause and we have the satisfiability tree of K, we only have to review which satisfiable branches of the tree falsify φ, and this can be done in linear time on the number of satisfiable branches of the tree. 3. For monotone formulas, ISAT keeps satisfiable formulas. If each variable maintains an unique sign in both K and φ then (K ∧ φ) is always satisfiable. Let us consider now that K is a 2-CF and φ is a general CF, both of them different from the previous cases. By the results presented in Section 4, each ϕi ∈ φ such that K ` ϕi is removed from φ, so we assume that φ = (φ − ϕi ). It means, we will consider only the clauses in φ which decrease effectively the set of models of K. Assume that the computation of both T (x) and Bi = F AL(ϕi ) have been computed for each x ∈ Lit(K) and each ϕi ∈ φ, respectively. The proposal for reviewing the satisfactibility of (K ∧ φ) is based on the following properties: 30 1. Given the partial assignments A1 , A2 which they are part of any model (if there exists) of K. Those partial assignments may be extended in a way that they do not falsify any ϕi ∈ φ, which is verified by Ind(Aj , ϕi ), j = 1, 2. If it is possible, then a model for (K ∧ φ) is built. 2. Otherwise, Ind(Aj , ϕi ) = ∅, j = 1, 2 and any model of K will be part of any falsifying assignment of φ. Thus, (K ∧ φ) is unsatisfiable. When the operation Ind(A1 , ϕi ) is applied, a new literal x will be joined to A1 . In fact, we consider to join T (x) instead of x. For example, if A1 = ∗01∗∗∗1∗ and ϕ1 = ∗0 ∗ 010 ∗ ∗, Ind(A1 , ϕi ) gives as a result ∗011 ∗ ∗1∗, ∗0100 ∗ 1∗ and ∗010101∗. However, in this case it means to build the following three parcial assignments: A1 ∪T (x4 ), A1 ∪T (¬x4 )∪T (¬x5 ), and A1 ∪T (¬x4 )∪T (x5 )∪T (¬x6 ). If any of those strings is inconsistent then such string is substituted by ∅. Let us analyze the growth on the number of possible partial assignments of the operation: Ind(A1 , ϕi ), ∀ϕi ∈ φ. Firstly, the number of partial assignments for a fixed ϕi is |S| = |υ(ϕi ) − υ(A1 )|. Moreover, each partial assignment si ∈ S is independent to the other assignments in S, because they are different in at least one literal, and each of them hold |si+1 | ≥ |si | + 1, ∀si ∈ S. Although Ind(A, ϕi ) is computed in linear time on the size of both strings, the computational complexity of the revision procedure depends on the number of strings generated by Ind(A, ϕi ), ∀ϕi ∈ φ. In some cases, Ind(A, ϕi ) may generate empty sets. However, in the worst case, the time complexity depends on the cardinality of the sets Li = {x1 , . . . , xp } = lit(ϕi ) − lit(A), i = 1, . . . , k. In order to improve the time complexity of our procedure, it is convenient to sort the clauses ϕi ∈ φ according to the cardinality of the sets Li , i = 1, . . . , k from the smallest to the biggest and removing the clauses that are independent with A. Once the clauses are sorted in φ with respect to their cardinalities Li , the operation Ind(Ind(....Ind(Ind(A, ϕ1 ), ϕ2 ), . . . , ϕk ) is applied, determining so the succession: S0 = v(A), S1 = v(ϕ1 ) − v(A), S2 = v(ϕ2 ) − (v(ϕ1 ) ∪ v(A)), . . ., Sk = v(ϕk ) − (v(ϕk−1 ) ∪ . . . ∪ v(ϕ1 ) ∪ v(A)) Then, the number of new clauses in the worst case is given by: k Y | Ind(A, φ) |≤ | Si |=| S1 | ∗ | S2 | ∗ . . . ∗ | Sik | . (2) i=1 It is clear that the number of strings in |Ind(A, φ)| is not bigger than the number of assignments in SAT (K) − F AL(φ) since the falsifying assignments of ϕi ∈ φ are removed from the partial assignment denoted by the string A. That means |S1 | ∗ |S2 | ∗ . . . ∗ |Sk |∈ O(|SAT (K) − F AL(φ)|). From this upper bound, we infer some tractable cases for ISAT. Theorem 1. Let K be a 2-CF formula and φ a CF formula. The following holds: 1. If |SAT (K)| ≤ poly(n) then ISAT is solved in polynomial time. In fact, we can have the set of models S explicitly and each model s ∈ S can be checked: φ[s]. 31 2. If |SAT (K) − F AL(φ)| ≤ poly(n) then the number of strings in |Ind(A, φ)| is upper bounded by |SAT (K) − F AL(φ)| ≤ poly(n). 3. When φ[T (x)] is false for all consistent T (x), Ind(K, φ) finds the unsatis- fiability of (K ∧ φ) in polynomial time on the set of literals of K and the number of clauses of φ. Consequently, this determines a tractable case for the 2-ISAT problem. Conclusions We propose a novel method to review K ` φ when K and φ are both in Conjunc- tive Normal Forms. This initial method is extended to consider the incremental satisfiability (ISAT) problem. We have shown different cases where the ISAT problem can be solved in polynomial time. Especially, we designed an algorithm for solving the 2-ISAT problem that allow us to determine an upper bound for the time-complexity of this problem. Furthermore, we have established some tractable cases for the 2-ISAT problem. References 1. Buresh-Oppenheim J., Mitchell D., Minimum 2CNF resolution refutations in poly- nomial time, Proc. SAT’07 - 10th int. Conf. on Theory and applications of satisfia- bility testing, (2007), pp.300-313. 2. Cabodi G., Lavagno L., Murciano M., Kondratyev A., Watanabe Y., Speeding-up heuristic allocation, scheduling and binding with SAT-based abstraction/refinement techniques, ACM Trans. Design Autom. Electr. Syst., 15(2), (2010). 3. Creignou N., Papini O., Pichler R., Woltran S., Belief Revision within fragments of propositional logic, DBAI Tech. Report DBAI-TR-2012-75, (2012). 4. Eén N., S orensson K., An Extensible SAT-solver, In Enrico Giunchiglia and Ar- mando Tacchella, editors, Selected Revised Papers of 6th International Conference on Theory and Applicationsof Satisfiability Testing (SAT), Santa Margherita Ligure, Italy, LNCS Vol. 2919, (2003), pp. 502-518. 5. Gallier J., Logic for Computer Science: Foundations of Automatic Theorem Proving (chapter 9), (2003), online revision (free to download). 6. Gusfield, D., Pitt, L., A Bounded Approximation for the Minimum Cost 2-Sat Prob- lem, Algorithmica 8, (1992), pp. 103-117. 7. Hooker J.N., Solving the incremental satisfiability problem. Journal of Logic Pro- gramming 15, (1993), pp.177-186. 8. Khardon R., Roth D.: Reasoning with Models, Artificial Intelligence 87, No.1, (1996), pp. 187-213. 9. Gutierrez J., Mali A., Local search for incremental Satisfiability, Proc. Int. Conf. on AI (IC-AI’02), Las Vegas, (2002), pp. 986-991. 10. Nadel A., Ryvchin V., Strichman O., Ultimately Incremental SAT, Proc. SAT 2014, LNCS Vol. 8561, (2014), pp. 206218. 11. Whittemore J., Joonyoung K., Sakallah K.A. SATIRE: A New Incremental Satis- fiability Engine, In Proceedings of the 38th Design Automation Conference (DAC)- ACM, Las Vegas - USA, (2001), pp. 542-545. 12. Wieringa S., Incremental Satisfbiability Solving and its Applications, PhD thesis, Department of Computer Science and Engineering, Aalto University Pub., (2014). 32