DOI

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.
Original languageUndefined/Unknown
Title of host publicationTheory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004
EditorsHH Hoos, DG Mitchell
Place of PublicationBerlin
PublisherSpringer
Pages145-156
Number of pages12
ISBN (Print)3-540-27829-X
DOIs
Publication statusPublished - 2005
EventThe 7th International Conference on Theory and Applications of Satisfiability Testing, Vancouver, BC, Canada - Berlin
Duration: 10 May 200413 May 2004

Publication series

Name
PublisherSpringer
NameLecture Notes in Computer Science
Volume3542
ISSN (Print)0302-9743

Conference

ConferenceThe 7th International Conference on Theory and Applications of Satisfiability Testing, Vancouver, BC, Canada
Period10/05/0413/05/04

    Research areas

  • Wiskunde en Informatica, Techniek, technische Wiskunde en Informatica, conference contrib. refereed, ZX CWTS JFIS < 1.00

ID: 3209205