On good algorithms for determining unsatisfiability of propositional formulas Original Research Article

This paper is concerned with an algorithm that provides short certificates of unsatisfiability with high probability when an input I is a random instance of 3-SAT. Rather than build a refutation DAG, the algorithm finds bounds on nI(true), the number of variables that must be set to true, and nI(false), the number that must be set to false, if all clauses of I are to be satisfied. If the sum nI(true)+nI(false) is greater than the number of variables in I then I must be unsatisfiable. Bounds on nI(true) and nI(false) may be found by throwing out all clauses except those having only negative or only positive literals and finding nI+(true) for the remaining positive clause set I+ and nI−(false) for the remaining negative clause set I−. These questions can alternatively be stated as 3-hitting set problems on I+ and I− separately. It is shown that a good enough approximation algorithm for 3-hitting set can determine useful bounds on nI(true) and nI(false) (high probability of success for large enough constant ratio of clauses to variables). Although a good enough algorithm seems evasive, one that comes fairly close is proposed and analyzed.