A Polynomial-Time Algorithm for Satisfiability
Daniel J. Buehrer · International Journal of Engineering · 2016
In this paper we present an algorithm for calculating a rough set of rough models for a propositional Boolean formula. The rough set exists if and only if the formula is satisfiable. The rough set involves the leftmost minimal model and its corresponding dual rightmost maximal model. This rough set can be calculated in time O(m2l) where m is the number of OR arguments and l is the number of literals in the formula. Extended