On 2-SAT and Renamable Horn

Alvaro del Val, Universidad Autónoma de Madrid

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.