Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. (English) Zbl 1403.68226
Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40969-6/pbk; 978-3-319-40970-2/ebook). Lecture Notes in Computer Science 9710, 228-245 (2016).
Summary: The Boolean Pythagorean triples problem has been a longstanding open problem in Ramsey theory: can the set \(\mathbb {N}= \{1,2,\dots \}\) of natural numbers be divided into two parts, such that no part contains a triple \((a,b,c)\) with \(a^2 + b^2 = c^2\)? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the cube-and-conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.
For the entire collection see [Zbl 1337.68009].
For the entire collection see [Zbl 1337.68009].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 05D10 | Ramsey theory |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
Software:
Flyspeck; tawSolver; PicoSAT; DRABT; Treengeling; Plingeling; Lingeling; MiniSat; DRAT-trim; kcnfsOnline Encyclopedia of Integer Sequences:
The 2-color Rado numbers for x_1^2 + x_2^2 + ... + x_n^2 = z^2.Number of 2-colorings of [1..n] with no monochromatic Pythagorean triple.
References:
| [1] | Mizar proof checker. Accessed: November 2015 |
| [2] | Coq proof manager. Accessed: November 2015 |
| [3] | The site of \[ flyspeck \] project, the formal verification of the proof of Kepler Conjecture. Accessed: November 2015 |
| [4] | Ahmed, T., Kullmann, O., Snevily, H.: On the van der Waerden numbers w(2; 3, t). Discrete Appl. Math. 174, 27–51 (2014) · Zbl 1298.05313 · doi:10.1016/j.dam.2014.05.007 |
| [5] | Biere, A.: Picosat essentials. JSAT 4(2–4), 75–97 (2008) · Zbl 1159.68403 |
| [6] | Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013, p. 51 (2013) |
| [7] | Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009) · Zbl 1183.68568 |
| [8] | Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999) |
| [9] | Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pp. 151–158 (1971) · doi:10.1145/800157.805047 |
| [10] | Cooper, J., Overstreet, R.: Coloring so that no Pythagorean triple is monochromatic (2015). arXiv:1505.02222 |
| [11] | Cooper, J., Poirel, C.: Note on the Pythagorean triple system (2008) |
| [12] | Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of 5th International Conference on Knowledge Representation and Reasoning, KR 1996, pp. 148–159. Morgan Kaufmann (1996) |
| [13] | Dequen, G., Dubois, O.: kcnfs: an efficient solver for random k-SAT formulae. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 486–501. Springer, Heidelberg (2004) · Zbl 1204.68189 · doi:10.1007/978-3-540-24605-3_36 |
| [14] | Dransfield, M.R., Marek, V.W., Truszczyński, M.: Satisfiability and computing van der Waerden numbers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 1–13. Springer, Heidelberg (2004) · Zbl 1204.05097 · doi:10.1007/978-3-540-24605-3_1 |
| [15] | Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In: International Joint Conferences on Artificial Intelligence (IJCAI), pp. 248–253 (2001) |
| [16] | Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005) · Zbl 1128.68463 · doi:10.1007/11499107_5 |
| [17] | Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37 |
| [18] | Franco, J., Martin, J.: A history of satisfiability. In: Biere et al. [7], Chap. 1, pp. 3–74 |
| [19] | Garey, M.R., Johnson, D.S.: Computers and Intractability/A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, New York (1979) · Zbl 0411.68039 |
| [20] | Henschen, L.J., Wos, L.: Unit refutations and Horn sets. J. Assoc. Comput. Mach. 21(4), 590–605 (1974) · Zbl 0296.68093 · doi:10.1145/321850.321857 |
| [21] | Heule, M.J.H., Biere, A.: Clausal proof compression. In: 11th International Workshop on the Implementation of Logics (2015) |
| [22] | Heule, M.J.H., Biere, A.: Compositional propositional proofs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 444–459. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-48899-7_31 · Zbl 1471.68310 · doi:10.1007/978-3-662-48899-7_31 |
| [23] | Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 345–359. Springer, Heidelberg (2013) · Zbl 1381.68270 · doi:10.1007/978-3-642-38574-2_24 |
| [24] | Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 591–606. Springer, Heidelberg (2015) · Zbl 1465.68285 · doi:10.1007/978-3-319-21401-6_40 |
| [25] | Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012) · doi:10.1007/978-3-642-34188-5_8 |
| [26] | Heule, M.J.H., van Maaren, H.: Look-ahead based SAT solvers. In: Biere et al. [7], Chap. 5, pp. 155–184 |
| [27] | Järvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010) · Zbl 1284.03208 · doi:10.1007/978-3-642-12002-2_10 |
| [28] | Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355–370. Springer, Heidelberg (2012) · Zbl 1358.68256 · doi:10.1007/978-3-642-31365-3_28 |
| [29] | Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatche, J.W. (eds.) Complexity of Computer Computations, pp. 85–103. Plenum Press, New York (1972) · doi:10.1007/978-1-4684-2001-2_9 |
| [30] | Kay, W.: An overview of the constructive local lemma. Master’s thesis, University of South Carolina (2009) |
| [31] | Kouril, M.: Computing the van der Waerden number \[ {W}(3,4) = 293 \] . INTEGERS: Electron. J. Comb. Number Theory 12(A46), 1–13 (2012) · Zbl 1283.05261 |
| [32] | Kouril, M., Paul, J.L.: The van der Waerden number \[ {W}(2,6) \] is \[ 1132 \] . Exp. Math. 17(1), 53–61 (2008) · Zbl 1151.05048 · doi:10.1080/10586458.2008.10129025 |
| [33] | Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96–97, 149–176 (1999) · Zbl 0941.68126 · doi:10.1016/S0166-218X(99)00037-2 |
| [34] | Kullmann, O.: Fundaments of branching heuristics. In: Biere et al. [7], Chap. 7, pp. 205–244 |
| [35] | Levin, L.: Universal search problems. Problemy Peredachi Informatsii 9, 115–116 (1973) · Zbl 0313.02026 |
| [36] | Li, C.M.: A constraint-based approach to narrow search trees for satisfiability. Inf. Process. Lett. 71(2), 75–80 (1999) · Zbl 1015.68518 · doi:10.1016/S0020-0190(99)00088-5 |
| [37] | Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), pp. 366–371. Morgan Kaufmann Publishers (1997) |
| [38] | Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Proceedings of Haifa Verification Conference 2012 (2012) |
| [39] | Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et al. [7], Chap. 4, pp. 131–153 |
| [40] | Mijnders, S., de Wilde, B., Heule, M.J.H.: Symbiosis of search and heuristics for random 3-SAT. In: Mitchell, D., Ternovska, E. (eds.) Third International Workshop on Logic and Search (LaSh 2010) (2010) |
| [41] | Myers, K.J.: Computational advances in Rado numbers. Ph.D. thesis, Rutgers University (2015) |
| [42] | Rado, R.: Some partition theorems. In: Colloquia Mathematica Societatis János Bolyai 4. Combinatorial Theory and Its Applications III, pp. 929–936. North-Holland, Amsterdam (1970) |
| [43] | Schur, I.: Über die Kongruenz \[ x^m + y^m = z^m \] (mod p). Jahresbericht der Deutschen Mathematikervereinigung 25, 114–117 (1917) · JFM 46.0193.02 |
| [44] | Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning 2, pp. 466–483. Springer, Heidelberg (1983) · doi:10.1007/978-3-642-81955-1_28 |
| [45] | van der Waerden, B.L.: Beweis einer Baudetschen Vermutung. Nieuw Archief voor Wiskunde 15, 212–216 (1927) · JFM 53.0073.12 |
| [46] | Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008) |
| [47] | Voevodski, V.: Lecture at ASC 2008, How I became interested in foundations of mathematics. Accessed: November 2015 |
| [48] | Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Heidelberg (2014) · Zbl 1423.68475 · doi:10.1007/978-3-319-09284-3_31 |
| [49] | Zhang, H.: Combinatorial designs by SAT solvers. In: Biere et al. [7], Chap. 17, pp. 533–568 |
| [50] | Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880–10885 (2003) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
