Abstract
We present a preprocessing algorithm for SAT, based on the HypBinRes inference rule, and show that it does not improve the performance of a DPLL-based SAT solver with conflict recording. We also present evidence that the ineffectiveness of the preprocessing algorithm is the result of interaction with the branching heuristic used by the solver. © Springer-Verlag 2004.
Cite
CITATION STYLE
APA
Drake, L., & Frisch, A. (2004). The interaction between inference and branching heuristics. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2919, 370–382. https://doi.org/10.1007/978-3-540-24605-3_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free