For every choice of positive integers c and k such that k ≥ 3 and c2-k ≥ 0.7, there is a positive number ε 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 + ε)n clauses.
ASJC Scopus subject areas
- Control and Systems Engineering
- Information Systems
- Hardware and Architecture
- Artificial Intelligence