Let @math be a 3CNF formula with n variables and m clauses. A simple nonconstructive argument shows that when m is sufficiently large compared to n, most 3CNF formulas are not satisfiable. It is an open question whether there is an efficient refutation algorithm that for most such formulas proves that they are not satisfiable. A possible approach to refute a formula @math is: first, translate it into a graph @math using a generic reduction from 3-SAT to max-IS, then bound the maximum independent set of @math using the Lovasz @math function. If the @math function returns a value @math , this is a certificate for the unsatisfiability of @math . We show that for random formulas with @math clauses, the above approach fails, i.e. the @math function is likely to return a value of m.
@cite_5: For every choice of positive integers c and k such that k ≥ 3 and c 2 - k ≥ 0.7, there is a positive number e such that, with probability tending to 1 as n tends to ∞, a randomly chosen family of cn clauses of size k over n variables is unsatisfiable, but every resolution proof of its unsatisfiability must generate at least (1 + e) n clauses.
@cite_8: The width of a Resolution proof is defined to be the maximal number of literals in any clause of the proof. In this paper, we relate proof width to proof length (=size), in both general Resolution, and its tree-like variant. The following consequences of these relations reveal width as a crucial “resource” of Resolution proofs. In one direction, the relations allow us to give simple, unified proofs for almost all known exponential lower bounds on size of resolution proofs, as well as several interesting new ones. They all follow from width lower bounds, and we show how these follow from natural expansion property of clauses of the input tautology. In the other direction, the width-size relations naturally suggest a simple dynamic programming procedure for automated theorem proving—one which simply searches for small width proofs. This relation guarantees that the runnuing time (and thus the size of the produced proof) is at most quasi-polynomial in the smallest tree-like proof. This algorithm is never much worse than any of the recursive automated provers (such as DLL) used in practice. In contrast, we present a family of tautologies on which it is exponentially faster.
A possible approach for refuting a formula @math is to find a resolution proof for the unsatisfiability of @math . However, Chvatal and Szemeredi @cite_5 proved that a resolution proof of a random 3CNF formula with linear number of clauses is almost surely of exponential size. A result of a similar flavor for denser formulas was given by Ben-Sasson and Wigderson @cite_8 who showed that a random formula with @math clauses almost surely requires a resolution proof of size @math . These lower bounds imply that finding a resolution proof for a random formula is computationally inefficient.