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


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.