P = NP: A Polynomial-Time Solution to 3-SAT
Full text
I am sorry if my paper eventually lacks in technicalities, I am but an undergrad student and as such I have -with all probabilityapproached the problem in a very naive way: of course I did my research, grasping the basic concepts behind this beautiful branch of Computer Science, yet I will most likely lack the elegance, diligence and wisdom that an experienced professor might have. That being said, I hope the ideas and the demonstrations (if proved to be logically impeccable), in their novel approach, might share a light on this undoubtedly important problem: not just for academics, but our society in general. Notice: this paper is a preprint. Pretty much everything inside it needs refinement and editing from someone with more experience then me. If you see an error or margin of improvement I beg you to notify me at the following email address: lorenzo.taborc[email protected] Every kind of constructive feedback is welcomed. Due to some radical changes in the last part of the paper I have decided to put the latest updates in an appendix, just so you can see them before I have decided how to integrate them into the paper. Notice that, since these updates shift the entire problem in a completely different direction, some of the last paragraphs have yet to be overhauled: specifically section 3.2.3 and 3.2.4. Check out Appendix C. 1
Contents 1 Introduction: what is a 3-SAT problem? 3 2 Core elements 4 2.1 Solution Set and Variable Set . . . . . . . . . . . . . . . . . . . . 4 2.2 Clause classification and 3-SAT subproblems . . . . . . . . . . . 8 2.3 Pn k=0 2kand Cumulative Preservation . . . . . . . . . . . . . . . 16 3 3-SAT Polynomial-Time solver 18 3.1 Full-House Problem (colloquially: Tonina’s problem) . . . . . . . 18 3.2 Combinatorial-Based Problem (colloquially: Bianca’s problem) . 22 3.2.1 3-SAT as Composition of its Subproblems . . . . . . . . . 22 3.2.2 Matrix-based Solution . . . . . . . . . . . . . . . . . . . . 30 3.2.3 Combinatorial Based Problem Algorithm Explained . . . 31 3.2.4 Algorithm Complexity . . . . . . . . . . . . . . . . . . . . 40 3.2.5 Soundness and Completeness . . . . . . . . . . . . . . . . 43 3.2.6 Optimized Algorithm (colloquially: Luna’s Algorithm) . . 43 4 Conclusion 44 5 Appendix A: BSC and how it solves 3-SAT decision problem 45 6 Appendix B: 3-QBF reduction to 3-SAT (PSPACE = NP = P) 50 7 Appendix C: reduction to 2-SAT 52 2
P = NP: A Polynomial-Time Solution to 3-SAT Lorenzo Taborchia∗ October 28, 2025 1 Introduction: what is a 3-SAT problem? The 3-SAT problem is a subcategory of SAT (or Boolean Satisfiability Problem): a well-rooted computational theory problem where the computer is asked to find a series of assignments capable of solving a given Boolean formula in conjunctive normal form (CNF) 1. An example of said problem might be2: (x1+x2+x4)·(x3+x4+x6) This problem has been classified as NP-complete by Cook-Levin’s Theorem: that means that 3-SAT is a special problem which solution may be verified in polynomial time and is NP-hard. Hence, each NP problem may be reduced to a 3-SAT since it is within the most difficult NP problems. That is, being able to find such an algorithm that would solve 3-SAT in polynomial time would mean that each NP-problem may be solved in polynomial time. The main challenge in finding a polynomial solution for an NP-hard problem such as 3-SAT is that it suffers from combinatorial explosion: that is brute-forcing3a 3-SAT instance with n variable would force our machine to check 2npossible solutions in the worst case scenario. The exponential nature of 3-SAT runs even deeper since classic algorithms such as ’Branch & Bound’ or ’DPLL’ are not able to solve such a problem in polynomial-time for every instance. This hints to the fact that either 3-SAT has exponential complexity for every possible algorithm made to solve it (P=NP), or we have to analyze the problem’s nature deeper in order to find a polynomial solution (P=NP ). My whole research took the second route. By discovering a way to represent a 3-SAT in set form and classifying all its clauses over multiple abstraction levels, I was able to find a way to transform the problem in such a way that an elaborate algorithm within a 8(n+1)×n 3matrix is able to solve it in ∗To anyone who exists or has ever existed in my life, however lost. 1Where the formula consists of a conjunction (AND) of several OR clauses 2From now on I will use the same notation used by Boole in his books: that is, plus sign for ORs and the multiplication dot for ANDs 3Hence checking whether each possible solution solves the problem 3
polynomial-time (hence P=NP ). I have in fact found an Θ(n6) complexity in a the worst case that involves performing every possible operation made on each element in a column of said matrix. An even much more optimized algorithm may be found (probably) using a mathematical property linked to base-two-finite-geometric-series I like to call Cumulative Preservation (this part is still work in progress). 2 Core elements Before diving into my proof’s heart I have to introduce the main ideas that went behind it. First of all that each SAT problem Solution Set, that is the number of possible solutions of a given SAT problem, can be presented as a Venn’s Diagram where each set (e.g. variable’s Set) intercepts the others generating a total of 2nregions. this theorem will be later demonstrated. Yet, before rushing to the demonstration let me define, borrowing some concepts from set theory, what I even mean by Solution Set. 2.1 Solution Set and Variable Set Definition 2.1.1 (Solution Set) ASolution Set (SS) is the universal set (U) of an SAT problem. Each Solution Set is defined by the following axioms: (i): Each element of the Solution Set is an n-tuple of boolean elements. That is, each Solution Set solution is defined as: ti∈U:ti= (x1, x2, x3, ..., xn) And: ∀xj∈ti:xj∈ {1,0} Direct consequence: each solution is a different ti (ii): We call each generic subset ViVariable Set (VS) that be presented as n-tuple vi: ∀Vi⊂U:vi= (x1, x2, x3, ..., xn) Where: ∀j− {k} ∈ {1, ..., n}:xj=X, xk= 1 And we define D={1,0, X}a set containing all possible symbols, where Xmeans the variable is not asserted and may be either 1or 0. 4
(iii): An intersection between Variable Sets may still be presented as an n-tuple: Wi∩j= (Vi∩Vj)⊂U:wi∩j= (x1, x2, x3, ..., xn) Where: ∀k−C∈ {1, ..., n}:xk=X And: C⊂ {1, .., n},∀c∈C, xc∈V1∨xc∈V2:xc∈ {0,1} (iv): A Variable Set n-tuple may be negated using a bit-wise NOT, therefore: ¬vi= (¬x1, ..., ¬xn) And: ∀j− {k} ∈ {1, ..., n}:xj=X, xk= 0 (v) AND between Variable Spaces: AND is a binary operation between Variable Space n-tuples such that: vi·vj= (x1·x′ 1, ..., xn·x′ n) And ∀k∈ {1, .., n}: xk·x′ k= 1 : (xk= 1 ∧x′ k=X)∨(x′ k= 1 ∧xk=X) 0:(xk= 0 ∧x′ k=X)∨(x′ k= 0 ∧xk=X) X: (xk=X∧x′ k=X) It has to be considered as the result of an interception between Variable Sets. In fact for v1·v2you have (by definition of interception) that: vi·vj= (y1, ..., yn) With: (yi, yj= 1 ∀k∈ {1, ..., n}−{i.j}:yk=X Notice that yiand yjmay also be equal to 0if the variable space n-tuple is negated, yet what we have just said remains true since each Variable Set’s ntuple does not overlap other VSs by definition. We then have to analyze a crucial property of each clause in an SAT instance: Property 2.1.1 (De Morgan in Solution Set) Each 3-SAT clause in CNF form implicitly rules out a set of possible solutions (within the SS) of our 3-SAT problem, where three variables are asserted in a specific way. 5
Demostration 2.1.1 (De Morgan in Solution Set) Each 3-SAT clause in CNF combines three generic variables i, j, k ∈ {1, ..., n}: (xi+xj+xk) Where: xi, xj, xk∈ {0,1} If we where to apply De Morgan to this CNF clause we would get: (xi+xj+xk) = ¬(¬xi· ¬xj· ¬xk) That automatically rules out the solution where xi, xj, xkare asserted in the opposite way. Example 2.1.1 (of Property 2.1.1) Take this clause for example: (x1+x3+¬x4) Re-apply 4De Morgan to the single clause and you will get: (x1+x3+¬x4) = ¬(¬x1· ¬x2·x4) Hence you have that in a n= 4 3-SAT problem (0,0, X, 1) →(0,0,0,1) ∨ (0,0,1,1) do not solve the problem. Let us now demonstrate that: Theorem 2.1.1 (Solution Set Nature) (i) : an SS may be presented as a Venn’s Diagram where each set intercepts the others generating a total of 2nregions. That is: |U|= 2n Where nis the number of variables in the SS; (ii) : each region has cardinality one, e.g. contains only one element. Hence ∀B: |Vi\ ∀b∈B Vb−[ ∀c∈Bc Vc|= 1 Where Viis an arbitrary Variable Set and B⊂ {1, ..., n}−{i}. And: |U− 2n−1 [ i=1 (Vi\ ∀b∈B Vb−[ ∀c∈Bc Vc)|= 1 4I say re-apply because it is already used to put each SAT instance in CNF 6
Demostration 2.1.2 (Solution Set Nature) Let U be a general n-variables Solution Set. Due to how we defined it, each SS is composed of all the possible solutions that you may have with n-variables. Given that Ucontains each n-tuple ti(axiom i), and each variable in a n-tuple may assume either 1 or 0, you get that Uhas cardinality: |U|=|D2,n|= 2 ·2·2·... ·2=2n Proving (i). Each VS by definition assumes a variable is 1 while others may either be 0 or 1 (X) because of axiom (ii). Hence, for an arbitrary VS Vi: vi= (x1, x2, x3, ..., xn) : ∀k∈ {1, .., n}−{i}, xk=X, xi= 1 We may then untie each xk∈vi:∀k∈ {1, ..., n}−{i}in order to find each possible solution linked V1(using axiom ii), that is: |Vi|=|D2,n−1|= 2n−1 Then do the same for Vj, hence: vj= (x1, x2, x3, ..., xn) : j=i, ∀k∈ {1, .., n}−{j}, xk=X, xj= 1 And: |Vj|=|D2,n−1|= 2n−1 Then use axiom v: |Vi\Vj|=|v1·v2|=|D2,n−2|= 2n−2 You may continue by adding other VSs following this rule until you get: |(Vi\ ∀j∈{1,..,n}−{i} Vj)|= 2n−n= 20= 1 Leading us to the general rule: |(Vi\ ∀b∈B⊂{1,..,n}−{i} Vb)|= 2n−|B| Following this rule Let B⊂ {1, ..., n}−{i}, then: #solution in region =|Vi\ ∀b∈B Vb−[ ∀c∈Bc Vc|= 2n−|B|− |{1,...,n}|=n X j=|B|+1 2n−j= 2n−|B|− n X j=|B|+1 2n−j 7
But this is a finite geometric series, hence: n X j=|B|+1 2n−j=2n−|B|−1+1 −1 2−1= 2n−|B|−1 Then you have: |Vi\ ∀b∈B Vb−[ ∀c∈Bc Vc|= 2n−|B|−2n−|B|+ 1 = 1 For each subset B, hence each possible interception. Thus, this property extends to a total of 2n−1regions: that is, each possible interception given by the formula above. Lemma 2.1.1 (nature of 2n−1regions within SS) In a Solution Space there is a total of 2n−1regions created following rule: Vi\ ∀b∈B Vb−[ ∀c∈Bc Vc Proof 2.1.1 (nature of 2n−1regions within SS) Each region is given by an interception between Variable Spaces. The only solution that does not follow such a rule is v0= (0, ..., 0) since axiom v requires that that: ∃xi∈v∩:xi= 1 where v∩is the result of using axiom v on at least two VSs. But if there are a total of 2nregions as proved in (i), and only one region does not follow our Lemma: then we have 2n−1solutions that follow our Lemma, proving it. So there is only one ”special region” where the formula above is not valid, linked to (0,0,0, ..., 0). We can define it as: U− 2n−1 [ i=1 (Vi\ ∀b∈B Vb−[ ∀c∈Bc Vc) But if each region of the solution space has cardinality one, which is what we have just shown, then (ii)is demonstrated. Our Solution Set constitutes a map of our problem, as a basis might do in a vector-space. 2.2 Clause classification and 3-SAT subproblems We now further inspect our problem by classifying its clauses. 8
Example 2.2.1 Let us consider a 4-SS, that is, the Solution-Set of an SAT problem in four variables. In this scenario we may subdivide each clause in a class based on how variables are asserted in the clause we are considering. That is: Class 1: Each variable has value zero, so there is only one specimen for this class. One example might be: (¬x1,¬x2,¬x4) = (0,0, X, 0) linked to clause (x1+x2+x4) Class 2: One variable has value one, so there are three specimens this class: one for every variable put to 1.One example might be: (x1,¬x2,¬x4) = (1,0, X, 0) linked to clause (¬x1+x2+x4) Class 3: Two variables have value one so there are three specimens this class: one for every variable put to 0. One example might be: (x1, x2,¬x4) = (1,1, X, 0) linked to clause (¬x1+¬x2+x4) Class 4: Each variable has value one, so there is only one specimen for this class. One example might be: (x1, x2, x4) = (1,1, X, 1) linked to clause (¬x1+¬x2+¬x4) To each of these classes four 4 types of solution can be linked. Take class one for example and you may have: •(X, 1,1,1) •(1, X, 1,1) •(1,1, X, 1) •(1,1,1, X) Notice how shifting the X gives us different clauses: this behavior is extended to every other n-SS (with n > 3) due to the combinatorial nature of this structure (as I will show in Lemma 2.2.1.) Hence each solution is a different combination based on the X position. So the combination of three variables in a four-variable space is given by: 4 3= 4 Let us extend this to arbitrary n. Lemma 2.2.1 (Number of Clauses per Asserted Variables Position) In a n-SS clauses we may generate: n 3=n n−3=n! 3!(n−3)! =n·(n−1) ·(n−2) ·(n−3)! 3·2·(n−3)! = 9
2.3 Pn k=0 2kand Cumulative Preservation Before diving into our problem head first we have to examine a specific property, however obvious to the experienced reader, of the two-based finite geometric series (as the one in the title). I call this propriety Cumulative Preservation: Definition 2.3.1 (Cumulative Preservation) We call Cumulative Preservation the two-based finite geometric series property of being able to unequivocally discern each element in a partial sum where 2nis the greatest term. That is: Property 2.3.1 (Cumulative Preservation) Sn= n X k=0 2k= 2n+ 2n−1+... + 1 And a A a generic subset of indexes {0,1,2,...,n-1}. We can define the finte series S′as: S′ n= 2n+X a∈A 2a,∀generic subsets A of {0,1,2,...,n-1} S′exhibits Cumulative Preservation. Let us demonstrate it: Demostration 2.3.1 (Cumulative Preservation) Given the following sum: Sn= n X k=0 2k= 2n+ n−1 X k=0 2k= 2n−2n+ 1 = 1 Hence: n−1 X k=0 2k= 2n−1 This means that called ian element from B={1,2,3, ..., n}. Then: 2n> n−i X k=0 2k= 2|n−i|+1 −1,∀i∈B And for the same principle we have that: 2n> n−i X k=0 2k= 2|n−i|+1 −1> n−j X k=0 2k= 2|n−j|+1 −1,∀i, j ∈B:i>j 16
We can also prove that each generic subset follows a similar order. (Lemma 2.3.1) Define C and C’ two generic ordered6subsets of B each so that C, C′⊂B and they differ of at least one element (e.g. C={1,2,3}and C′={1,2,0}). Then, if c≥c′and max(C′)≤max(C)< n, ∀c∈C, c′∈C′: 2n+X C⊂B 2k>2n+X C′⊂B 2k′,∀C=C′, k ∈C, k′∈C′ Since each subset follows the rule above. This can be proved because by hypothesis either: 1. max(C′)< max(C) 2. max(C) = max(C′) In the first case you have that C and C’ sums are: 2max(C)+X D⊂C 2k>2max(C′)+X D′⊂C′ 2k′ With D, D′holding the same properties of Cand C′except that they might be the same subset due to how we constructed Cand C′. In that case we would have that: 2max(C)+X D⊂C 2k>2max(C′)+X D⊂C′ 2k That is: 2max(C)>2max(C′) Which means they are different numbers due to max(C′)< max(C). Else we would eventually find subsets Gand G′so that max(G′)< max(G). This process proceeds by eliminating same elements of the sums showing that each sum gives a different number based on the elements they do not have in common. An example might be: 2max(C)+ 2max(D)>2max(C′)+ 2max(D′) If C, C′had cardinality 2 and D, D′:D=D′had cardinality 1. In the second case (2.) we follow the same process described in (1.): so it is reduced to case one since the algorithm continues until it finds two different elements (that exist by hypothesis). This propriety is what we call Cumulative Preservation since we have just demonstrated that in a partial sum described as above exist at least two different terms that discern one partial sum from another. This property is essential to find an optimized version of our 3-SAT PolynomialTime solver algorithm. 6That is, each element xi> xj:i>jwith i, j set’s indexes (e.g {1,2,3}have indexes {0,1,2}) 17
3 3-SAT Polynomial-Time solver I will now proceed by theoretically describing my 3-SAT Polynomial-Time solver. A 3-SAT problem to be defined as such must have at least a 3-solution-space (e.g. be composed of three variables): else it would be impossible to create a clause using three variables, which is all 3-SAT is about. This distinguishes our 3-SAT problem into two subproblems: the first one I call ”Full-House Problem”, while the second one ”Combinatorial-Based problem”. We will now examine them further. 3.1 Full-House Problem (colloquially: Tonina’s problem) A 3-SAT problem is considered a Full-House Problem if it takes place in a 3-SS. Hence, a Full-House Problem is a 3-SAT problem in three variables, the most simple 3-SAT problem you may create. In order to solve it we classify each possible SS solution into the same four classes seen in Example 2.2.1, hence: Class 1: contains (0,0,0) Class 2: contains (0,0,1), (0,1,0), (1,0,0) Class 3: contains (0,1,1), (1,0,1), (1,1,0) Class 4: contains (1,1,1) To each of these we assign a specific element of the sum =P3 i=0 2ifinite series so that (x1, x2, x3)→(sum1, sum2, sum3). Each sum is initialized to 0.Then based on the solution given we prune the SS in order to find the correct solution: Class 1: we assign (sum1+20, sum2+20, sum3+20) if (x1+x2+x3) is inputted, meaning that (0,0,0) is not a solution. Class 2: we assign (sum1+21, sum2, sum3) if (¬x1+x2+x3) is inputted, meaning that (1,0,0) is not a solution. (sum1, sum2+ 21, sum3) if (x1+¬x2+ x3) is inputted, meaning that (0,1,0) is not a solution. (sum1, sum2, sum3+ 21) if (x1+x2+¬x3) is inputted, meaning that (0,0,1) is not a solution. Class 3: we assign (sum1+ 22, sum2, sum3) if (x1+¬x2+¬x3) is inputted, meaning that (0,1,1) is not a solution. (sum1, sum2+22, sum3) if (¬x1+ x2+¬x3) is inputted, meaning that (1,0,1) is not a solution. (sum1, sum2, sum3+ 22) if (¬x1+¬x2+x3) is inputted, meaning that (1,1,0) is not a solution. Class 4: we assign (sum1+ 23, sum2+ 23, sum3+ 23) if (¬x1+¬x2+¬x3) is inputted, meaning that (1,1,1) is not a solution. So our clauses are linked to each class based on this scheme: Class 1: linked to (x1+x2+x3). 18
Class 2: linked to (¬x1+x2+x3),(x1+¬x2+x3),(x1+x2+¬x3). Class 3: linked to (x1+¬x2+¬x3),(¬x1+x2+¬x3),(¬x1+¬x2+x3). Class 4: linked to (¬x1+¬x2+¬x3) Because of how we have assigned each element of the series we have that if all clauses are inputted then: (sum1, sum2, sum3)=( 3 X i=0 2i, 3 X i=0 2i, 3 X i=0 2i) = (15,15,15) And since each sum is a finite geometric series it shows Property 2.3.1 and each element may be unequivocally determined with the sum itself (e.g 15 = 8 + 4 + 2 + 1) by removing elements starting from the greatest one (23) to the lowest one(20): intuitively, if removing the element we are analyzing return a negative sum then that element was not inserted (e.g. sum = 23+ 22, then sum −23<0). So if a 3-SS 3-SAT instance is given then we associate each clause to an element from the series and then solve it by iteratively removing elements from each sum until we have that sumi(i∈1,2,3) is 0 and we move to the next one: if in doing so we find that an element was not inserted we have found ourselves the right solution. Suppose our sums are saved in a three-variables array, more rigorously the Full-House algorithm follows these steps: 1. Initialize each array’s variable to zero 2. input the problem by converting each assertion into a specific n-tuple of sums. 3. Save in ithe index of the lowest value within the array 4. Eliminate each element in sumistarting from 23down to 20: if removing an element returns a negative sumithen you have find a solution 5. Else sumi= 0 and you have no solution Step 5represents the worst case scenario: that is, all solutions have been inputted since the smallest among the values was 15. That is because every other sum’s value would have led to an element missing, hence a possible solution. This means that in the worst case scenario we have to check four possible solutions (and input eight clauses in our array). Definition 3.1.1 (How clauses are inputted) Generally each clause in CNF is inputted as a triplet of integers where the module identifies the variable and its sign whether it is negated (−) or not (+) 19
Example 3.1.1 (How clauses are inputted) (x1+¬x2+¬x5)−→ (1,−2,−5) With this in mind let us analyze our algorithm in pseudo-code7: Algorithm 1: Full House Algorithm 1: Input nand D[3][m] 2: Generate A[3] 3: for i= 0 to 2 do 4: A[i]←0 5: end for 6: for i= 0 to mdo 7: if D[0][i]<0 and D[1][i]<0 and D[2][i]<0then 8: A[0] ←A[0] + 20 9: A[1] ←A[1] + 20 10: A[2] ←A[2] + 20 11: else if D[0][i]>0 and D[1][i]<0 and D[2][i]<0then 12: A[0] ←A[0] + 21 13: else if D[0][i]<0 and D[1][i]>0 and D[2][i]<0then 14: A[1] ←A[1] + 21 15: else if D[0][i]<0 and D[1][i]<0 and D[2][i]>0then 16: A[2] ←A[2] + 21 17: else if D[0][i]<0 and D[1][i]>0 and D[2][i]>0then 18: A[0] ←A[0] + 22 19: else if D[0][i]>0 and D[1][i]<0 and D[2][i]>0then 20: A[1] ←A[1] + 22 21: else if D[0][i]>0 and D[1][i]>0 and D[2][i]<0then 22: A[2] ←A[2] + 22 23: else if D[0][i]>0 and D[1][i]>0 and D[2][i]>0then 24: A[0] ←A[0] + 23 25: A[1] ←A[1] + 23 26: A[2] ←A[2] + 23 27: end if 28: end for 29: max index ←0 30: for i= 0 to 2 do 31: Search greatest element in Aand save its index in max index 32: end for 33: max value ←A[max index] 34: counter ←3 35: while max value −2counter ≥0do 36: max value ←max value −2counter 7nis the SS size, mthe number of clauses inputted 20
37: counter ←counter −1 38: end while 39: Generate X[3] 40: if max value > 0then 41: if counter = 3 then 42: X[0] ←1 43: X[1] ←1 44: X[2] ←1 45: else if counter = 2 then 46: if max index = 2 then 47: X[0] ←1 48: X[1] ←1 49: X[2] ←0 50: else if max index = 1 then 51: X[0] ←1 52: X[1] ←0 53: X[2] ←1 54: else if max index = 0 then 55: X[0] ←0 56: X[1] ←1 57: X[2] ←1 58: end if 59: else if counter = 1 then 60: if max index = 2 then 61: X[0] ←0 62: X[1] ←0 63: X[2] ←1 64: else if max index = 1 then 65: X[0] ←0 66: X[1] ←1 67: X[2] ←0 68: else if max index = 0 then 69: X[0] ←1 70: X[1] ←0 71: X[2] ←0 72: end if 73: else if counter = 0 then 74: X[0] ←0 75: X[1] ←0 76: X[2] ←0 77: end if 78: end if 79: Return X This algorithm will be quite useful to optimize our Combinatorial-Based 21
algorithm: that is, the algorithm that finds a solution in a generic n-SS 3.2 Combinatorial-Based Problem (colloquially: Bianca’s problem) Definition 3.2.1 (Combinatorial-Based Problem) A 3-SAT problem is considered Combinatorial-Based if it has a n-SS with n > 3: that is, it is composed of at least four variables. As seen in section 2.2 these 3-SAT problems can be composed of at most P(n) = 4 3·(n3−3n2+ 2n) clauses. This idea can be explored further in order to make us have the right solution within the n-SS in polynomial time. We will need to use an 8(n+1)xn 3matrix called Combinatorial Matrix: where rows differentiate subproblems based on the values asserted8and each column differentiate subproblems based on which variables have been asserted9. Over this structure we will perform a series of operations that deterministically lead us to an exact solution to our 3-SAT problem, within its n-SS. But before getting any more technical let us demonstrate the principle that defines the correctness and soundness of our algorithm. 3.2.1 3-SAT as Composition of its Subproblems Theorem 3.2.1 (3-SAT as composition of subproblems) S= (x1, ..., xn) : ∀i∈ {1, ..., n}, xi∈ {0,1},n-SS solution that solves 3-SAT ←→ n 3non ruled out, coherent, distinct subproblem solutions Let me explain what non ruled out, coherent, distinct means: Definition 3.2.1.1 (Non Ruled Out) ∀c∈C:c=clause inputted, a subproblem solution Siis Non Ruled Out if: Siasserted in C=TRUE We may also rigorously define what an assertion is by saying: Definition 3.2.1.2 (Assertion) Assertion is a function that links a variable i∈c:cclause ∈Cto an element xi∈Si. 8e.g in a row you will find (X, 0,0,0),(0, X, 0,0), ... 9e.g in a column you will find (X, 0,0,0),(X, 0,0,1),(X, 0,1,0), ... 22
Example 3.2.1 (Assertion) (¬x2+¬x3+x4), Si= (X, 0,1,1, X)→(¬x2+¬x3+x4)=(¬0 + ¬1 + 1) = (1 + 0 + 1) = 1 To explain what coherent means we have to introduce two specific operations, called Composition and Contradictory Detection, used to generate our n-SS solution starting from a batch of its subproblem solutions. Let me first explain what I mean by contradictory: Definition 3.2.1.3 (Contradictory) xand x′subproblem solutions are contradictory if a function we call Contradictory Detector (d) that operates gets an element xi,x′ iand returns 0,1,X returns 0 (FALSE) for at least one couple xi, x′ i∈ {1, ..., n} Definition 3.2.1.4 (Non-Contradictory) xand x′subproblem solutions are non-contradictory if a function we call Contradictory Detector (d) that operates gets an element xi,x′ iand returns 0,1,X returns 1 (TRUE) ∀xi, x′ i∈ {1, ..., n} We now define the Contradictory detector as: Definition 3.2.1.5 (Contradictory-Detector) A function (d) that operates on two xi(∈x), x′ i(∈x′)subproblem solutions elements and returns a an element in D={0,1, X}in this way: d(xi,x′ i) = (0if (xi=x′ i= 1 ∨0) ∨(xi=X∧x′ iasserted)∨(xiasserted ∧x′ i=X) 1if (xi= 0 ∧x′ i= 1) ∨(xi= 1 ∨x′ i= 0) And our Composition is given by the Composition Operator: Definition 3.2.1.6 (Composition Operator, ⊗) Given x, x′Non-Contradictory subproblem solutions, Composition is a specific binary operation written as x⊗x′that works on each ordered couple xi,x′ iand returns an n-tuple containing: xi⊗x′ i= 1if xi=x′ i= 1 ∨(xi= 1 ∧x′ i=X)∨(xi=X∧x′ i= 1) 0if xi=x′ i= 0 ∨(xi= 0 ∧x′ i=X)∨(xi=X∧x′ i= 0) X ifxi=x′ i=X ∀i∈ {1, ..., n} Definition 3.2.1.7 (Coherent) Two or more subproblem solutions Si= (x1, ..., xn)and Sj= (x′ 1, ..., x′ n)are coherent if: ∀xk, x′ k∈Si, Sj:d(xk, x′ k)=0 23
Definition 3.2.1.8 (Distinct) Called Si, Sjtwo generic Subproblem Solution linked to X, they are Distinct if: ∃xi∈Si:x′ i(∈Sj)=xi, xi=X Demostration 3.2.1.1 (3-SAT as composition of subproblems) Let us first demonstrate (→). Suppose you already have S= (x1, ..., xn)that solves our 3-SAT instance. By definition of Subproblem Solution you have n 3Distinct subproblems. Each of these subproblems is generated by iteratively asserting a different variable’s triplet within Swhile putting the other variables to X(By definition of Subproblem Solution and how we defined S). This batch of solutions is made of Non Ruled Out solutions because each triplet of asserted values is a subset of S. That is: S= (x1, ..., xn) Si= (s1, ..., sn),where sj=xj, sk=xk, sm=xm And: ∀l∈ {1, ..., n}:l=j=k=m, sl=X We may prove this property by contradiction. Say you have: Si= (s1, ..., sn),where sj=xj, sk=xk, sm=xm But Simakes a generic inputted clause cfalse. It is impossible to have Sbeing a solution to the problem since one of its subset Simakes a clause false by definition of 3-SAT solution. Hence we proved our property. You also have that each subproblem solution Sigiven as above is Coherent by definition. You may also prove this by contradiction. Say you have two distinct subproblem solutions: Si= (s1, ..., sn) And: Sj= (s′ 1, ..., s′ n) Created following the same principle of the Siabove. Now suppose that using a Contradictory-Detector bit wise you get that: d(sk, s′ k) = 1 Then you have that: 24
sk, s′ k∈ {0,1}:sk=s′ k, k ∈ {1, ..., n} But each element is Sis fixed, that is: ∀i∈ {1, ..., n}, xi∈S:xi∈ {0,1} And you cannot have: xk=X Hence the contradiction since: (if xk=skthen you cannot generate Sjas a ’subset’ of S if xk=s′ kthen you cannot generate Sias a ’subset’ of S Now let us demonstrate (←). Definition 3.2.1.9 (Free Solutions Set) Call USia generic set containing each subproblem solution linked to a specific subproblem. USiis divided into Fand Fc Where Fis called Free Solution Set and: ∀S= (s1, ..., sn)∈Fc:Shas been ruled out using De Morgan So Fcontains those subproblem solutions that have not been ruled out by any clause, hence free solutions since they may be used to construct a n-SS solution and do not violate any clause inputted. It is just another way of saying that they are Non Ruled Out subproblem solutions. Now we have to identify a Coherent batch of distinct subproblem solutions within F. To do so consider a generic free-solution: Si= (s1, s2, ..., sn) : (si, sj, skasserted :i=j=k sm=X, ∀m={1, ..., n}, m =i, j, k And free-solution: Sj= (s′ 1, s′ 2, ..., s′ n) : (s′ i′, s′ j′, s′ k′asserted :i′=j′=k′ s′ m′=X, ∀m′={1, ..., n}, m′=i′, j′, k′ 25
subproblem then by definition our 3-SAT instance has no solution since there would be no way to solve (e.g. find a free solution) for at least one of its subproblems (the one we where examining). Batch Space Cut: as seen in Theorem 3.2.2.1 given a subproblem solution S′we know it is linked to C(n) = n−3 3·3 0+n−3 2·3 1+n−3 1·3 2 subproblem solutions where each addend (e.g. n−3 3·3 0) is a specific group of subproblem solutions with the same overlap class with S′12. Let me classify them more rigorously: Group 0, n−3 3·3 0:has zero overlaps with the starting subproblem solution S′. One example might be S′= (0,0,0, X, X, X) and S1= (X, X, X, 0,0,0); Group 1, n−3 2·3 1:has one overlap with the starting subproblem solution S′. One example might be S′= (0,0,0, X, X, X) and S1= (X, X, 0,0,0, X); Group 2, n−3 1·3 2:has two overlaps with the starting subproblem solution S′. One example might be S′= (0,0,0, X, X, X) and S1= (X, 0,0,1, X, X); During this phase we will eventually rule out, or rather ’cut’, some subproblem solutions within this batch of solutions based on two inference rules I will rigorously define later on since they represent the core of this algorithm. Composition: simultaneously to the BSC (Batch Space Cut) phase we compose our global solution (a model solution to our 3-SAT instance) based on the information given by the BSC. This phase will be discussed in a paragraph of its own, later on. (Check appendix A: BSC and how it solves 3-SAT decision problem) ——————————— To be changed —————————— Lemma 3.2.3.2 BSC rule 1 You have S′subproblem solution :S′asserts xi, xj, xkIf: (i): you have S1, S2∈Group2:(S1asserts xi, xj, x′ k′with k =k′ S2asserts xi, xk, x′ k′ (ii): you have S1, S2∈Group1:(S1asserts xi, x′ j′, x′ k′with k =k′, j =j′ S2asserts xj, x′ j′, x′ k′ And S1is ruled out, then: S2is ruled out 12There is no need to demonstrate this since is due to how we defined them in Theorem 3.2.2.1 32
Demostration 3.2.3.1 BPS rule 1 This is due to the fact that: S′⊗S1=S′⊗S2 So trying to compose a global solution with S′and S2(using the composition operator) would result in the same partial solution S′⊗S1which would not solve S1subproblem by definition (e.g. it ’solves’ that subproblem with S1which has already been ruled out). Lemma 3.2.3.3 BSC rule 2 You have S′subproblem solution :S′asserts xi, xj, xk. If: (i): you have S1, S2∈Group1:(S1asserts xi, x′ j′, x′ k′with k =k′, j′=j S2asserts xi, x′ j′,¬x′ k′ If S1, S2are ruled out then ∀S:x′ j′is ruled out (ii): you have S1, S2∈Group0: S1asserts x′ i′,¬x′ j′,¬x′ k′with k =k′, j′=j, i′=i S2asserts x′ i′,¬x′ j′, x′ k′ S3asserts x′ i′, x′ j′,¬x′ k′ S4asserts x′ i′, x′ j′, x′ k′ If S1, S2, S3, S4are ruled out then ∀S:x′ i′is ruled out (iii): you have S1, S2∈Group0:(S1asserts x′ i′, x′ j′, x′ k′with k =k′, j′=j S2asserts x′ i′, x′ j′,¬x′ k′ If S1, S2are ruled out then ∀S:x′ i′, x′ j′is ruled out Demostration 3.2.3.2 BPS rule 2 (i) : for each subproblem within Group1there are four solutions and they follow this scheme: 1. (xi,¬x′ j′,¬x′ k′) 2. (xi,¬x′ j′, x′ k′) 3. (xi, x′ j′,¬x′ k′) 4. (xi, x′ j′, x′ k′) Notice how two of them have x′ j′and two have ¬x′ j′13. So if 1.and 2.are ruled out you have that our global solution necessarily has x′ j′asserted (otherwise it would not solve our subproblem). So every subproblem solutions that asserts ¬x′ j′is ruled out. (ii) : it is the same that happens for (i)but in a Group0. (iii) : extends (i)to two variables in Group0. 13and the same happens to x′ k′ 33
Theorem 3.2.1 Subproblem Solution is Ruled Out by Input or BPS rules S:x′ i′, x′ j′, x′ k′asserted is ruled out ←→ follows BPS rules Demostration 3.2.3.3 Subproblem Solution is Ruled Out by Input or BPS rules (←):was demonstrated by lemmas 3.2.3.2 and 3.2.3.3 (→):Consider subproblem solution S′:xi, xj, xkasserted and we have the same situation as lemma 3.2.3.2 and 3.2.3.3 Let us now describe in practical terms how the algorithm works and then translate it into pseudo-code: Step 1: We generate our Combinatorial Matrix A: writing every possible subproblem solution there is (that is: 8×n 3). Each column is a subproblem, and each subproblem is strictly categorized based on the elements it asserts: we use another 3×n 3to categorize these problems, following a rule described in Definition 3.2.3.1. Step 2: Each subproblem solution has a ruled-out flag that is either 1 (e.g. our subproblem solution is ruled out) or 0 (that is, not ruled out). We set each flag to 0 at the beginning. Step 3: We input the problem, using De Morgan in order to understand which subproblem solution has to be ruled out: that is we set a subproblem solution ruled-out flag to 1 for each clause inputted. Step 4: We find the column with the least free solutions available: if there are more then one column with this property pick the first one. Operationally we simply generate a ruled-out solutions counter that counts how many ruled-out solutions each column has. if a column has more ruled-out solution then those analyzed before we update the ruled-out solutions counter and a variable that stores the column index. Step 5: We now examine each free solution within this column, starting from the first-most: that is, the one with the smaller row index. Notice that this step identifies S′. Step 6: Generate an nelements array: we will use it to generate the global solution to our problem. For each free solution that will be examined within Step 4 column we initialize this array to the specific free solution we are currently analyzing. 34
Step 7: Starting from subproblems of Group2 we analyze each subproblem solution within this group and apply BPS rules when one or more of these solutions has been ruled out. Step 8: When a BPS rule force us set a certain variable to a value (for example if BPS rule 2.(ii) applies), then we update our global solution array in order to follow said rule. Step 9: If by the end of our BPS phase did not completely ruled out a certain subproblem compatible solution (e.g. there is at least one free-solution, compatible with at least another from evert other subproblem) then we have found our global solution: notice that if our global solution has not asserted certain variables (e.g. we end up with (1,0,0, X, X, X) then we may assign to each Xwhatever value we what. Let us say that ∀xi= X, xi= 1, so to remove every ambiguity. Step 10: Else check the next subproblem free-solution within Step 4 column. After every solution has been analyzed, if non of them end with Step 9 then our problem has no solution. Before writing the actual pseudo-code here is the incremental rule I cited in Step 1: Definition 3.2.3.1 (Incremental Rule for indexes) Each variable asserted within a clause may be identified by their indexes within the n-tuple represented by the subproblem it refers to. So say you have a subproblem identified by its asserted variables si, sj, sk. That is: S= (s1, ..., sn) With: (si, sj, skasserted :i, j, k ∈ {1, ..., n}, i =j=k sm=X, ∀m∈ {1, ..., n}:m=i=j=k so that the subproblem is identified by the triplet: indexes = (i, j, k) You may order each of these triplets using this rule: Input n14 Start with indexes ←(1,2,3) i←1 j←2 k←3 while indexes = (n−2, n −1, n)do 14Problem input size 35
for k←j+ 1 to ndo k←k+ 1 indexes ←(i, j, k) Output indexes end for if j=n−1then j←j+ 1 else i←i+ 1 j←i+ 1 end if end while Example 3.2.1 (Incremental Rule for Indexes) So if you have n= 5 then the algorithm above gives the following indexes: 123 124 125 134 135 145 234 235 245 345 As said before we use this algorithm to save each subproblem in a structured way within our Combinatorial Matrix. So, in order to be able to check which subproblem is which within the Combinatorial Matrix, we also generate another matrix called: Definition 3.2.3.2 (Index Matrix) A3×n 3matrix where each row indicates a specific subproblem through the indexes of its asserted variables. So given a subproblem column we want to analyze using our algorithm, say subproblem 125 we already know which subproblems fall under the Group2 category: that is, 123,124,135,145,235,245. And which fall under the Group1 (e.g. 134,234,345) and Group0 (e.g. none for n= 5) category. So - in practical terms - all we have to do in order to check which subproblem is from which group we simply add an n+1 element (to each 3-tuple, hence to each row) that identifies the group number 0,1,2. So we simply iterate trough the Index Matrix and categorize each 3-tuple. Once we are done we iterate trough the matrix and analyze each 3-tuple with flag 2, then 1 and ultimately flag 0. Let me write down the rule and algorithm: Definition 3.2.3.3 (Group Detection Rule) Given Iand a starting subproblem solution asserted variables indexes array S′ I we may categorize each of I’s 3-tuple within a group from Group0, Group1, Group2 using the following algorithm: Input Iand S′ I= (i, j, k) Group2←false Group1←false Group0←false for each 3-tuple within Ido 36
Group2←I[row].i =i∧I[row].j =j∨I[row].i =i∧I[row].k =k∨ I[row].j =j∧I[row].k =k Group1←I[row].i =i∨I[row].j =j∨I[row].k =k if Group2and I[row]=S′then I[n+ 1][row]←2 else if Group1and not Group2and I[row]=S′then I[n+ 1][row]←1 else if not Group1and not Group2and I[row]=S′then I[n+ 1][row]←0 else if I[row] = S′then I[n+ 1][row]←315 end if end for Now let us write our algorithm more rigorously, in pseudo-code: Algorithm 2: Combinatorial Based Algorithm 1: Input n 2: Generate A[n 3][8(n+ 1)] 3: Generate I[n 3][3 + 1] 4: Use Incremental rule to initialize I 5: for each subproblem do 6: i←0 7: j←0 8: k←0 9: row ←0 10: while i=j=k= 1 do 11: subproblem solution array at row ←(i, j, k) 12: increment i, j, k in order to get each subproblem solution ▷We start from (0,0,0) →(0,0,1) →(0,1,0)... →(1,1,1) 16 13: row + + 14: end while 15: end for 16: for each inputted clause do 17: find subproblem solution based on how variables are asserted ▷Each clause is a 3-tuple of three values, e.g (-1,2,3), where the module indicates which variable is asserted (e.g. 2 = x2) and the sign indicates whether that variable is negated or not (e.g. −1 = ¬x1) 18: Set subproblem solution array’s n+ 1 element to 1 19: end for 20: Generate max index ←0 21: Generate ruled −out counter ←0 15Group3flag means that this subproblem is the same of S′ 16While every other element is put to X 37
22: Generate max ruled −out counter ←0 23: for each column in Ado 24: for each element in the column do 25: update max ruled −out counter if clause is ruled out 26: end for 27: if ruled −out counter > max ruled −out counter then 28: max index ←actual column index 29: end if 30: ruled −out counter ←0 31: end for 32: Generate composition array C[n] 33: Generate possible n-tuples matrix M[2 + 1 ·n−3 2][4] 34: for each subproblem solution in max index column do 35: C[n]←max index current subproblem solution 36: for each 3-tuple in Ido ▷We set the group flag for each 3-tuple 37: Use group detection rule 38: Store subproblem order in a array B[n]▷Were each subproblem is ordered based on its group (e.g. (10,3,5,1,6,2,4,7,8,9) → groups = (3,2,2,2,2,2,2,1,1,1)).So if we have n= 5 we know the first is the starting subproblem, then we have 6 subproblems from Group2, then 3 from Group1 39: end for 40: endCicle ←0 41: for each element within B[n] and not endCicle do 42: for each subproblem solution within subproblem do 43: if subproblem solution is ruled-out then 44: for every other Groupxsubproblem solution that follows BPS rule 1 do 45: rule-it out by setting n+ 1 element to 1 46: end for 47: if each subproblem solution within subproblem is ruled out then 48: endCicle ←1 49: end if 50: end if 51: end for 52: for each element within B[n] and not endCicle do 53: Generate array BPS2[2n]▷This array (of boolean numbers) is used to check which elements function as x′ j′ and x′ i′from BPS rule 2. BPS2= (x1,¬x1, ..., xn,¬xn). 54: Set each of its elements to 0 55: Generate arrayBPScounter[6]▷This array counts the occurrences of each x′ i′, x′ j′.BPScounter = [xicounter, ¬xicounter, xjcounter, ¬xjcounter, xkcounter, ¬xkcounter] 56: Set each of its elements to 0 57: Generate array stringBP Scounter[3 2·2] ▷ This array counts specific occurrence of 2-tuples x′ i′, x′ j′in order to follow 38
BPS rule2.(iii). That is BPScounter = [xi∧xjcounter, xi∧xkcounter, ...] 58: Generate array stingBP S2[2 ·n−3 2]▷Works as BP S2[n] but with specific 2-tuples (x′ i′, x′ j′) in order to follow BPS rule2.(iii). 59: end for 60: for each subproblem solution within subproblem do 61: if subproblem solution has at least one of its x′ xput to one in BPS2or stringBPS2then 62: rule solution out 63: end if 64: if solution is ruled-out and Group1then 65: Update BPScounter 66: for each element in BPScounter do 67: if BPScounter[element in 3−tuple]≥2then 68: BPS2[element]←1 69: if at least one BPS2[element] linked to C[i] = 1 then 70: endCicle ←1 71: else 72: set C[i] with the opposite of asserted value linked to BPS2[element] 73: end if 74: end if 75: end for 76: end if 77: if solution is ruled-out and Group0then 78: Update BPScounter 79: Update StringBPScounter 80: for each element in BPScounter do 81: if (BPScounter[element in 3−tuple]≥4then 82: BPS2[element]←1 83: if at least one BPS2[element] linked to C[i] = 1 then 84: endCicle ←1 85: else 86: set C[i] with the opposite of asserted value linked to BPS2[element] 87: end if 88: end if 89: for each element in stringBPScounter do 90: if (stringBP Scounter[2-tuple in 3-tuple] ≥2then 91: stringBP S2[2-tuple] ←1 92: if at least one BPS2[2-tuple] linked to C2-tuple = 1 then 93: endCicle ←1 94: else 95: Update M 96: end if 97: end if 39
98: end for 99: 100: if each subproblem solution within subproblem is ruled out then 101: endCicle ←1 102: end if 103: end for 104: if endCicle = 1 then 105: set each Xin Cto 1 106: Output ”Our solution is:” C 107: end if 108: 109: if the solution has not already been inputted then 110: Output ”There is no solution” 111: end if So, before going any further and examine the complexity of such algorithm we have to prove two other things: why examining a column with the lowest number of free solutions is enough to say wether a n-SS solution exists or not? This may be answered by the following lemma: Lemma 3.2.3.4 (One column is enough) Examining each free-solution in a Combinatorial Matrix’s column is enough to check all possible overlaps and all possible combinations of n 3subproblems in a n-solution-space, and hence solving our each 3-SAT instance Demostration 3.2.3.4 (One column is enough) This is due to the fact that examining one subproblem free solutions shows us how each of these free solution is linked to other subproblem solutions in other subproblems. Ending its examination with Step 7 means that each possible nsolution-space solution ended with a contradiction, hence we have to shift it to Fcsince we want to find a coherent, Non-Contradictory solution (as shown in Theorem 3.2.2.1). If all solutions end with Step 7 then no subproblem solution within the column gives a Non-Contradictory solution: hence we have to shift all of them to Fc: but if all of them are ruled out then there is no solution that satisfies all possible subproblems, hence there is no solution that satisfies our 3-SAT instance. Hence our algorithm can be greatly optimized by searching for the column with the least amount of free-solutions as this represents a bottleneck to the number of operations we have to perform. 3.2.4 Algorithm Complexity Now we only have to study the algorithm’s complexity and verify it is polynomialtime. Let me use asymptotic analysis to analyze the worst case scenario 40
Theorem 3.2.1 (Algorithm Complexity in worst-case scenario) Each Combinatorial-Based Problem that uses a Combinatorial Matrix has Θ(n4) complexity in the worst-case scenario Demostration 3.2.4.1 (Algorithm Complexity in worst-case scenario) Each Combinatorial-Based Problem is divided into the following phases: 1. Input Phase; 2. Column Selection; 3. Free-Solution Examination; 4. BPS: group 2, 1 and 0; 5. Composition Examination; For the first phase we have that each subproblem solution exists within the Combinatorial Matrix as an n+1 array. We have a one to one conversion from clause to array since each clause inputs three variables, ordered within a set of n variable: while our array inputs three assertion and puts every other element to X (that operatively may be whichever unsigned int or int that is not 1or 0). If the total amount of possible clauses is n 3, then we have total complexity: Θ(n·n 3·8) = Θ(n·P(n)) = Θ(n4) Where n 3·8is the matrix’s dimension. Then we have to input the Index Matrix. Hence: Θ(4) ·Θ(P(n)/8) = Θ(n3) We then initialize Iusing the incremental rule, check the algorithm written in Definition 3.2.3.1. and you will see that the while cycle ends in n 3iterations, hence: Θ(n3) We then initialize A: each subproblem solution follows a specific incremental rule that may be generated by a series of nested ifs, so global cost is simply: Θ(n·n 3·8) = Θ(n·P(n)) = Θ(n4) Since we access one element within the matrix once, Then we have to use De Morgan to mark each subproblem solution that has been ruled-out: in the worst case scenario, we search the specific column we have to analyze using Iand then search the right subproblem solution to rule out by examining each array within the column and eventually put its n+ 1 element to 1. This means: Θ(m)·Θ(8n) = Θ(n3)·Θ(8n) = Θ(n4) 41
1. (0,0,0,0,0) violates (x1+x3+x5) 2. (0,0,1,0,0) violates (x1+x2+¬x3) 3. (1,0,0,0,0) violates (¬x1+x3+x4) 4. (1,0,1,0,0) violates (¬x1+¬x3+x5) Proving our cut was correct. Let us now demonstrate the correctness of this cut: Theorem 5.0.1 (BSC Resolution Cut correctness) Every subproblem solution eliminated by our BSC Resolution Cut cannot satisfy the formula. Demostration 5.0.0.1 (BSC Resolution Cut correctness) Let k= 1, then we have that our cut is: for i = 0..1, ki∈KV:Ai∧ki ∧iAi Where KV={0,1}hence we may write our cut as: S0= (A0∧k0), S1= (A1∧k1) R=A0∧A1 That is: S0={s0SS n−tuple :follows A0assertions, bit k = 0}, S1={s1SS n−tuple :follows A1assertions, bit k = 1} And: R={rSS n −tuple :follows A0∧A1} Hence: R=S0∪S1 That means that ruling out S0and S1means ruling out R. We may extend this thought to k=n: for i = 0..2n−1, ki∈KV:Ai∧ki ∧iAi Which follows what we said for k= 1 but with: R= n [ i=0 Si Hence we have the same result: that is, ruling out every Sirules out R. So BSC Resolution if applied within the combinatorial matrix finds us every possible ruled-out solution we may directly derive from already ruled-out subproblem solutions: but in order to find every ruled-out subproblem solution within the matrix we have to use the following rule also. 48
Definition 5.0.0.3 (BSC Propagation cut) Given E a ruled-out solution, then: E S,∀S:E⊆S Hence Sis also ruled-out. This rule states that if a string contains an already ruled-out k-tuple Ethen it is also ruled out. Its correctness may be easily demonstrated: Theorem 5.0.2 (BSC Propagation cut correctness) Every subproblem solution eliminated by our BSC Propagation Cut cannot satisfy the formula. Demostration 5.0.0.2 (BSC Propagation cut correctness) Say Eis a ruled out solution: by definition asserting bits in such a way that they follow E’s assertions means that we are inserting an unsatisfiable global solution (we are not inserting a model). Hence every solution Sthat contains Eis also ruled out. Together, these two cuts form an inference system that eliminates every subproblem solution which, if included in a global assignment, would violate at least one clause from the original formula. In order to demonstrate this we have to demonstrate that this system is complete. Theorem 5.0.3 (BSC Resolution + BSC Propagation is complete) Once we iteratively use BSC Propagation an BSC Resolution we end up having at least one non ruled-out subproblem solution for each subproblem, with which we may use to generate a model. Demostration 5.0.0.3 (BSC Resolution + BSC Propagation is complete) Let ϕ=C1∨... ∨Cmbe a 3-SAT CNF problem and M:{x1, ..., xn} → {0,1}: M|=ϕ. As we know each clause is linked to a ruled-out string Siso that Si∈Fc: Ci= (xj+xk+xl)→Si=(xj, xk, xlare asserted ∀pindex ∈Ci:p=j, k, l →xp=X Once we have applied each BSC Resolution and Propagation we have that: Lemma 5.0.0.1 ∀Si∈Fcis not compatible with M Which may be demonstrated with a proof by contradiction. Say: ∃Si∈Fccompatible with M 49
That means that: Mj=xj,Mk=xk,Ml=xl But each of the rules we derived Sifrom is proven to be sound (De Morgan, BSC Propagation, BSC Resolution): hence, Sicannot be compatible with M, leading to a contradiction. So every Mcompatible sub-string within our combinatorial matrix has to be ∈F. This means that we may find at least one Si:Si= (Mj, Mk, Ml),∀i, j, k ∈ {0..m}:i=j=k, hence proving our system completeness. 6 Appendix B: 3-QBF reduction to 3-SAT (PSPACE = NP = P) ——————— Note to the reader: check out Appendix C since if proven to be true it also proves PSPACE=P because it transforms the 3-SAT associated to the 3-QBF in a 2-SAT. ——————— Even a wilder assumption on the nature of computational complexity can be made when analyzing and even harder problem: QBF, or Quantified Boolean Formula. As its name suggests, QBF is an SAT variant where variables are associated to either an universal quantifier (∀) or an existential quantifier (∃). To get a broad understanding of QBFs here is an example: ∀x1,∃x2: (x1+x2)·(¬x1+x2) You can clearly see how it adds another layer of complexity to an already hard problem as SAT is. As a matter of fact QBF is classified as PSPACEcomplete, where PSPACE is a complexity class that contains NP: e.g. NP ⊆ PSP ACE. This appendix wants to show how we can reduce QBFs to SAT in polynomial time: hence showing how PSPACE = NP. The technique I will later explain is based on the following concept. Given a QBF problem we can subdivide it into ”subproblems” without changing its logic, that is: ∀x1,∃x2, ..., ∃xn−1,∀xn:ϕ(x1, ..., xn) = ∀x1: (∃x2,∀x3: (...(∃xn−1,∀xn:ϕ(x1, ..., xn))) So we modularity solve the problem starting form the inner-most ’block’, that is ∃xn−1,∀xn:ϕ(x1, ..., xn). Before jumping to the following ’block’, every ruledout solution linked to the ’block’ will be added to a list of ruled-out solutions. Let me show how the technique works with some examples. Let us say you have the following 3-QBF instance: ∀x1,: (∃x2,∀x3: (x1+x2+x3)·(¬x1+x2+x3)) 50
As we have extensively seen in the 3-SAT proof we have that each clause is linked to a ruled-out solution. For example, in the 3-QBF from before we have that: ((x1+x2+x3)→(0,0,0) (¬x1+x2+x3)→(1,0,0) The first step is to check wether the 3-SAT linked to our QBF instance is UNSAT: to do so we employ the algorithm used to solve 3-SAT17. Hence we end up having the following ruled out solutions: (0,0,0) (1,0,0) − − −− (X, 0,0) The next step is to analyze the following subproblem: ∃x2,∀x3: (x2+x3)·(x2+x3) Hence the following solution is ruled out: (X, 0,0) That already was within the ruled-out solutions list. So we continue by examining the next subproblem: ∀x1,: (∃x2,∀x3: (x1+x2+x3)·(¬x1+x2+x3)) That is, we have to check wether (0, X, X, X)∨(1, X, X, X) is ruled-out: (0,0,0) (1,0,0) (X, 0,0) You can clearly see that (0, X, X, X), nor (1, X, X, X) have been ruled out: hence our problem has a solution. Another example might have been: ∀x1,(∃x2,∀x3: (x1+x2+x3)·(x1+¬x2+¬x3)·(¬x1+x2+¬x3)·(¬x1+¬x2+x3)) We then have: (0,0,0) (0,1,1) (1,0,1) (1,1,0) 17For now you may check the code linked to this preprint to get a sense of what I’m talking about 51
So we analyze: ∃x2∀x3: (x2+x3)·(¬x2+¬x3)·(x2+¬x3)·(¬x2+x3) That is: (X, 0,0) (X, 1,0) (X, 0,1) (X, 1,1) − − −− (X, X, 0) (X, X, 1) (X, 0, X) (X, 1, X) − − −− (X, X, X) Notice how both the ∃x2and ∀x3are violated since the first one was asking: ¬[(X, 0, X)inserted ∧(X, 1, X)inserted] While the second one was asking: ¬[(X, X, 0) inserted ∨(X, X, 1) inserted] Hence the problem has no solution. So in general the problem consists of following the technique described above iteratively, starting from the innermost pair of variables, unfolding a pair of variable for each step in order to find wether the following rules are violated: (∀xi=¬(xiinserted ∨ ¬xiinserted) ∃xj=¬(xjinserted ∧ ¬xjinserted) Where by ”inserted” I mean inserted into the ruled-out solutions list. Notice how each step consists of generating at most O(n3) ruled-out-solutions for each step. If the number of steps is n 2then we have O(n4) iterations at most. 7 Appendix C: reduction to 2-SAT As we already know each 3-SAT problem may be written in CNF form, that is: (i+j+k)·other clauses such as the first one The main problem a 3-SAT CNF clause has is that it does not explicitly says which combinations satisfy the clause. Usually in order to do so we have to 52
write the clause in DNF, that is explicitly write down seven combinations of three literals: C= (i+j+k) = ijk +¬ijk +i¬jk +ij¬k+i¬j¬k+¬ij¬k+¬i¬jk If you look closely this expression may be reduced to: (i+j+k)=(i+j+¬jk) = T(C) That is, we were able to reduce the 3-SAT CNF clause to an equivalent 2-form. Without further ado, let us prove this equivalence. Lemma 7.0.0.1 (3-SAT CNF clause reduction to 2-form) Let Cbe a generic 3-SAT CNF clause so that: C= (i+j+k) C may be reduced to T(C). Demostration 7.0.0.1 (3-SAT CNF clause reduction to 2-form) As we have already extensively shown in previous chapters: (i+j+k)≡ ¬(¬i· ¬j· ¬k) That is: (i+j+k)≡T(C) While I simply derived this from the group of possible assignments the clause has, we may demonstrate it more extensively by using a table truth: T(C) = i=true, j =true, k =true →true i=true, j =false, k =true →true i=true, j =true, k =false →true i=true, j =false, k =false →true i=false, j =true, k =true →true i=false, j =false, k =true →true i=false, j =true, k =false →true i=false, j =false, k =false →false As you may notice it has the same truth table of (i+j+k), that is: (i+j+k)≡T(C) So i+j+¬jk is the 2-form of (i+j+k), a generic 3-SAT CNF clause. We may now write each 3-SAT CNF input as: 3−SAT =C1·C2·... ·Cm≡T(C1)·T(C2)·... ·T(Cm) 53
As we know Hp →Th, hence: Hp →Th ≡ ¬Hp +Th Hence we may rewrite our generic T(C) as: T(C) = i+j+¬jk = (¬jk) + i+j=¬Hp +Th = (j+¬k)→(i+j) There are six equivalent expressions to write T(C) using the rule above. So we may write T(C) as a conjunction of those expressions: T(C) = i+j+¬jk ≡(j+¬k)→(i+j) i+j+¬ik ≡(i+¬k)→(i+j) i+k+¬kj ≡(k+¬j)→(i+k) i+k+¬ij ≡(i+¬j)→(i+k) j+k+¬ji ≡(j+¬i)→(j+k) j+k+¬ki ≡(k+¬i)→(j+k) And we may use the contrapositive in order to add new information about the opposite nodes: T1(C) = (j+¬k)→(i+j)≡(¬i¬j)→(¬jk) (i+¬k)→(i+j)≡(¬i¬j)→(¬ik) (k+¬j)→(i+k)≡(¬i¬k)→(¬kj) (i+¬j)→(i+k)≡(¬i¬k)→(¬ij) (j+¬i)→(j+k)≡(¬i¬k)→(i¬j) (k+¬i)→(j+k)≡(¬j¬k)→(i¬k) We also know that: (i+j+k)≡(¬i¬j)→k We may add literals we know will be false when the hypothesis is true in order to create a ”fake” disjunction. Hence the general clause becomes a conjunction of: T2(C) = (i+i+j+k)≡(¬i¬j)→k+i (i+i+j+k)≡(¬i¬k)→j+i (i+j+j+k)≡(¬j¬i)→k+j (i+j+j+k)≡(¬j¬k)→i+j (i+j+k+k)≡(¬k¬i)→k+i (i+j+k+k)≡(¬k¬j)→k+j 54
We may also use their respective contrapositive in order to add more information: T3(C) = (¬k¬i)→i+j (¬j¬i)→i+k (¬k¬j)→i+j (¬i¬j)→k+j (¬k¬i)→i+k (¬k¬j)→k+j Now, a deeper analysis must be done for the opposite implication (e.g. (i+j)→ ¬k¬i), that is because: (i+j)→ ¬k¬i≡(¬i¬j)+(¬k¬i) = ¬i(¬j+¬k) That does not automatically lead to a single CNF clause or a T(C) form. Yet something may be done by looking at its truth table: (i+j)→ ¬k¬i= i=true, j =true, k =true →false i=true, j =false, k =true →false i=true, j =true, k =false →false i=true, j =false, k =false →false i=false, j =true, k =true →false i=false, j =false, k =true →true i=false, j =true, k =false →true i=false, j =false, k =false →true Now knowing that each T(C) (or CNF clause) makes only a single assertion false, that is T(C)=(i+j+k)≡i+j+¬jk =¬(¬i¬j¬k) We may write the implication above as a conjunction of T(C) implications, that is18: mixed impliction = (i+j)→ ¬k¬i≡T4(C) = (¬j+¬k)→(¬i+¬j) (¬j+k)→(¬i+¬j) (j+¬k)→(i+¬j) (j+k)→(i+¬j) (¬j+k)→(¬i+j) One may prove this equivalence by simply looking at their respective truth table, but in here I will simply prove it by using Lemma 7.0.0.1. 18Whenever I write a system of implications it means all the implications are in conjunction(AND, (·))with one another 55
Lemma 7.0.0.2 (Lemma 7.0.0.1. Corollary) (i+j)→ ¬k¬i≡T4(C) Demostration 7.0.0.2 (Lemma 7.0.0.1. Corollary) As Lemma 7.0.0.1 demonstrates: (j+¬k)→(i+j)≡(i+jk +¬jk) = (i+j+k)≡ ¬(¬i¬j¬k) So T4(C)becomes: T4(C) = ¬(ij¬k) ¬(ijk) ¬(i¬j¬k) ¬(i¬jk) ¬(¬ijk) Hence T4(C)and (i+j)→ ¬k¬ishare the same truth table and are thus logically equivalent. As a consequence we have that: Lemma 7.0.0.3 (3-SAT reduction to form2) F= 3 −SAT CNF input =∧m i=1"T(C)·T1(C)·T2(C)·T3(C)#· · ∧mixed implications "mixed implication ·its contrapositive#= =form2(F) Demostration 7.0.0.3 (3-SAT reduction to form2) Direct consequence of lemmas 7.0.0.1 and 7.0.0.2 Specifically, since each implication we created is equivalent to a 3-SAT CNF clause (or a block of them) from the input, solving a form2is the same thing as solving a 3-SAT CNF problem because we did not alter any table truth, we created equivalent clauses (the implications) in conjunction with one another, as the 3-SAT CNF. We may now demonstrate that form2creates a fully skewsymmetric implication graph. Lemma 7.0.0.4 (form2is fully skew-symmetric) Our form2implication graph has the following properties: ∀(v→u),∃(¬u→ ¬v) With v, u nodes in the implication graph. And it is transitively closed. 56
Demostration 7.0.0.4 (form2is skew-symmetric) In a 3-SAT nodes are either (i+j)or (i·j)(with i, j generic literals). Thanks to lemma 7.0.0.2 and lemma 7.0.0.1 we know that you may create these connections: (i+j)→(j+k) (¬i¬j)→(¬j¬k) (¬ij)→(j+k) (¬j¬k)→(j+k) Hence the graph given is skew-symmetric. Using these rules, starting from any node we want we are able to reach each other node within the graph. That is, given (i+j),(ij),(lk),(l+k)generic nodes, the following paths are allowed: 1.(ij)→(lk) 2.(ij)→(l+k) 3.(i+j)→(lk) 4.(i+j)→(lk) In fact we may reach them through: 1.(ij)→(jl)→(lk) 2.(ij)→(¬j+l)→(l+k) 3.(i+j)→(¬il)→(lk) 4.(i+j)→(i+l)→(l+k) This covers the fact that the graph is fully skew-symmetric since it proves the graph is transitively closed and skew-symmetric. Lemma 7.0.0.5 (Lemma 7.0.0.4 corollary: graph correctness and completeness) Given G= (V, E), the implication graph I described, and the original 3-SAT CNF problem F, we have that: ∀assignment α :α|=G←→ α|=F Demostration 7.0.0.5 (Lemma 7.0.0.4 corollary: graph correctness and completeness) Direct consequence of Lemma 7.0.0.4. We have in other words found an implication graph completely equivalent to that of 2-SAT: that is, finding an SCC (Strongly Connected Component) that links a node and its opposite (e.g. (i+j)↔(¬i¬j)) in this graph means that the 3-SAT we started from is UNSAT. Otherwise we have a SAT problem. So, 57