Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method - Oliver Kullmann (26th International Joint Conference on Artificial Intelligence (IJCAI 2017), 2017)
A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem by the authors, yielding the largest (but "clever") proof yet. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, integrating the ``old'' and the ``new'' method of SAT solving.