The interaction between inference and branching heuristics

L Drake; A Frisch

The interaction between inference and branching heuristics

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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	English
Title of host publication	THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
Editors	E Giunchiglia, A Tacchella
Place of Publication	BERLIN
Publisher	Springer
Pages	370-382
Number of pages	13
ISBN (Print)	3-540-20851-8
Publication status	Published - 2004
Event	6th International Conference on Theory and Applications of Satisfiability Testing - Santa Margherita Ligure Duration: 5 May 2003 → 8 May 2003

Conference

Conference	6th International Conference on Theory and Applications of Satisfiability Testing
City	Santa Margherita Ligure
Period	5/05/03 → 8/05/03

Cite this

@inproceedings{ea5b21ee25eb4640ad3b05fd78d32d11,

title = "The interaction between inference and branching heuristics",

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.",

author = "L Drake and A Frisch",

year = "2004",

language = "English",

isbn = "3-540-20851-8",

pages = "370--382",

editor = "E Giunchiglia and A Tacchella",

booktitle = "THEORY AND APPLICATIONS OF SATISFIABILITY TESTING",

publisher = "Springer",

address = "Germany",

note = "6th International Conference on Theory and Applications of Satisfiability Testing ; Conference date: 05-05-2003 Through 08-05-2003",

}

TY - GEN

T1 - The interaction between inference and branching heuristics

AU - Drake, L

AU - Frisch, A

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

M3 - Conference contribution

SN - 3-540-20851-8

SP - 370

EP - 382

BT - THEORY AND APPLICATIONS OF SATISFIABILITY TESTING

A2 - Giunchiglia, E

A2 - Tacchella, A

PB - Springer

CY - BERLIN

T2 - 6th International Conference on Theory and Applications of Satisfiability Testing

Y2 - 5 May 2003 through 8 May 2003

ER -