Hard satisfiable 3-SAT instances via autocorrelation

Srinivasan Arunachalam, Ilias Kotsireas


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.


AT-solver, autocorrelation, D-optimal matrices

Full Text:



Amir Aavani, David G. Mitchell, and Eugenia Ternovska. New encoding for translating pseudo-boolean constraints into SAT. In Proceedings of the Tenth Symposium on Abstraction, Reformulation, and Approximation, SARA 2013, 11-12 July 2013, Leavenworth, Washington, USA., 2013.

Srinivasan Arunachalam and Ilias Kotsireas, 2014. Satisfiability through auto correlation, in SAT competition.

Srinivasan Arunachalam and Ilias Kotsireas, 2014. Satisfiability through autocorrelation. https://sites.google.com/site/autocorthroughsat/home.

Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of boolean cardinality constraints. In Principles and Practice of Constraint rogramming - CP 2003, 9th International Conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, pages 108–122, 2003.

Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.

Richard P. Brent and Judy-anne H. Osborn. General lower bounds on maximal determinants of binary matrices. Electr. J. Comb., 20(2):P15, 2013.

SAT Conference. Sat Competition. http://www.satcompetition.org/.

Stephen A. Cook and David G. Mitchell. Finding hard instances of the satisfiability problem: A survey. In Satisfiability Problem: Theory and Applications, Proceedings of a DIMACS Workshop, Piscataway, New Jersey, USA, March 11-13, 1996, pages 1–18, 1996. Edited by: Dingzhu Du, Jun Gu, Panos M. Pardalos.

Dragomir Z. Djokovic and Ilias S. Kotsireas. New results on D-optimal matrices. J. Combin. Des., 20(6):278–289, 2012.

Dragomir Z. Djokovic and Ilias S. Kotsireas. Compression of periodic complementary sequences and applications. Des. Codes Cryptogr., 74(2):365–377, 2015.

Niklas E ́en and Niklas S'orensson. Translating pseudo-boolean constraints into SAT. JSAT, 2(1-4):1–26, 2006.

Ilias S. Kotsireas and Panos M. Pardalos. D-optimal matrices via quadratic integer optimization. J. Heuristics, 19(4):617–627, 2013.

Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, pages 827–831, 2005.

G. S. Tseitin. On the complexity of derivation in propositional calculus. In Automation of Reasoning, pages 466–483. Springer, 1983.


  • There are currently no refbacks.