Attacking Very Hard Problems via SAT
- 14:00 29th June 2017 ( week 10, Trinity Term 2017 )Room 051, Wolfson Building, Parks Road
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
Share this:
