The Interaction Between Inference and Branching Heuristics

Lyndon Drake; Alan M. Frisch

The Interaction Between Inference and Branching Heuristics

Computer Science

Research output: Contribution to conference › Paper

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.

Original language	Undefined/Unknown
Pages	370-382
Publication status	Published - 2003

Access to Document

Cite this

@conference{741afc2fa7054a0ea41ac00722ca5a0d,

title = "The Interaction Between Inference and Branching Heuristics",

abstract = "We present a preprocessing algorithm for SAT, based on theHypBinRes inference rule, and show that it does not improve the performanceof a DPLL-based SAT solver with conflict recording. We alsopresent evidence that the ineffectiveness of the preprocessing algorithm isthe result of interaction with the branching heuristic used by the solver.",

author = "Lyndon Drake and Frisch, {Alan M.}",

year = "2003",

language = "Undefined/Unknown",

pages = "370--382",

}

TY - CONF

T1 - The Interaction Between Inference and Branching Heuristics

AU - Drake, Lyndon

AU - Frisch, Alan M.

PY - 2003

Y1 - 2003

N2 - We present a preprocessing algorithm for SAT, based on theHypBinRes inference rule, and show that it does not improve the performanceof a DPLL-based SAT solver with conflict recording. We alsopresent evidence that the ineffectiveness of the preprocessing algorithm isthe result of interaction with the branching heuristic used by the solver.

AB - We present a preprocessing algorithm for SAT, based on theHypBinRes inference rule, and show that it does not improve the performanceof a DPLL-based SAT solver with conflict recording. We alsopresent evidence that the ineffectiveness of the preprocessing algorithm isthe result of interaction with the branching heuristic used by the solver.

M3 - Paper

SP - 370

EP - 382

ER -