On the power of top-down branching heuristics

Reference:

Matti Järvisalo and Tommi Junttila. On the power of top-down branching heuristics. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI-08), pages 304–309. AAAI Press, 2008.

Abstract:

We study the relative best-case performance of DPLL-based structure-aware SAT solvers in terms of the power of the underlying proof systems. The systems result from (i) varying the style of branching and (ii) enforcing dynamic restrictions on the decision heuristics. Considering DPLL both with and without clause learning, we present a relative efficiency hierarchy for refinements of DPLL resulting from combinations of decision heuristics (top-down restricted, justification restricted, and unrestricted heuristics) and branching styles (typical DPLL-style and ATPG-style branching). An an example, for DPLL without clause learning, we establish a strict hierarchy, with the ATPG-style, justification restricted branching variant as the weakest system.

Suggested BibTeX entry:

@inproceedings{JarvisaloJ:AAAI08,
    author = {Matti J{\"a}rvisalo and Tommi Junttila},
    booktitle = {Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI-08)},
    editor = {Dieter Fox and Carla P. Gomes},
    pages = {304--309},
    publisher = {AAAI Press},
    title = {On the power of top-down branching heuristics},
    year = {2008},
}