Standard

Lower bounds for myopic DPLL algorithms with a cut heuristic. / Itsykson, Dmitry; Sokolov, Dmitry.

Algorithms and Computation - 22nd International Symposium, ISAAC 2011, Proceedings. 2011. p. 464-473 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7074 LNCS).

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

Harvard

Itsykson, D & Sokolov, D 2011, Lower bounds for myopic DPLL algorithms with a cut heuristic. in Algorithms and Computation - 22nd International Symposium, ISAAC 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7074 LNCS, pp. 464-473, 22nd International Symposium on Algorithms and Computation, ISAAC 2011, Yokohama, Japan, 5/12/11. https://doi.org/10.1007/978-3-642-25591-5_48

APA

Itsykson, D., & Sokolov, D. (2011). Lower bounds for myopic DPLL algorithms with a cut heuristic. In Algorithms and Computation - 22nd International Symposium, ISAAC 2011, Proceedings (pp. 464-473). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7074 LNCS). https://doi.org/10.1007/978-3-642-25591-5_48

Vancouver

Itsykson D, Sokolov D. Lower bounds for myopic DPLL algorithms with a cut heuristic. In Algorithms and Computation - 22nd International Symposium, ISAAC 2011, Proceedings. 2011. p. 464-473. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-25591-5_48

Author

Itsykson, Dmitry ; Sokolov, Dmitry. / Lower bounds for myopic DPLL algorithms with a cut heuristic. Algorithms and Computation - 22nd International Symposium, ISAAC 2011, Proceedings. 2011. pp. 464-473 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

BibTeX

@inproceedings{4a9dec8b46764ead87e7c5eb782b7640,
title = "Lower bounds for myopic DPLL algorithms with a cut heuristic",
abstract = "The paper is devoted to lower bounds on the time complexity of DPLL algorithms that solve the satisfiability problem using a splitting strategy. Exponential lower bounds on the running time of DPLL algorithms on unsatisfiable formulas follow from the lower bounds for resolution proofs. Lower bounds on satisfiable instances are also known for some classes of DPLL algorithms; this lower bounds are usually based on reductions to unsatisfiable instances. In this paper we consider DPLL algorithms with a cut heuristic that may decide that some branch of the splitting tree will not be investigated. DPLL algorithms with a cut heuristic always return correct answer on unsatisfiable formulas while they may err on satisfiable instances. We prove the theorem about effectiveness vs. correctness trade-off for deterministic myopic DPLL algorithms with cut heuristic. Myopic algorithms can see formulas with erased signs of negations; they may also request a small number of clauses to read them precisely. We construct a family of unsatisfiable formulas Φ (n) and a polynomial time samplable ensemble of distributions Q n concentrated on satisfiable formulas such that every deterministic myopic algorithm that gives a correct answer with probability 1-o(1) on a random formula from the ensemble Q n runs exponential time on the formulas Φ (n).",
author = "Dmitry Itsykson and Dmitry Sokolov",
year = "2011",
month = dec,
day = "26",
doi = "10.1007/978-3-642-25591-5_48",
language = "English",
isbn = "9783642255908",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "464--473",
booktitle = "Algorithms and Computation - 22nd International Symposium, ISAAC 2011, Proceedings",
note = "22nd International Symposium on Algorithms and Computation, ISAAC 2011 ; Conference date: 05-12-2011 Through 08-12-2011",

}

RIS

TY - GEN

T1 - Lower bounds for myopic DPLL algorithms with a cut heuristic

AU - Itsykson, Dmitry

AU - Sokolov, Dmitry

PY - 2011/12/26

Y1 - 2011/12/26

N2 - The paper is devoted to lower bounds on the time complexity of DPLL algorithms that solve the satisfiability problem using a splitting strategy. Exponential lower bounds on the running time of DPLL algorithms on unsatisfiable formulas follow from the lower bounds for resolution proofs. Lower bounds on satisfiable instances are also known for some classes of DPLL algorithms; this lower bounds are usually based on reductions to unsatisfiable instances. In this paper we consider DPLL algorithms with a cut heuristic that may decide that some branch of the splitting tree will not be investigated. DPLL algorithms with a cut heuristic always return correct answer on unsatisfiable formulas while they may err on satisfiable instances. We prove the theorem about effectiveness vs. correctness trade-off for deterministic myopic DPLL algorithms with cut heuristic. Myopic algorithms can see formulas with erased signs of negations; they may also request a small number of clauses to read them precisely. We construct a family of unsatisfiable formulas Φ (n) and a polynomial time samplable ensemble of distributions Q n concentrated on satisfiable formulas such that every deterministic myopic algorithm that gives a correct answer with probability 1-o(1) on a random formula from the ensemble Q n runs exponential time on the formulas Φ (n).

AB - The paper is devoted to lower bounds on the time complexity of DPLL algorithms that solve the satisfiability problem using a splitting strategy. Exponential lower bounds on the running time of DPLL algorithms on unsatisfiable formulas follow from the lower bounds for resolution proofs. Lower bounds on satisfiable instances are also known for some classes of DPLL algorithms; this lower bounds are usually based on reductions to unsatisfiable instances. In this paper we consider DPLL algorithms with a cut heuristic that may decide that some branch of the splitting tree will not be investigated. DPLL algorithms with a cut heuristic always return correct answer on unsatisfiable formulas while they may err on satisfiable instances. We prove the theorem about effectiveness vs. correctness trade-off for deterministic myopic DPLL algorithms with cut heuristic. Myopic algorithms can see formulas with erased signs of negations; they may also request a small number of clauses to read them precisely. We construct a family of unsatisfiable formulas Φ (n) and a polynomial time samplable ensemble of distributions Q n concentrated on satisfiable formulas such that every deterministic myopic algorithm that gives a correct answer with probability 1-o(1) on a random formula from the ensemble Q n runs exponential time on the formulas Φ (n).

UR - http://www.scopus.com/inward/record.url?scp=84055217288&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-25591-5_48

DO - 10.1007/978-3-642-25591-5_48

M3 - Conference contribution

AN - SCOPUS:84055217288

SN - 9783642255908

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 464

EP - 473

BT - Algorithms and Computation - 22nd International Symposium, ISAAC 2011, Proceedings

T2 - 22nd International Symposium on Algorithms and Computation, ISAAC 2011

Y2 - 5 December 2011 through 8 December 2011

ER -

ID: 49786553