Skip to main content

Attacking Very Hard Problems via SAT

Oliver Kullmann ( University of Swansea )

In my talk I will discuss "theory and practice" of attacking very hard *concrete* problems in the neighbourhood of NP, via SAT solving and other related tools, exploiting massive computations. Concerning problems to be solved, I will focus on problems from Ramsey theory. On the one hand a rich theory is available here, and, perhaps surprisingly, on the other hand the problems show some strong similarities to real-world problems. Concerning algorithms, I will outline the Cube-and-Conquer paradigm, a hybrid scheme for SAT solving. This will prompt the need for a "hybrid" complexity theory, employing oracles, and leveraging the advantages of trees *and* dags. A recent success story here was the solution of the Boolean Pythagorean Triples problem:

https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem 

http://cs.swan.ac.uk/~csoliver/papers.html#PYTHAGOREAN2016C

 

 

Share this: