Sciweavers

JAR
2000

Resolution versus Search: Two Strategies for SAT

13 years 9 months ago
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.
Irina Rish, Rina Dechter
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2000
Where JAR
Authors Irina Rish, Rina Dechter
Comments (0)