title:
Complexity of Propositional Proofs under a Promise

Abstract:
We study the problem of certifying the unsatisfiability of CNF formulas under
the promise that if a CNF is satisfiable then it has many satisfying
assignments, within the framework of propositional proof complexity (the term
`many' stands for an explicitly specified function \Lambda in the number of
variables n). For this purpose we develop propositional proof systems under
different measures of promises (that is, different \Lambda) as extensions of
Resolution. This is done by augmenting Resolution with axioms that, roughly,
can eliminate sets of truth assignments defined by Boolean circuits. We then
investigate the complexity of such systems, obtaining an exponential separation
in the average-case between Resolution under different size of promises:
(i) Resolution has polynomial-size refutations for all unsatisfiable 3CNF
    formulas when the promise is (\epsilon 2^n), for any constant 0<\epsilon<1;
(ii) There are no sub-exponential size Resolution refutations for random 3CNF
    formulas, when the promise is 2^{\delta n} (and the number of clauses is
   o(n^{3/2})), for any constant 0<\delta<1.

Joint work with Nachum Dershowitz