System and Method for Solving Logic Instances

Background of the Invention

[0001] Presented in 1971 by Stephen Cook [1], the P vs NP Problem has been called the most important unsolved problem in computer science [2]. The boolean satisfiability problem is one NP-Complete problem [3]. Any boolean satisfiability problem instance can be converted to a equisatisfiable boolean 3-satisfiability (3SAT) problem instance. If a solution to one NP-Complete problem has polynomial time complexity in the worst case, then all NP-Complete problems have polynomial-time solutions in the worst case, and P = NP.

Abstract

We introduce a method of solving boolean 3-satisfiability (3SAT) logic instances of n variables and k clauses by advancing through a search space that is formed by assigning the bit positions of an n-bit binary number Z to variables of the instance. We start with the initial value of Z, which is either all false values or the initial value of a partition of the search space having false values below the partition values, and we form a boolean 2-satisfiability (2SAT) instance from the information available in the 3SAT clauses. Based on the satisfiability of the 2SAT instance, we either form a new 2SAT instance with an additional bit, we exit with satisfiability of the 3SAT instance, we modify the value of the bit, or we exit with non-satisfiability of the 3SAT instance.

We Claim

1. The formation of a boolean 2-satisfiability (2SAT) instance by taking the values of the variables at the bit positions of an n-bit binary number Z from n - 1 down through to an index position identifier ix where said 2SAT clauses are formed when the literals at the bit positions evaluate to false where those literals are present in any of the boolean 3-satisfiability (3SAT) instance clauses, with the 2SAT member variables being the other two literals of said 3SAT clauses containing said literals evaluating to zero.
2. The increasing and decreasing of the index position identifier ix- from claim 1- through the bit positions of the search space that is formed from assigning the n bits of the boolean 3-satisfiability instance to an n-bit binary number Z based on the outcomes of the solutions of the boolean 2SAT instance mentioned in claim 1, where if a 2SAT instance is satisfiable and ix is greater than zero (2 is 0 in our implementation case because since 0 and 1 are reserved, the zeroth bit position is 2), then ix is decreased by 1; or where if a 2SAT instance is satisfiable and ix is equal to zero (again, 2 is 0 in our case), then we have found a satisfying assignment of truth values in the values of Z for the 3SAT instance and we return satisfiable; or where if a 2SAT instance is not satisfiable, we set all bit values of Z of lower order than ix to false and perform an addition and any associated carry operations to the bit of Z at ix; or finally where we have reached the end of the search space or the end of the current partition of the search space and we find that the corresponding 2SAT instance is not satisfiable, resulting in a not-satisfiable return value for the said search space or search space partition.

Specification

[0002] Consider the following set of conjoined 3 conjunctive normal form (3CNF) clauses: (a | b | c) & (d | b | e) & (f | ~b | g) & (h | ~b | i). If the value of b is set to false, then the literal b evaluates to false, and we observe that both either a or c must evaluate to true and either d or e must evaluate to true: (a | c) & (d | e). If the value of b is set to true, then the literal ~b evaluates to false, and we observe that both either f or g must evaluate to true and either h or i must evaluate to true: (f | g) & (h | i).

[0003] We start with the highest-order value of Z- indicated by ix- that is not pre-set by the partitioning process and first set it to false (0) as well as all bits of lower order than ix. We draw a set of implied 2CNF information as described above from the bits going from order n-1 down through ix. We run a 2SAT solver on that and see if it’s satisfiable. If the 2SAT instance is satisfiable and ix is greater than 0 (2 is 0 for us in our implementation case), we decrease ix by one. If the 2SAT instance is satisfiable and ix is equal to 0 (again, 2 is 0 for us), we have found a satisfying assignment of truth values in the values of Z for the 3SAT instance being tested, and we return satisfiable. If the 2SAT instance is not satisfiable, then we set all bits of lower order than ix to false and add 1 to the value at bit position ix in Z, and perform any associated carry operations. For partitioning the search space for the purpose of multithreading, we use the concept of chops, which is the number of highest-order bits being pre-set in order to partition the search space. If after a carry operation either the value of bit position n-1 goes from true to false, or for when evaluating a partition the highest-order bit position below the “chops” bits goes from true to false, we have reached the end of the search space for the entire problem or for the current partition of the entire problem, respectively, and we return not satisfiable for this space.

References

1. Cook, Stephen (1971). "The complexity of theorem proving procedures". Proceedings of the Third Annual ACM Symposium on Theory of Computing. pp. 151–158. doi:10.1145/800157.805047. ISBN 9781450374644. S2CID 7573663.
2. Fortnow, Lance (2009). "The status of the P versus NP problem" (PDF). Communications of the ACM. 52 (9): 78–86. CiteSeerX 10.1.1.156.767. doi:10.1145/1562164.1562186. S2CID 5969255. Archived from the original (PDF) on 24 February 2011. Retrieved 26 January 2010.
3. Karp, Richard M. (1972). "Reducibility Among Combinatorial Problems". In Raymond E. Miller; James W. Thatcher (eds.). Complexity of Computer Computations. New York: Plenum. pp. 85–103. ISBN 0-306-30707-3.