On good algorithms for determining unsatisfiability of propositional formulas
This paper is concerned with an algorithm that provides short certificates of unsatisfiability with high probability when an input is a random instance of 3-SAT. Rather than build a refutation DAG, the algorithm finds bounds on , the number of variables that must be set to true, and , the number that must be set to false, if all clauses of are to be satisfied. If the sum is greater than the number of variables in then must be unsatisfiable. Bounds on and may be found by throwing out all clauses except those having only negative or only positive literals and finding for the remaining positive clause set and for the remaining negative clause set . These questions can alternatively be stated as 3-hitting set problems on and separately. It is shown that a good enough approximation algorithm for 3-hitting set can determine useful bounds on and (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.
satisfiability resolution theorem proving hitting set