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 satis ablity problem (ISAT), and we present di erent cases where ISAT can be solved in polynomial time. Keyword: Satis ability Problem, Incremental Satis ability Problem, 2SAT, Entail Propositional Problem, E cient Satis ability Instances.
Introduction The primary goal of complexity theory is to classify computational problems according to their inherent computational complexity. A central issue in determining these frontiers has been the satis ability problem (SAT) in the propositional calculus. The case 2-SAT, to determine the satis ability of propositional two Conjunctive Normal Forms (2-CF), is an important tractable case of SAT. Variations 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 Arti cial Intelligence (AI) applications.
It is known that logic entail problem is a hard challenge in automatic
reasoning due to it is co-NP-Hard even in the propositional case [
Hooker [
We present here an algorithm for solving the 2-ISAT problem, and we establish an upper bound for the time-complexity of 2-ISAT, as well as, we show some e cient cases for the ISAT and the 2-ISAT problems. 2
Preliminaries Let X = fx1; : : : ; xng be a set of n Boolean variables. A literal is either a variable xi or a negated variable xi. As usual, for each x 2 X, x0 = x and x1 = x.
A clause is a disjunction of di erent and non-complementary literals. Notice that we discard the case of tautological clauses. For k 2 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 containing 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 2 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 = fx1; x1; :::; xn; xng. Also we used :Y as the negation operator on the object Y . We denote f1; 2; :::; ng by [[n]], and the cardinality of a set A by jAj.
An assignment s for a formula F is a function s : (F ) ! f0; 1g. An assignment s can also be considered as a set of literals without a complementary pair of literals, e.g., if l 2 s, then l 62 s. Let c be a clause and s an assignment, c is satis ed by s if and only if c \ s 6= ;. On the other hand, if for all l 2 c, l 2 s, then s falsi es c.
Let F be a CF, F is satis ed by an assignment s if each clause in F is satis ed by s. F is contradicted by s if any clause in F is falsi ed by s. A model of F is an assignment for (F ) that satis es F . A falsifying assignment of F is an assignment for (F ) that contradicts F . A DF F is satis ed by s if any phrase is satis ed by s. F is contradicted by s if all of its phrases are contradicted by s.
If n = j (F )j, then there are 2n possible assignments de ned over (F ). Let S(F ) be the set of 2n assignments de ned 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 ) n 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 ).
A Knowledge Base (KB) is a set K of formulas. Given a KB K and a propositional formula , we say that K implies , and we write K ` , if is satis ed for each model of K, i.e., if SAT (K) SAT ( ). This last problem is known as the propositional entail problem. The incremental satis ability problem (ISAT) consists in deciding if an initial knowledge Base K keeps its satis ability anytime a conjunction of new clauses is added. 3
Computing falsifying assignments of CF's Assume a KB K in CF, K = Vim=1 Ci, where each Ci is a clause, i 2 [[m]]. For each clause Ci, i 2 [[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 2 K determines a subset of falsifying assignments of K. The following lemma expresses how to form the falsifying set of assignments of a CF.
g Lemma 1 Given a CF K = Vim=1 Ci, it holds that F AL(K) = Sim=1f 2 S(K) j F AL(Ci)
remains unsatis able.
K0, K0
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 ` i 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( )
The best known case of an e cient 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
application of SLD-resolution has been the mechanism most commonly used in the
development of logic programming languages [
However, including 2-CF's as extensions of a Horn formula and continue applying SLD-resolution method as the inference engine, gives an exponentialtime complexity process on the number of Horn inferences to perform.
Despite of the refutation methods commonly used in the Horn inference, we consider here another method to determine whether K ` . When K = Vim=1 Ci and = Vik=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 = j (K)j. Given a clause Ci = (xi1 _: : :_xik ), the value at each position from i1-th to ik-th of the string Ai is xed with the truth value falsifying each literal of Ci. E.g., if xij 2 Ci, the ij-th element of Ai is set to 0. On the other hand, if xij 2 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 f0; 1g. In this way, the string Ai of length n = j (K)j 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: 8i 2 [[k]] : F AL('i)
Sjm=1 F AL(Cj) where K = Vim=1 Ci; = Vik=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.
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 xed values.
Let F = fC1; C2; ; Cmg be a CF, n = j (F )j. Let Ci; i 2 [[m]] be a clause in F and x 2 (F ) n (Ci) be any variable, we have that Ci (Ci _ :x) ^ (Ci _ x)
Lit(C2)
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 = f1; : : : ; pg f1; : : : ; ng such that for each i 2 I; xi 2 C1 but xi 62 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 fx1; x2; : : : ; xpg = Lit(C1)n 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 rst 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).
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 de ne:
8 ' Ind(C; ') = < ; : indep reduction(C; ') if ' and C are independent if Lit(C) n Lit(') = ; C Otherwise
The operation Ind(C; ') forms a conjunction of clauses whose falsifying assignments 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)
Let K = Vjm=1 Cj be a CF and ' be a clause. If we apply the Ind operator between each Cj 2 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 2 K according to the length jSjj = jLit(Cj) n Lit(')j in ascending order, because the number of literals in Cj, di erent 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 2 K, allow us to build the space F AL(') F AL(K). Thus, the following recurrence is de ned as: A1 = ', Aj+1 = Ind(Cj; Aj)); j = 1; : : : ; m.
In order to perform Ind(Cj; Aj), the remaining clauses in Cl 2 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 2 ; i = 1; : : : ; k, as: Ai;1 = 'i; Ai;j+1 = Ind(Cj; Ai;j); j = 1; : : : ; m; and i = 1; : : : ; k being so constructed clauses Ai;m+1 such that Sik=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.
L L
The transitive closure of !R, denoted by ")" allows to de ne T (x) = fxg [ fy : x ) yg.
The incremental satis ability problem (ISAT) involves checking whether
satis ability is maintained when new clauses are added to an initial satis able
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) [
Di erent 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 [
As a generalization of SAT, ISAT has been considered as an NP Problem, although until now, we have not seen complexity theory studies about the complexity-time di erences between SAT and ISAT. For example, it is known that 2-SAT is in the complexity class P, however it is not known the computational complexity of 2-ISAT. It is clear that a set of changes over a satis able KB K in 2-CF could change K into a general CF, in whose case, it turns in a general CF K0, K K0, and where the SAT problem on K0 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 [
Assuming an initial KB K, and a new CF to be added, both are satis able
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 [
Let us consider now that K is a 2-CF and is a general CF, both of them di erent from the previous cases. By the results presented in Section 4, each 'i 2 such that K ` 'i is removed from , so we assume that = ( 'i). It means, we will consider only the clauses in which decrease e ectively 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 2 Lit(K) and each 'i 2 , respectively.
The proposal for reviewing the satisfactibility of (K ^ ) is based on the following properties: 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 2 , which is veri ed 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 unsatis able.
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), 8'i 2 . Firstly, the number of partial assignments for a xed 'i is jSj = j ('i) (A1)j. Moreover, each partial assignment si 2 S is independent to the other assignments in S, because they are di erent in at least one literal, and each of them hold jsi+1j jsij + 1; 8si 2 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); 8'i 2 . 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 = fx1; : : : ; xpg = 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 2 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: j Ind(A; ) j k Y j Si j=j S1 j j S2 j : : : j Sik j : i=1 (2)
It is clear that the number of strings in jInd(A; )j is not bigger than the number of assignments in SAT (K) F AL( ) since the falsifying assignments of 'i 2 are removed from the partial assignment denoted by the string A. That means jS1j jS2j : : : jSkj2 O(jSAT (K) F AL( )j). From this upper bound, we infer some tractable cases for ISAT.
Theorem 1. Let K be a 2-CF formula and holds: a CF formula. The following 1. If jSAT (K)j poly(n) then ISAT is solved in polynomial time. In fact, we can have the set of models S explicitly and each model s 2 S can be checked: [s].
We propose a novel method to review K ` when K and are both in Conjunctive Normal Forms. This initial method is extended to consider the incremental satis ability (ISAT) problem. We have shown di erent 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.