Learning to Select Branching Rules in the DPLL Procedure for Satisfiability Export

@article{citeulike:6086764, abstract = {The DPLL procedure is the most popular complete satisfiability (SAT) solver. While its worst case complexity is exponential, the actual running time is greatly affected by the ordering of branch variables during the search. Several branching rules have been proposed, but none is the best in all cases. This work investigates the use of automated methods for choosing the most appropriate branching rule at each node in the search tree. We consider a reinforcement-learning approach where a value function, which predicts the performance of each branching rule in each case, is learned through trial runs on a typical problem set of the target class of SAT problems. Our results indicate that, provided sufficient training on a given class, the resulting strategy performs as well as (and, in some cases, better than) the best branching rule for that class. Research supported in part by NSF grant IRI-9702576. The first author was also partially supported by the Lilian-Voudouri Foundation in Greece. The authors gratefully acknowledge the influence of Don Loveland, Ron Parr, and Henry Kautz in helping to shape this work.}, author = {Lagoudakis, Michail and Littman, Michael}, citeulike-article-id = {6086764}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/S1571-0653(04)00332-4}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S1571065304003324}, doi = {10.1016/S1571-0653(04)00332-4}, issn = {15710653}, journal = {Electronic Notes in Discrete Mathematics}, keywords = {algorithm\_selection, reinforcement\_learning, satisfiability}, month = {June}, pages = {344--359}, posted-at = {2009-11-09 00:11:45}, priority = {2}, title = {{Learning to Select Branching Rules in the DPLL Procedure for Satisfiability}}, url = {http://dx.doi.org/10.1016/S1571-0653(04)00332-4}, volume = {9}, year = {2001} }

TY - JOUR ID - citeulike:6086764 L3 - citeulike-article-id:6086764 N2 - The DPLL procedure is the most popular complete satisfiability (SAT) solver. While its worst case complexity is exponential, the actual running time is greatly affected by the ordering of branch variables during the search. Several branching rules have been proposed, but none is the best in all cases. This work investigates the use of automated methods for choosing the most appropriate branching rule at each node in the search tree. We consider a reinforcement-learning approach where a value function, which predicts the performance of each branching rule in each case, is learned through trial runs on a typical problem set of the target class of SAT problems. Our results indicate that, provided sufficient training on a given class, the resulting strategy performs as well as (and, in some cases, better than) the best branching rule for that class. Research supported in part by NSF grant IRI-9702576. The first author was also partially supported by the Lilian-Voudouri Foundation in Greece. The authors gratefully acknowledge the influence of Don Loveland, Ron Parr, and Henry Kautz in helping to shape this work. JF - Electronic Notes in Discrete Mathematics SN - 15710653 EP - 359 TI - {Learning to Select Branching Rules in the DPLL Procedure for Satisfiability} VL - 9 SP - 344 KW - algorithm_selection KW - reinforcement_learning KW - satisfiability AU - Lagoudakis, Michail AU - Littman, Michael PY - 2001/06// UR - http://dx.doi.org/10.1016/S1571-0653(04)00332-4 ER -