Without Loss of Satisfaction

The success of automated reasoning presents us with an interesting peculiarity: while modern solving tools can handle gigantic real-world instances, they often fail miserably on supposedly easy problems. Their poor performance is frequently caused by using reasoning techniques that can only learn logically implied facts. In recent years, a couple of new proof systems have been proposed to overcome this issue by allowing to learn facts that are not logically implied, but preserve satisfaction. Moreover, these systems are surprisingly strong, even without the introduction of new definitions, which is a key feature of short proofs presented in the proof-complexity literature. We demonstrate the effectiveness of reasoning "without loss of satisfaction" using three problems that are hard for automated-reasoning approaches. First, we present short proofs of mutilated chessboard problems that are completely different than the classical argument. We can produce these proofs automatically and they are understandable. Second, our proofs of the chromatic number of Mycielski graphs show that these proof systems can compactly express arguments that go beyond symmetry breaking. Finally, we illustrate the impact on the proof size using Ramsey number problems. Resolution proofs of Ramsey number four consist of about a billion resolution steps. In contrast, our "without loss of satisfaction" proof uses just 38 steps. None of these proofs introduce new variables.