Combining SAT Solvers with CAS to Verify Combinatorial Conjectures (2016)
Aloul, F.A. Markov, I.L. Sakallah, K.A.: Shatter: efficient symmetry-breaking for boolean satisfiability. In: Proceedings of the 40th Annual Design Automation Conference, pp. 836–839. ACM, (2003)
Areces, C., Déharbe, D., Pascal, F., Ezequiel, O.: SyMT: finding symmetries in SMT formulas. In: SMT Workshop 2013 11th International Workshop on Satisfiability Modulo Theories, (2013)
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. IJCAI 9, 399–404 (2009)
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A.: CVC4. In: Gopalakrishnan, Ganesh, Qadeer, Shaz (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 6806, pp. 171–177. Springer, Berlin (2011)
Bayless, S., Bayless, N., Hoos, H.H., Hu, A.J.: SAT modulo monotonic theories. In: Twenty-Ninth AAAI Conference on Artificial Intelligence, (2015)
Benhamou, B., Nabhani, T., Ostrowski, R., Saïdi, M.R.: Enhancing clause learning by symmetry in SAT solvers. In: 22nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2010, vol. 1, pp. 329–335. IEEE, (2010)
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of satisfiability, volume 185 of frontiers in artificial intelligence and applications. IOS Press, (2009)
Bosma, W., Cannon, J., Playoust, C.: The magma algebra system I: the user language. J. Symb. Comput. 24(3), 235–265 (1997)
Bouton, T., de Oliveira, D.C.B., Déharbe, D.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) Automated Deduction: CADE-22. LNCS, vol. 5663, pp. 151–156. Springer, Berlin (2009)
Bright, C., Ganesh, V., Heinle, A., Kotsireas, l., Nejati, S., Czarnecki, K.: MathCheck2: A SAT+CAS verifier for combinatorial conjectures. In: Computer Algebra in Scientific Computing (to appear). Springer, Berlin (2016)
Char, B.W., Fee, G.J., Geddes, K.O., Gonnet, G.H., Monagan, Michael B.: A tutorial introduction to Maple. J. Symb. Comput. 2(2), 179–200 (1986)
Chen, Y.-C., Li, K.-L.: Matchings extend to perfect matchings on hypercube networks. In: Proceedings of the International Multiconference of Engineers and Computer Scientists, vol. 1. Citeseer, (2010)
Colbourn, C.J., Dinitz, J.H. (eds.): Handbook of Combinatorial Designs. Discrete Mathematics and its Applications (Boca Raton), 2nd edn. Chapman & Hall/CRC, Boca Raton (2007)
Darga, P.T., Sakallah, K.A., Markov, I.L.: Faster symmetry discovery using sparsity of symmetries. In: Proceedings of the 45th Annual Design Automation Conference, pp. 149–154. ACM, (2008)
De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340. Springer, Berlin (2008)
Déharbe, D., Fontaine, P., Merz, S., Paleo, B.W.: Exploiting symmetry in SMT problems. In: Automated deduction–CADE-23, pp. 222–236. Springer, Berlin (2011)
Devos, S., Norine, M.: Edge-antipodal colorings of cubes. Open Problems Garden (2008)
Dooms, G., Deville, Y., Dupont, P.: CP(Graph): introducing a graph computation domain in constraint programming. In: Principles and Practice of Constraint Programming-CP 2005, pp. 211–225. Springer, Berlin (2005)
Downey, R.G., Fellows, M.R.: Fundamentals of parameterized complexity, vol. 4. Springer, London (2013)
Een, N., Sörensson, N.: MiniSat: a SAT solver with conflict-clause minimization. Sat, 5:8th, (2005)
Feder, T.: Subi, Carlos: On hypercube labellings and antipodal monochromatic paths. Discrete Appl. Math. 161(10), 1421–1426 (2013)
Fink, J.: Perfect matchings extend to Hamilton cycles in hypercubes. J. Comb. Theory Ser. B 97(6), 1074–1076 (2007)
Fink, J.: Connectivity of matching graph of hypercube. SIAM J. Discrete Math. 23(2), 1100–1109 (2009)
Frigo, M., Johnson, S.G.: The design and implementation of FFTW3. In: Proceedings of the IEEE, 93(2):216–231, (2005). Special issue on “Program Generation, Optimization, and Platform Adaptation”
Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer Aided Verification, pp. 519–531. Springer, Berlin (2007)
Ganesh, V., O’donnell, C.W., Soos, M., Devadas, S., Rinard, M.C., Solar-Lezama, A.: Lynx: A programmatic SAT solver for the RNA-folding problem. In: Theory and Applications of Satisfiability Testing–SAT 2012, pp. 143–156. Springer, (2012)
Gebser, M., Janhunen, T., Rintanen, J.: SAT modulo graphs: Acyclicity. In: Logics in Artificial Intelligence, pp. 137–151. Springer, (2014)
Gent, I.P., Petrie, K.E., Puget, J.F.: Symmetry in constraint programming. Handbook of constraint programming, pp. 329–376, (2006)
Gent, I., Smith, P.: Symmetry breaking during search in constraint programming. Citeseer, Barbara (1999)
Gregor, P.: Perfect matchings extending on subcubes to Hamiltonian cycles of hypercubes. Discrete Math. 309(6), 1711–1713 (2009)
Hadamard, J.: Résolution d’une question relative aux déterminants. Bull. Sci. Math. 17(1), 240–246 (1893)
Hedayat, A., Wallis, W.D.: Hadamard matrices and their applications. Ann. Stat. 6(6), 1184–1238 (1978)
Heule, M.J.H., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Formal methods in computer-aided design (FMCAD), 2013, pp. 181–188. IEEE, (2013)
Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. arXiv preprint arXiv:1605.00723, (2016)
Holm, J., de Lichtenberg, K., Thorup, M.: Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity. J. ACM 48(4), 723–760 (2001)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)
Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Applegate, D., Brodal, G.S., Panario, D., Sedgewick, R (eds) Proceedings of the Ninth Workshop on Algorithm Engineering and Experiments and the Fourth Workshop on Analytic Algorithms and Combinatorics, pp. 135–149. SIAM, (2007)
Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: SAT, (2014)
Kotsireas, I.S.: Algorithms and Metaheuristics for Combinatorial Matrices. In: Handbook of Combinatorial Optimization, pp. 283–309. Springer, New York, (2013)
Kotsireas, I.S., Koukouvinos, C., Seberry, J.: Hadamard ideals and Hadamard matrices with two circulant core. Eur. J. Comb. 27(5), 658–668 (2006)
Koukouvinos, C., Kounias, S.: Hadamard matrices of the Williamson type of order (4cdot m), (m=pcdot q) an exhaustive search for (m=33). Discrete Math 68(1), 45–57 (1988)
Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential recency weighted average branching heuristic for SAT solvers. In: Schuurmans, D., Wellman, M.P. (eds), Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12–17, 2016, Phoenix, Arizona, USA., pp. 3434–3440. AAAI Press, (2016)
Lifschitz, V.: What is answer set programming? AAAI 8, 1594–1597 (2008)
Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Vol. 1, pp. 609–619, (2015)
Muller, D.E.: Application of Boolean algebra to switching circuit design and to error detection. Electronic Computers, Transactions of the IRE Professional Group on Electronic Computers, EC-3(3):6–12, (1954)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader F., Voronkov A. (eds.) LPAR, volume 3452 of Lecture Notes in Computer Science, pp. 36–50. Springer, (2004)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science & Business Media, (2002)
Doković, D.Z.: Williamson matrices of order 4n for n = 33, 35, 39. Discrete Math. 115(1), 267–271 (1993)
Doković, D.Z., Kotsireas, I.S.: Compression of periodic complementary sequences and applications. Des. Codes Cryptogr. 74(2), 365–377 (2015)
Paley, R.E.A.C.: On orthogonal matrices. J. Math. Phys. 12(1), 311–320 (1933)
Reed, I.: A class of multiple-error-correcting codes and the decoding scheme. Trans. IRE Prof. Group Inf. Theory 4(4), 38–49 (1954)
Ruskey, F., Savage, C.: Hamilton cycles that extend transposition matchings in Cayley graphs of ({S}_n). SIAM J. Discrete Math. 6(1), 152–166 (1993)
Sakallah, K.A.: Symmetry and satisfiability. Handb. Satisf. 185, 289–338 (2009)
Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3, 141–224 (2007)
Seberry, J.: Library of Williamson Matrices. http://www.uow.edu.au/~jennie/WILLIAMSON/williamson.html
Sloane, N.: Library of Hadamard Matrices. http://neilsloane.com/hadamard/
Soh, T., Le Berre, D., Roussel, S., Banbara, M., Tamura, N.: Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem. In Logics in Artificial Intelligence, pp. 684–693. Springer, (2014)
Stein, W.A., et al.: Sage Mathematics Software (Version 6.3), (2010)
Sylvester, J.J.: Thoughts on inverse orthogonal matrices, simultaneous sign successions, and tessellated pavements in two or more colours, with applications to Newton’s rule, ornamental tile-work, and the theory of numbers. Lond. Edinb. Dublin Philos. Magaz. J. Sci. 34(232), 461–475 (1867)
The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0
Thurley, M.: sharpSAT–counting models with advanced component caching and implicit BCP. In Theory and Applications of Satisfiability Testing–SAT 2006, pp. 424–429. Springer, (2006)
Torlak, E.: A constraint solver for software engineering: finding models and cores of large relational specifications. PhD thesis, Massachusetts Institute of Technology, (2009)
Velev, M.N., Gao, P.: Efficient SAT techniques for absolute encoding of permutation problems: Application to Hamiltonian cycles. In SARA, (2009)
Walsh, J.L.: A closed set of normal orthogonal functions. Am. J. Math. 45(1), 5–24 (1923)
Stéfan van der Walt, S., Colbert, C., Varoquaux, G.: The NumPy array: a structure for efficient numerical computation. Comput. Sci. Eng. 13(2), 22–30 (2011)
Wetzler, N., Heule, M.J.H., Hunt Jr, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In International Conference on Theory and Applications of Satisfiability Testing, pp. 422–429. Springer, (2014)
Williamson, J.: Hadamard’s determinant theorem and the sum of four squares. Duke Math. J 11(1), 65–81 (1944)
Wolfram, S.: The Mathematica Book, version 4. Cambridge University Press, Cambridge (1999)
Zulkoski, E., Ganesh, V.: SageSAT, (2015) https://bitbucket.org/ezulkosk/sagesat
Zulkoski, E., Ganesh, V., Czarnecki, K.: MathCheck: A math assistant based on a combination of computer algebra systems and SAT solvers. In International Conference on Automated Deduction, Berlin, Germany, 08/2015. Springer, Berlin (2015)
Source: link.springer.com…
