March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver Export

@incollection{Heule05march, abstract = {This paper discusses several techniques to make the look- ahead architecture for satisfiability (Sat) solvers more competitive. Our contribution consists of reduction of the computational costs to perform look-ahead and a cheap integration of both equivalence reasoning and local learning. Most proposed techniques are illustrated with experimental results of their implementation in our solver march\_eq.}, author = {Heule, Marijn and Dufour, Mark and van Zwieten, Joris and van Maaren, Hans}, citeulike-article-id = {2360515}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/11527695_26}, doi = {10.1007/11527695_26}, journal = {Theory and Applications of Satisfiability Testing}, keywords = {ela, march, nnet}, pages = {345--359}, posted-at = {2009-10-30 14:49:54}, priority = {2}, title = {March\_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver}, url = {http://dx.doi.org/10.1007/11527695_26}, year = {2005} }

TY - CHAP ID - Heule05march L3 - citeulike-article-id:2360515 N2 - This paper discusses several techniques to make the look- ahead architecture for satisfiability (Sat) solvers more competitive. Our contribution consists of reduction of the computational costs to perform look-ahead and a cheap integration of both equivalence reasoning and local learning. Most proposed techniques are illustrated with experimental results of their implementation in our solver march_eq. JF - Theory and Applications of Satisfiability Testing EP - 359 TI - March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver SP - 345 KW - ela KW - march KW - nnet AU - Heule, Marijn AU - Dufour, Mark AU - van Zwieten, Joris AU - van Maaren, Hans PY - 2005/// UR - http://dx.doi.org/10.1007/11527695_26 ER -