Many Hard Examples for Resolution

Vašek Chvátal, Endre Szemerédi

Research output: Contribution to journalArticle

280 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)759-768
Number of pages10
JournalJournal of the ACM (JACM)
Issue number4
Publication statusPublished - Oct 1 1988


  • Resolution
  • satisfrability

ASJC Scopus subject areas

  • Software
  • Control and Systems Engineering
  • Information Systems
  • Hardware and Architecture
  • Artificial Intelligence

Cite this