Research output: Chapter in Book/Conference proceedings/Edited volume › Conference contribution › Scientific › peer-review

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

Research output: Chapter in Book/Conference proceedings/Edited volume › Conference contribution › Scientific › peer-review

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

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). Springer. https://doi.org/DOI:10.1007/11527695_12

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

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

note = "null ; Conference date: 10-05-2004 Through 13-05-2004",

}

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

Y2 - 10 May 2004 through 13 May 2004

ER -

ID: 3209205