=Paper=
{{Paper
|id=Vol-2189/paper15
|storemode=property
|title=Hard Combinatorial Problems: A Challenge for Satisfiability
|pdfUrl=https://ceur-ws.org/Vol-2189/paper15.pdf
|volume=Vol-2189
|authors=Ilias Kotsireas
|dblpUrl=https://dblp.org/rec/conf/scsquare/Kotsireas18
}}
==Hard Combinatorial Problems: A Challenge for Satisfiability==
https://ceur-ws.org/Vol-2189/paper15.pdf
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