A Decision-Making Procedure for Resolution-Based SAT-Solvers Export

@incollection{gsat08, abstract = {We describe a new decision-making procedure for resolution-based SAT-solvers called Decision Making with a Reference Point (DMRP). In DMRP, a complete assignment called a reference point is maintained. DMRP is aimed at finding a change of the reference point under which the number of clauses falsified by the modified point is smaller than for the original one. DMRP makes it possible for a DPLL-like algorithm to perform a ”local search strategy”. We describe a SAT-algorithm with conflict clause learning that uses DMRP. Experimental results show that even a straightforward and unoptimized implementation of this algorithm is competitive with SAT-solvers like BerkMin and Minisat on practical formulas. Interestingly, DMRP is beneficial not only for satisfiable but also for unsatisfiable formulas.}, author = {Goldberg, Eugene}, citeulike-article-id = {6083301}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-79719-7_11}, citeulike-linkout-1 = {http://www.springerlink.com/content/b32u58m468217415}, doi = {10.1007/978-3-540-79719-7_11}, journal = {Theory and Applications of Satisfiability Testing – SAT 2008}, keywords = {cdcl, hybrid, local-search, sat}, pages = {119--132}, posted-at = {2009-11-07 19:46:54}, priority = {2}, title = {A Decision-Making Procedure for Resolution-Based SAT-Solvers}, url = {http://dx.doi.org/10.1007/978-3-540-79719-7_11}, year = {2008} }

TY - CHAP ID - gsat08 L3 - citeulike-article-id:6083301 N2 - We describe a new decision-making procedure for resolution-based SAT-solvers called Decision Making with a Reference Point (DMRP). In DMRP, a complete assignment called a reference point is maintained. DMRP is aimed at finding a change of the reference point under which the number of clauses falsified by the modified point is smaller than for the original one. DMRP makes it possible for a DPLL-like algorithm to perform a ”local search strategy”. We describe a SAT-algorithm with conflict clause learning that uses DMRP. Experimental results show that even a straightforward and unoptimized implementation of this algorithm is competitive with SAT-solvers like BerkMin and Minisat on practical formulas. Interestingly, DMRP is beneficial not only for satisfiable but also for unsatisfiable formulas. JF - Theory and Applications of Satisfiability Testing – SAT 2008 EP - 132 TI - A Decision-Making Procedure for Resolution-Based SAT-Solvers SP - 119 KW - cdcl KW - hybrid KW - local-search KW - sat AU - Goldberg, Eugene PY - 2008/// UR - http://dx.doi.org/10.1007/978-3-540-79719-7_11 ER -