Detecting Boolean Functions for Proving Unsatisfiability
Richard Ostrowski, Lionel Paris · 2009
In 1997, B. Selman andH. Kautz proposed a series of 10 challenges. One of them concerned the design of a practical stochastic local search procedure for proving unsatisfiability (Challenge 5). Today, more than 10 years later, only few attempts were led to address this challenge, in spite of the great number of incomplete methods for proving satisfiability. In this paper, we propose a two steps algorithm for proving unsatisfiability of CNF formulas. The first step consists in detecting ¿-gates greedily. At the same time, a polynomial algorithm is used to eventually prove the unsatisfiability of the extracted set of ¿-gates. We show that this method outperforms the existing ones on some classes of instances. This method is then extended to other logical functions (¿-gates & ¿-gates).