Research report 2015 - Max Planck Institute for Informatics
Solving the Unsolvable
Automation of Logic
Summary"Learning from Conflicts" is one of the most important strategies for solving computationally hard problems. By guessing a solution that respects local constraints either an overall solution is obtained or a conflict. A conflict can be efficiently turned into further constraints for the problem. "Learning from Conflicts" has pushed the performance of computer programs on hard problems to a new level. For example, automatic verification of computer hardware has turned from an academic discipline into an industry standard.