Toward A Good Algorithm for Determining Unsatisfiability of Propositional Formulas,
John Franco, R. Swaminathan · 1997
We present progress toward an algorithm that provides short certificates of unsatisfiability with high probability when inputs are random instances of 3-SAT. Such an algorithm would incorporate an approximation algorithm A for the 3-Hitting Set problem. Using A it would determine an approximation for the minimum fraction of variables that must be set to true (false) in order to satisfy the positive (negative) clauses. If the fraction is high enough, then the instance is deemed unsatisfiable. Key words Satisfiability, Resolution, Theorem Proving, Hitting Set 1 Introduction It is well known that the problem of determining the existence of a satisfying truth assignment for a given propositional formula in Conjunctive Normal Form (CNF) is NP-complete. If clauses have exactly three literals each, the problem is called 3-SAT and this problem is also NP-complete. However, there exist polynomial time algorithms that, under certain circumstances, can produce a solution to a random satis...