An On-Line Satisfiability Algorithm for Conjunctive Normal Form Expressions with Two Literals

May 2002

Proceedings of the Fifteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2002)

Volume

Proceedings of the Fifteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2002)

All Papers

This paper describes two algorithms for determining the satisfiability of Boolean conjunctive normal form expressions limited to two literals per clause (2-SAT) extending the classic effort of Aspvall, Plass, and Tarjan. The first algorithm differs from the original in that satisfiability is determined upon the presentation of each clause rather than the entire clause set. This on-line algorithm experimentally exhibits average run-time linear to the number of variables. This performance is achieved by performing a single depth first search of one of the incoming literals. Additional search is avoided by excluding clauses containing pure variables or variables whose truth value has been explicitly provided or can be inferred. An off-line algorithm is also described that incorporates these strategies