Abstract

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