Zero-One Designs Produce Small Hard SAT Instances

Allen Van Gelder, Ivor Spence

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Citations (Scopus)

Abstract

Some basics of combinatorial block design are combined with certain constraint satisfaction problems of interest to the satisfiability community. The paper shows how such combinations lead to satisfiability problems, and shows empirically that these are some of the smallest very hard satisfiability problems ever constructed. Partially balanced (0,1) designs (PB01Ds) are introduced as an extension of balanced incomplete block designs (BIBDs) and (0,1) designs. Also, (0,1) difference sets are introduced as an extension of certain cyclical difference sets. Constructions based on (0,1) difference sets enable generation of PB01Ds over a much wider range of parameters than is possible for BIBDs. Building upon previous work of Spence, it is shown how PB01Ds lead to small, very hard, unsatisfiable formulas. A new three-dimensional form of combinatorial block design is introduced, and leads to small, very hard, satisfiable formulas. The methods are validated on solvers that performed well in the SAT 2009 and earlier competitions.
Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2010
Subtitle of host publication13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings
PublisherSpringer
Pages388-397
Number of pages10
Volume6175 LNCS
ISBN (Electronic)978-3-642-14186-7
ISBN (Print)978-3-642-14185-0
DOIs
Publication statusPublished - Jul 2010
EventTheory and Applications of Satisfiability Testing - Edinburgh, United Kingdom
Duration: 11 Jul 201014 Jul 2010

Conference

ConferenceTheory and Applications of Satisfiability Testing
CountryUnited Kingdom
CityEdinburgh
Period11/07/201014/07/2010

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'Zero-One Designs Produce Small Hard SAT Instances'. Together they form a unique fingerprint.

  • Cite this

    Van Gelder, A., & Spence, I. (2010). Zero-One Designs Produce Small Hard SAT Instances. In Theory and Applications of Satisfiability Testing – SAT 2010: 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Vol. 6175 LNCS, pp. 388-397). Springer. https://doi.org/10.1007/978-3-642-14186-7_37