[Mittagsseminar TI] Mittagsseminar am Di 11..12.2018

[Günter Rote <rote@inf.fu-berlin.de>]

Im Rahmen des Mittagsseminars der
Theoretischen Informatik der FU Berlin
spricht am

        Dienstag, 11.12.2018, 12:00 Uhr s.t., SR 055
        Marijn Heule (University of Texas, Austin)
        zum Thema: Solving very hard problems:
                   Cube-and-Conquer, a hybrid SAT solving method

Zusammenfassung:
Many search problems, from artificial intelligence to combinatorics, explore large search
spaces to determine the presence or absence of a certain object. These problems are hard
due to combinatorial explosion, and have traditionally been called infeasible. The
brute-force method, which at least implicitly explores all possibilities, is a general
approach to search systematically through such spaces. Brute force has long been regarded
as suitable only for simple problems. This has changed in the last two decades, due to the
progress in satisfiability (SAT) solving, which renders brute force into a powerful
approach to deal with many problems easily and automatically.

We illustrate the strength of SAT via the Boolean Pythagorean Triples problem, which has
been a long-standing open problem in Ramsey Theory. Our parallel SAT solver allowed us to
solve the problem on a cluster in about two days using 800 cores, demonstrating its linear
time speedup on many hard problems. Due to the general interest in this mathematical
problem, our result requires a formal proof. Exploiting recent progress in
unsatisfiability proof checking, we
produced and verified a clausal proof of the smallest counterexample, which is almost 200
terabytes in size. These techniques show great promise for attacking a variety of
challenging problems arising in mathematics and computer science.