Simplifying binary propositional theories into connected components twice as fast

Abstract

Binary propositional theories, composed of clauses with at most two literals, are one of the most interesting tractable subclasses of the satisfiability problem. We present two hybrid simplification algorithms for binary theories, which combine the unit-resolution-based 2SAT algorithm BinSat [9] with refined versions of the classical strongly connected components (SCC) algorithm of [1]. We show empirically that the algorithms are considerably faster than other SCC-based algorithms, and have greater simplifying power, as they combine detection of entailed literals with identification of SCCs, i.e. sets of equivalent literals. By developing faster simplification algorithms we hope to contribute to attempts to integrate simplification of binary theories within the search phase of general SAT solvers.