On 2-SAT and Renamable Horn

Abstract

We introduce new linear time algorithms for satisfiability of binary propositional theories (2-SAT), and for recognition and satisfiability of renamable Horn theories. The algorithms are based on unit resolution, and are thus likely easier to integrate within general SAT solvers than other graph-based algorithms. Introduction 2-SAT and renamable Horn SAT are the paradigmatic examples of tractable problems in propositional satisfiability, itself the paradigmatic example of NP-complete problem. 2-SAT is the problem of deciding the satisfiability of a set of binary clauses; renamable Horn SAT, or RenHorn-SAT for short, the problem of deciding the satisfiability of a set of clauses which is renamable Horn, i.e. which can be transformed into a set of Horn clauses by an uniform renaming of variables. We present linear time algorithms for satisfiability of binary theories, and for recognition and satisfiability of renamable Horn. For such two classic problems, the conceptual baggage, ...