On 2-SAT and Renamable Horn

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.

• Type: Conference
• Year: 2000
• Where: AAAI
• Authors: Alvaro del Val
• Keywords: AAAI 2000, Binary Propositional Theories, Intelligent Agents, Linear Time Algorithms, Renamable Horn Theories