Resolution versus Search: Two Strategies for SAT Export

@article{rish00resolution, abstract = {The paper compares two popular strategies for solving propositional satisfiability, 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 confirms theoretical prediction, showing that on low-w problems DR is very efficient, greatly outperforming the backtracking-based DavisPutnam -Logemann-Loveland procedure (DP). We also emphasize the...}, author = {Rish, Irina and Dechter, Rina}, citeulike-article-id = {553641}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.2820}, journal = {Journal of Automated Reasoning}, keywords = {knowledge\_compilation, logic, resolution, theorem\_proving}, number = {1/2}, pages = {225--275}, posted-at = {2006-03-16 01:35:25}, priority = {0}, title = {Resolution versus Search: Two Strategies for SAT}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.2820}, volume = {24}, year = {2000} }

TY - JOUR ID - rish00resolution L3 - citeulike-article-id:553641 N2 - The paper compares two popular strategies for solving propositional satisfiability, 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 confirms theoretical prediction, showing that on low-w problems DR is very efficient, greatly outperforming the backtracking-based DavisPutnam -Logemann-Loveland procedure (DP). We also emphasize the... IS - 1/2 JF - Journal of Automated Reasoning EP - 275 TI - Resolution versus Search: Two Strategies for SAT VL - 24 SP - 225 KW - knowledge_compilation KW - logic KW - resolution KW - theorem_proving AU - Rish, Irina AU - Dechter, Rina PY - 2000/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.2820 ER -