principle), but these statements are all
alien or extra-alien. Since these proofs
grow with m, the general statement
that all Ptn( 3; m) with m ³ 3 exist, is
then unprovable in principle.
Recent successes in brute reasoning,
such as solving the Erdős Discrepency
Problem and the Pythagorean Triples
Problem, show the potential of this
approach to deal with long-standing
open mathematical problems. Moreover, proofs for these problems can be
produced and verified completely automatically. These proofs may be big,
but we argued that compact elegant
proofs may not exist for some of these
problems, in particular (but not only)
for the exact bound results. The size
of these proofs does not influence the
level of correctness, and these proofs
may reveal interesting information
about the problem.
In contrast to popular belief,
mechanically produced huge proofs
can actually help in understanding the
given problem. We can try to understand their structure, and making them
thus smaller. Hardly any research has
been done yet in this direction apart
from removing redundancy in a given
proof. Possibilities are changing the
heuristics of a solver or introducing
new definitions of frequently occurring
patterns in the proof. Indeed, simply
validating a clausal proof does not only
produce a yes/no answer as to whether
the proof is correct, but also provides
an unsatisfiable core consisting of all
original clauses that were used to validate the proof—revealing important
parts of the problem. The size of the
core depends on the type of problem.
Problems in Ramsey Theory typically
have quite a large core and therefore
provide limited insight. Many bounded
model checking problems, however,
have small unsatisfiable cores, thereby
showing that large parts of the hardware design were not required to determine the safety property.
To conclude, it is definitely pos-
sible to gain insights by using SAT.
However that “insight” might need to
be reinterpreted here, and might work
on a higher level of abstraction. Every
paradigm change means asking differ-
ent questions. Gödel’s Incompleteness
Theorem solved partially the question
of the consistency of mathematics by
showing that the answer provably can-
not be delivered in the näive way. Now
the task is to live up to big complexi-
ties, and to embrace the new possibili-
ties. Proofs must become objects for
investigations, and understanding will
be raised to the next level, how to find
and handle them.
So, when the day finally comes
and the aliens arrive and ask us about
Ptn( 3; 3), we will tell them: “You know
what? Finding the answer yourself gives
you a much deeper understanding than
just telling you the answer—here you
have the SAT solving methodology,
that’s the real stuff!” And then humans
and aliens will live happily ever after.
Wir müssen wissen. Wir werden
(We must know. We will know.)
David Hilbert, 1930
1. Ahmed, T., Kullmann, O., Snevily, H. On the van der
Waerden numbers w( 2; 3, t). Disc. Appl. Math. 174
2. Biere, A., Fröhlich, A. Evaluating CDCL variable
scoring schemes. In SAT (Springer, 2015),
3. Biere, A., Heule, M. J.H., van Maaren, H., Walsh, T. eds.
Handbook of Satisfiability, volume 185 of FAIA.
IOS Press, Amsterdam, The Netherlands, Feb. 2009.
4. Buss, S. Propositional proofs in Frege and
Extended Frege systems (abstract). In Computer
Science— Theory and Applications (Springer, 2015),
5. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.
Bounded model checking using satisfiability
solving. Formal Methods in System Design 19, 1
6. Cook, S.A. The complexity of theorem-proving
procedures. In STOC (1971), 151–158.
7. Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G.,
Tacchella, A., Vardi, M. Y. Benefits of bounded model
checking at an industrial setting. In CAV (Springer,
8. Cruz-Filipe, L., Marques-Silva, J.P., Schneider-Kamp,
P. Efficient certified resolution proof checking, 2016.
9. de Moura, L., Bjørner, N. Satisfiability modulo theories:
Introduction and applications. Communications of the
ACM 54, 9 (2011), 69–77.
10. Eén, N., Sörensson, N. Temporal induction by
incremental SAT solving. Electr. Notes Theor. Comput.
Sci. 89, 4 (2003), 543–560.
11. Garey, M.R., Johnson, D.S. Computers and
Intractability; A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, 1979.
12. Goldberg, E. I., Novikov, Y. Verification of proofs of
unsatisfiability for CNF formulas. In DATE (IEEE,
13. Graham, R. L., Spencer, J. H. Ramsey theory. Scientific
American 263, 1 (July 1990), 112–117.
14. Heule, M. J. H., Hunt, W.A. Jr., Wetzler, N. Trimming
while checking clausal proofs. In FMCAD (IEEE,
15. Heule, M.J. H., Kullmann, O., Marek, V. W. Solving and
verifying the Boolean Pythagorean Triples problem via
Cube-and-Conquer. In SAT (Springer, 2016) 228–245.
16. Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.
Cube and conquer: Guiding CDCL SAT solvers by
lookaheads. In HVC (Springer, 2011), 50–65.
17. Heule, M. J. H., van Maaren, H. Look-ahead based
SAT solvers. In Biere et al. [ 3], Chapter 5,
18. Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar,
P. Efficient SAT-based bounded model checking
for software verification. Theoretical Computer
Science 404, 3 (2008), 256–274.
19. Karp, R.M. Reducibility among combinatorial
problems. In Complexity of Computer Computations
(Plenum Press, 1972), 85–103.
20. Kautz, H.A., Sabharwal, A., Selman, B. Incomplete
algorithms. In Biere et al. [ 3], Chapter 6, (2009),
21. Konev, B., Lisitsa, A. Computer-aided proof of Erdös
discrepancy properties. Artificial Intelligence 224, C
(July 2015), 103–118.
22. Kouril, M., Paul, J. L. The van der Waerden number
W( 2, 6) is 1132. Experimental Mathematics 17, 1
23. Kullmann, O. Fundaments of branching heuristics. In
Biere et al. [ 3], Chapter 7, (2009), 205–244.
24. Lam, C. W.H. The search for a finite projective plane of
order 10. The American Mathematical Monthly 98, 4
(April 1991), 305–318.
25. Lamb, E. Maths proof smashes size record:
Supercomputer produces a 200-terabyte proof—but is
it really mathematics? Nature 534 (June 2016), 17–18.
26. Landman, B.M., Robertson, A. Ramsey Theory on the
Integers, volume 24 of Student mathematical library.
American Mathematical Society, Providence, RI, 2003.
27. Lauria, M., Pudlák, P., Rödl, V., Thapen, N. The
complexity of proving that a graph is Ramsey. In
ICALP (Springer, 2013), 684–695.
28. Marques-Silva, J.P., Lynce, I., Malik, S. Conflict-driven
clause learning SAT solvers. In Biere et al. [ 3],
Chapter 4, (2009), 131–153.
29. McGuire, G., Tugemann, B., Civario, G. There
is no 16-clue Sudoku: Solving the Sudoku
minimum number of clues problem via hitting set
enumeration. Experimental Mathematics 23, 2 (2014),
30. Myers, K.J. Computational advances in Rado
numbers. PhD thesis, Rutgers University, New
Brunswick, NJ, 2015.
31. Oe, D., Stump, A., Oliver, C., Clancy, K. versat: A
verified modern SAT solver. In VMCAI (Springer,
32. Radziszowski, S.P. Small Ramsey numbers. The
Electronic Journal of Combinatorics (January 2014),
Dynamic Surveys DS1, Revision 14.
33. Ramsey, F.P. On a problem of formal logic.
Proceedings of the London Mathematical Society 30
34. Schur, I. Über die Kongruenz xm + ym = zm (mod p).
Jahresbericht der Deutschen Mathematiker-Vereinigung 25 (1917), 114–116.
35. Tao, T. The Erdös discrepancy problem. Discrete
Analysis 1 (February 2016), 29.
36. Voronkov, A. AVATAR: The architecture for first-order
theorem provers. In CAV (Springer, 2014) 696–710.
37. Wilson, R. Four Colors Suffice: How the Map Problem
Was Solved. Princeton University Press, Princeton,
NJ, revised edition, 2013.
Marijn J.H. Heule ( firstname.lastname@example.org) is a research
scientist at The University of Texas, Austin.
Oliver Kullmann ( email@example.com) is an
associate professor in computer science at Swansea
©2017 ACM 0001-0782/17/07 $15.00.
Watch the authors discuss
their work in this exclusive