Unit Propagation in a Tableau Framework

Unit propagation is one of the most important techniques of efficient SAT solvers. Unfortunately, this technique is not directly applicable to first-order clausal tableaux. We show a way of integrating a variant of unit propagation into the disconnection calculus and present some results obtained with an implementation of unit propagation in the DCTP theorem prover that show the usefulness of our new method.

• Type: Conference
• Year: 2005
• Where: TABLEAUX
• Authors: Gernot Stenz
• Keywords: Artificial Intelligence, Efficient Sat Solvers, TABLEAUX 2005, Unit Propagation, first-order Clausal Tableaux