Hard Combinatorial Problems: A Challenge for
              Satisfiability?

                                  Ilias S. Kotsireas1

                                     CARGO Lab
                              Wilfrid Laurier University
                               Waterloo, ON, Canada
                                  ikotsire@wlu.ca
                              http://www.cargo.wlu.ca




       Abstract. The theory and practice of satisfiability solvers has expe-
       rienced dramatic advances [1] in the past couple of decades. This fact
       attracted the attention of researchers that work with hard combinato-
       rial problems [2, 6, 9–11, 5] with the hope that if suitable and efficient
       SAT encodings of these problems can be constructed, then SAT solvers
       can be used to solve large instances of such problems effectively. On the
       other hand, researchers working in the area of SAT and SMT solvers
       observed that by combining the combinatorial search capabilities of SAT
       solvers with mathematical reasoning abilities of computer algebra sys-
       tems (CAS), one could attack combinatorial problems in a way that
       either of these approaches by themselves may not be able to [2]. Further,
       SAT researchers have been interested in hard combinatorial problems
       and produced significant breakthroughs [7, 8, 3, 4] using either custom-
       tailored highly-tuned SAT solvers implementations or by combining the
       SAT and CAS paradigms. In our own work, we are using SAT solvers
       to solve hard combinatorial problems, such as Williamson Hadamard
       matrices, D-optimal matrices, complex Golay pairs and so forth. These
       problems are defined via the fundamental concept of autocorrelation [12].
       It turns out that both these approaches (namely hand-tuned SAT solvers
       and SAT+CAS combinations) have had a number of successes already
       and it is safe to assume that a lot more successes are to be expected in
       the near future. Combinatorics is a vast source of very hard and chal-
       lenging problems, often containing thousands of discrete variables, and I
       firmly believe that the interaction between SAT researchers and combi-
       natorialists will continue to be very fruitful.

       Acknowledgement This is joint work with Vijay Ganesh at the Uni-
       versity of Waterloo.

       Keywords: SAT solvers · combinatorial conjectures · autocorrelation ·
       D-optimal designs · Hadamard matrices.

?
    Supported by an NSERC grant
2       Ilias S. Kotsireas

References
1. Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh. Handbook of Satis-
   fiability. Frontiers in Artificial Intelligence and Applications Volume 185, 2009.
2. Edward Zulkoski, Krzysztof Czarnecki, Vijay Ganesh. MathCheck: A Math Assis-
   tant via a Combination of Computer Algebra Systems and SAT Solvers. Interna-
   tional Conference on Automated Deduction CADE 2015, pp. 607-622, LNCS 9195,
   Springer, 2015.
3. Curtis Bright, Ilias Kotsireas, Vijay Ganesh. A SAT+CAS Method for Enumer-
   ating Williamson Matrices of Even Order. Thirty-second Conference on Artificial
   Intelligence AAAI 2018, AAAI Press, 2018.
4. Curtis Bright, Ilias Kotsireas, Albert Heinle, Vijay Ganesh. Enumeration of Com-
   plex Golay Pairs via Programmatic SAT. International Symposium on Symbolic
   and Algebraic Computation ISSAC 2018, pp. 111-118, ACM, 2018.
5. Erika Ábrahám, Building Bridges between Symbolic Computation and Satisfiability
   Checking, Invited Talk, ISSAC 2015, Bath, United Kingdom.
6. Srinivasan Arunachalam, Ilias Kotsireas. Hard satisfiable 3-SAT instances via auto-
   correlation. J. Satisf. Boolean Model. Comput. 10 (2016), pp. 11–22.
7. Marijn Heule. Avoiding triples in arithmetic progression. J. Comb. 8 (2017), no.
   3, pp. 391–422.
8. Marijn Heule, Oliver Kullmann, Victor W. Marek. Solving and verifying the Boolean
   Pythagorean triples problem via cube-and-conquer. Theory and applications of sat-
   isfiability testing, SAT 2016, pp. 228–245, LNCS 9710, Springer, Cham, 2016.
9. Edward Zulkoski, Curtis Bright, Albert Heinle, Ilias Kotsireas, Krzysztof Czarnecki,
   Vijay Ganesh. Combining SAT solvers with computer algebra systems to verify
   combinatorial conjectures. J. Automat. Reason. 58 (2017), no. 3, pp. 313–339.
10. Daniela Ritirc, Armin Biere, Manuel Kauers. Improving and extending the alge-
   braic approach for verifying gate-level multipliers. DATE 2018, pp. 1556–1561
11. Manuel Kauers, Martina Seidl. Symmetries of Quantified Boolean Formulas. SAT
   2018, pp. 199–216
12. I. S. Kotsireas. Algorithms and Meta-heuristics for Combinatorial Matrices. Hand-
   book of Combinatorial Optimization, 2nd Edition, 2013, P. M. Pardalos, D.-Z. Du,
   R. Graham (Editors) pp. 283–309