The science of brute force

Abstract

Mathematics solves problems by pen and paper. CS helps us to go far beyond that.

References

1. Ahmed, T., Kullmann, O., Snevily, H. On the van der Waerden numbers w(2; 3, t). Disc. Appl. Math. 174 (2014), 27--51.
2. Biere, A., Fröhlich, A. Evaluating CDCL variable scoring schemes. In SAT (Springer, 2015), 405--422.
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), 1--6.
5. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y. Bounded model checking using satisfiability solving. Formal Methods in System Design 19, 1 (2001), 7--34.
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, 2001), 436--453.
8. Cruz-Filipe, L., Marques-Silva, J.P., Schneider-Kamp, P. Efficient certified resolution proof checking, 2016. https://arxiv.org/abs/1610.06984.
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, 2003), 10886--10891.
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, 2013), 181--188.
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, (2009), 155--184.
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), 185--203.
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 (2008), 53--61.
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), 190--217.
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 2012) 363--378.
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 (1930), 264--286.
34. Schur, I. Über die Kongruenz x^m + y^m = z^m (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.

Index Terms

• Hardware

  • Hardware validation

    • Functional verification

• Security and privacy

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • Formal language definitions