On 2-SAT and Renamable Horn

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

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.