sgen1: A generator of small but difficult satisfiability benchmarks

Research output: Contribution to journalArticlepeer-review

15 Citations (Scopus)
3 Downloads (Pure)


The satisfiability problem is known to be NP-Complete; therefore, there should be relatively small problem instances that take a very long time to solve. However, most of the smaller benchmarks that were once thought challenging, especially the satisfiable ones, can be processed quickly by modern SAT-solvers. We describe and make available a generator that produces both unsatisfiable and, more significantly, satisfiable formulae that take longer to solve than any others known. At the two most recent international SAT Competitions, the smallest unsolved benchmarks were created by this generator. We analyze the results of all solvers in the most recent competition when applied to these benchmarks and also present our own more focused experiments.
Original languageEnglish
Article number1.2
Pages (from-to)1.2:1-1.2:15
Number of pages15
JournalACM Journal of Experimental Algorithmics
Issue numbernull
Publication statusPublished - 01 Jan 2010

ASJC Scopus subject areas

  • Theoretical Computer Science


Dive into the research topics of 'sgen1: A generator of small but difficult satisfiability benchmarks'. Together they form a unique fingerprint.

Cite this