Standard

Aligning CNF- and equivalence-reasoning. / Heule, MJH; van Maaren, H.

Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004. ed. / HH Hoos; DG Mitchell. Berlin : Springer, 2005. p. 145-156 (Lecture Notes in Computer Science; Vol. 3542).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Harvard

Heule, MJH & van Maaren, H 2005, Aligning CNF- and equivalence-reasoning. in HH Hoos & DG Mitchell (eds), Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004. Lecture Notes in Computer Science, vol. 3542, Springer, Berlin, pp. 145-156, The 7th International Conference on Theory and Applications of Satisfiability Testing, Vancouver, BC, Canada, 10/05/04. https://doi.org/DOI:10.1007/11527695_12

APA

Heule, MJH., & van Maaren, H. (2005). Aligning CNF- and equivalence-reasoning. In HH. Hoos, & DG. Mitchell (Eds.), Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004 (pp. 145-156). (Lecture Notes in Computer Science; Vol. 3542). Berlin: Springer. https://doi.org/DOI:10.1007/11527695_12

Vancouver

Heule MJH, van Maaren H. Aligning CNF- and equivalence-reasoning. In Hoos HH, Mitchell DG, editors, Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004. Berlin: Springer. 2005. p. 145-156. (Lecture Notes in Computer Science). https://doi.org/DOI:10.1007/11527695_12

Author

Heule, MJH ; van Maaren, H. / Aligning CNF- and equivalence-reasoning. Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004. editor / HH Hoos ; DG Mitchell. Berlin : Springer, 2005. pp. 145-156 (Lecture Notes in Computer Science).

BibTeX

@inproceedings{766dbaf5900b4fba88670a91ea5b8134,
title = "Aligning CNF- and equivalence-reasoning",
abstract = "Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the parity-family. Large instances of such CNF formulas cannot be solved in reasonable time if no detection of, and extra reasoning with, these clauses is incorporated. That is, in solving these formulas, there is a more or less separate algorithmic device dealing with the equivalence clauses, called equivalence reasoning, and another dealing with the remaining clauses. In this paper we propose a way to align these two reasoning devices by introducing parameters for which we establish optimal values over a variety of existing benchmarks. We obtain a truly convincing speed-up in solving such formulas with respect to the best solving methods existing so far.",
keywords = "Wiskunde en Informatica, Techniek, technische Wiskunde en Informatica, conference contrib. refereed, ZX CWTS JFIS < 1.00",
author = "MJH Heule and {van Maaren}, H",
year = "2005",
doi = "DOI:10.1007/11527695_12",
language = "Undefined/Unknown",
isbn = "3-540-27829-X",
publisher = "Springer",
pages = "145--156",
editor = "HH Hoos and DG Mitchell",
booktitle = "Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004",

}

RIS

TY - GEN

T1 - Aligning CNF- and equivalence-reasoning

AU - Heule, MJH

AU - van Maaren, H

PY - 2005

Y1 - 2005

N2 - Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the parity-family. Large instances of such CNF formulas cannot be solved in reasonable time if no detection of, and extra reasoning with, these clauses is incorporated. That is, in solving these formulas, there is a more or less separate algorithmic device dealing with the equivalence clauses, called equivalence reasoning, and another dealing with the remaining clauses. In this paper we propose a way to align these two reasoning devices by introducing parameters for which we establish optimal values over a variety of existing benchmarks. We obtain a truly convincing speed-up in solving such formulas with respect to the best solving methods existing so far.

AB - Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the parity-family. Large instances of such CNF formulas cannot be solved in reasonable time if no detection of, and extra reasoning with, these clauses is incorporated. That is, in solving these formulas, there is a more or less separate algorithmic device dealing with the equivalence clauses, called equivalence reasoning, and another dealing with the remaining clauses. In this paper we propose a way to align these two reasoning devices by introducing parameters for which we establish optimal values over a variety of existing benchmarks. We obtain a truly convincing speed-up in solving such formulas with respect to the best solving methods existing so far.

KW - Wiskunde en Informatica

KW - Techniek

KW - technische Wiskunde en Informatica

KW - conference contrib. refereed

KW - ZX CWTS JFIS < 1.00

U2 - DOI:10.1007/11527695_12

DO - DOI:10.1007/11527695_12

M3 - Conference contribution

SN - 3-540-27829-X

SP - 145

EP - 156

BT - Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004

A2 - Hoos, HH

A2 - Mitchell, DG

PB - Springer

CY - Berlin

ER -

ID: 3209205