You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Hard satisfiable 3-SAT instances via autocorrelation

Article type: Research Article

Authors: Arunachalam, Srinivasana; * | Kotsireas, Iliasb; **

Affiliations: [a] Centrum Wiskunde & Informatica, Amsterdam, The Netherlands. E-mail: arunacha@cwi.nl | [b] Wilfrid Laurier University, Waterloo, Ontario, Canada

Note: [*] Affiliated with Institute of Quantum Computing during most of this work and is grateful to Dr. Michele Mosca for support from NSERC.

Note: [**] Research supported by an NSERC grant. I am grateful to Dr. Michele Mosca for introducing me to the research of the first Author.

Keywords: SAT-solver, autocorrelation, D-optimal matrices

DOI: 10.3233/SAT190111

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 10, no. 1, pp. 11-22, 2016

Received 1 January 2016
|
Revision received 1 September 2016
|
Published: 1 December 2016
Get PDF open access

Abstract

We establish a reduction of a combinatorial problem defined via autocorrelation to an instance of Boolean satisfiability. As a consequence, we obtain a family of hard satisfiable 3-SAT instances. The combinatorial problem that we reduce is the D-optimal matrices problem. We generated a family of 3-SAT instances from the D-optimal matrices problem with the motivation to solve interesting cases using the power of SAT solvers. We give a detailed construction of the generated instances that were submitted to SAT competition 2014. Our reduction techniques is fairly straightforward and can be adapted to various other problems that are defined via autocorrelation.

Show more