Resolution versus Search: Two Strategies for SAT

The paper compares two popular strategies for solving propositional satis ability, backtracking search and resolution, and analyzes the complexity of a directional resolution algorithm DR as a function of the width" w of the problem's graph. Our empirical evaluation con rms theoretical prediction, showing that on low-w problems DR is very e cient, greatly outperforming the backtracking-based DavisPutnam-Logemann-Loveland procedure DP. We also emphasize the knowledgecompilation properties of DR and extend it to a tree-clustering algorithm that facilitates query answering. Finally, we propose two hybrid algorithms that combine the advantages of both DR and DP. These algorithms use control parameters that bound the complexity of resolution and allow time space trade-o s that can be adjusted to the problem structure and to the user's computational resources. Empirical studies demonstrate the advantages of such hybrid schemes.

• Type: Journal
• Year: 2000
• Where: JAR
• Authors: Irina Rish, Rina Dechter
• Keywords: Algorithms, JAR 2000, Propositional Satis Ability, Resolution Algorithm Dr