1. For the presented 3SAT solver algorithm to be polynomial, effective jumps via base literal access are required because there could be an arbitrary difference between the highest order among the limit literals and n (eg, 100 or 1000), resulting in a requirement of an exponential number of effective jumps offered by limit literals.

2. Effective jumps offered by base literal access are not possible. Suppose you have 4 successive jumps resulting in two limit literals that are inverses of each other. You may now replace the final jump with the 2nd-lowest-ordered limit literal, leaving one more limit literal to clear before base access can be achieved. In order to do this, you must have another 2 jumps, which creates 2 additional limit literals that must be cleared. To do this, you must create an additional 4 successive jumps, resulting in 4 more limit literals that must be cleared to achieve base literal access. This sequence repeats indefinitely. The only exception to this is where the 4 limit literals all are of the same variable, and this cannot be guaranteed in the worst case.

3. We consider 3SAT solver algorithms that traverse the search space in some organized fashion. Advances through the search space of magnitude 2^y where y is an arbitrary number, featuring constant-size logic to identify said advancements, is the best you can do as n grows large. Assume not. Assume there is a heuristic-based algorithm like DPLL or one of its variants. Because no heuristic applies to all logic instances, when the heuristic fails, in the worst case all possibilities must be exhaustively tried. In this case, we advance through the search space with jumps of magnitude 2⁰, which is worse than jumps of magnitude 2^y where y is an arbitrary number. What about a constant number c of advances through the search space? Not polynomial. Assume there is some technique to develop the logic to advance through the entire search space of n variables by a constant number of times, c. Now increase n by 1: n+1. In the worst case, the complexity of the logic doubles, so the technique to advance through the search space c times doubles in logical complexity, which is exponential. What about advances through the search space by 2x where x = f(n), where f(n) != n - c' (which would also necessarily employ a technique that doubles in logical complexity when n is increased by 1)? As n grows large, these all become exponential.

4. This shows that 3SAT is not polynomial in the worst case when traversing a search space.

Interestingly, the algorithm used in this proof may also prove that IMSAT is polynomial because the one variable shared by all clauses would be the base literal in each clause and it's only a distance of 1 above the highest limit variable. This would be the highest-order bit of Z, and since we chop the search space into 4 equal partitions, this bit (and the one immediately below it) are automatically set based on the partition sequence number. Therefore, the shared variable represented by this bit doesn't need to be accessed from the advancement process.

System and Method for Solving Logic Instances

Background of the Invention

[0001]

Abstract

We introduce a method of solving boolean 3-satisfiability logic instances by testing for the coverage of clauses that evaluate to false. We show how to set up a search space that represents a logic instance and identify 3 ways to advance forward through this search space, each corresponding to one of the 3 literals of the clause that we label the “jump”, the “limit”, and the “base”.

We Claim

1. The process of chopping (dividing) the search space into multiple partitions, with each partition no larger than ¼ of the entire search space.
2. The identification of where a jump offered by a jump literal (a jump literal being the lowest-order literal of a clause) is immediately succeeded by a jump offered by its inverse in the immediately-succeeding cycle and the replacement of the second jump with an effective jump offered by the lower-order of the limit literals of the two clauses as a new effective jump (a limit literal being the second-lowest-order literal of a clause).
3. The identification of where four successive jumps were replaced by two effective jumps offered by limit literals, as described above in claim 2, and where all limit literals among these four clauses use the same variable, and where one limit literal among the first two clauses is the inverse of one limit literal among the second two clauses, and the replacement of the effective jump offered by the second pair of limit literals by an effective jump offered by the lowest-order of the base literals of the four clauses (a base literal being the highest-order literal of a clause).

Specification

[0001] For a logic instance having n binary variables and k clauses we create an n-bit number Z and assign each binary variable to a unique bit location on Z. Starting with the beginning of the portion of the search space, we advance Z forward through the search space by what we’ll call “jumps” whereby for each jump a bit is identified that can be inverted. We continue identifying these bits and inverting them until either the entirety of all portions of the search space are found to have coverage of clauses evaluating to false or a value of Z is found not to have any available jumps, whereby the truth values of the bits of Z represent a satisfying assignment of truth values for the logic instance. We label the lowest-order literal of a given clause the “jump” literal, we label the second-lowest-order literal of that clause the “limit” literal, and we label the highest-order literal of that clause the “base” literal. Below we also show the conditions under which a jump can be replaced by a limit or a base to create a new effective jump of a higher order.

[0002] A jump literal x is identified when for a given value of Z one of the k clauses evaluates to false. Observe that when this occurs, all values of Z having the same bit values of higher- and equal-order to the jump variable x are covered (“coverage of clauses that evaluate to false”) by this one clause, and until we advance Z to the location where the bit value of x inverts. Carrying this strategy forward, if a jump is immediately followed by its inverse, we can replace the second jump by a new effective jump offered by the lower-order of the limit literals of the clauses containing the two successive jumps. We can do this because all values of Z up to the value where the lower-order limit literal inverts contain one of those two clauses evaluating to false. Carrying this strategy forward once more, when we identify two successive effective jumps offered by limit literals that are inverses of each other, where all four clauses feature literals of the same variable, we have identified a condition where all values of Z contain one of those two clauses containing our limit literals evaluating to false up to the location where the lowest order base literal among all four of our clauses inverts. When multiple clauses evaluate to false as a result of the value of Z being tested, we utilize the greedy approach and select the clause giving us the highest effective jump. When a clause has one false truth identity in it, we only consider the limit literal, and when a clause has two false truth identities in it, we only consider the jump literal.

[0003] When we invert a bit, we are adding a perfect power of 2 to Z, which means that we perform any carry operations just as we would with the addition of any two numbers in order to guarantee that we are advancing in exactly one direction through the search space- from lower values of Z to higher ones. After performing the addition operation on Z, we set all bits of lower order than this bit’s order to false because between the value of Z having all false values of lower order this bit’s order and the value of Z without having set these values to false there could be a value of Z that results in no clauses evaluating to false, which represents a satisfying assignment of truth values for the instance.

[0004] Note that an effective jump offered by a limit literal or base literal is never guaranteed and may not be available, and as all clauses have exactly 3 literals, the 2 highest-order bits of Z may not be accessible. To resolve this we chop the search space into at least 2^p equal partitions, as described in claim 1, where p is greater than or equal to 2, and encode each of the permutations of the p bits into the highest-order bits of each of the 2^p corresponding search space partitions. Obviously, we do not choose a power of p that is so large that it takes an excessive amount of time to process. All bits of the initial value of Z of lower order than the uppermost p bits of the permutation are set to 0.

[0005] When we modify a bit in the uppermost bits that have been permuted as a result of chopping (partitioning) the search space into at least 2^p equal partitions where p is greater than or equal to 2, as described in claim 1, either by the effective jump offered by the limit literal as described in claim 2 or by the base literal as described in claim 3, or otherwise by the carry operation of the effective addition that occurs as a result of inverting a bit set to true upon discovering a jump offered by a jump literal that cannot be replaced with an effective jump of higher order, we terminate the search of this chop (partition) and we conclude that clauses evaluating to false cover the entire partition.

[0006] When we look for a jump offered by the bits of a value of Z and discover that no clauses evaluate to false, we have discovered a corresponding satisfying assignment of truth values to the variables of the instance. In this case, we return these values of Z back to the function that invoked the call to the function that determines whether a partition is satisfiable.

References