Many hard examples for resolution

Vasek Chvatal, E. Szemerédi

Research output: Contribution to journalArticle

274 Citations (Scopus)

Abstract

It is proved that 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. The proof makes use of random hypergraphs.

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

Fingerprint

Hypergraph
Tend
Integer
Family

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Computer Graphics and Computer-Aided Design
  • Hardware and Architecture
  • Information Systems
  • Software
  • Theoretical Computer Science

Cite this

Many hard examples for resolution. / Chvatal, Vasek; Szemerédi, E.

In: Journal of the ACM, Vol. 35, No. 4, 10.1988, p. 759-768.

Research output: Contribution to journalArticle

Chvatal, Vasek ; Szemerédi, E. / Many hard examples for resolution. In: Journal of the ACM. 1988 ; Vol. 35, No. 4. pp. 759-768.
@article{7451a56a16fd4d8fac85ae43ddcf9bbd,
title = "Many hard examples for resolution",
abstract = "It is proved that 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. The proof makes use of random hypergraphs.",
author = "Vasek Chvatal and E. Szemer{\'e}di",
year = "1988",
month = "10",
doi = "10.1145/48014.48016",
language = "English",
volume = "35",
pages = "759--768",
journal = "Journal of the ACM",
issn = "0004-5411",
publisher = "Association for Computing Machinery (ACM)",
number = "4",

}

TY - JOUR

T1 - Many hard examples for resolution

AU - Chvatal, Vasek

AU - Szemerédi, E.

PY - 1988/10

Y1 - 1988/10

N2 - It is proved that 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. The proof makes use of random hypergraphs.

AB - It is proved that 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. The proof makes use of random hypergraphs.

UR - http://www.scopus.com/inward/record.url?scp=0024090265&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0024090265&partnerID=8YFLogxK

U2 - 10.1145/48014.48016

DO - 10.1145/48014.48016

M3 - Article

AN - SCOPUS:0024090265

VL - 35

SP - 759

EP - 768

JO - Journal of the ACM

JF - Journal of the ACM

SN - 0004-5411

IS - 4

ER -