Revisiting Decision Diagrams for SAT

Tom Van Dijk; Rüdiger Ehlers; Armin Biere

doi:10.48550/arXiv.1805.03496

Revisiting Decision Diagrams for SAT

Tom Van Dijk, Rüdiger Ehlers, Armin Biere

Institute of Formal Models and Verification

Research output: Working paper and reports › Preprint

Abstract

Symbolic variants of clause distribution using decision diagrams to eliminate variables in SAT were shown to perform well on hard combinatorial instances. In this paper we revisit both existing ZDD and BDD variants of this approach. We further investigate diﬀerent heuristics for selecting the next variable to eliminate. Our implementation makes further use of parallel features of the open source BDD library Sylvan.

Original language	English
Number of pages	7
DOIs	https://doi.org/10.48550/arXiv.1805.03496
Publication status	Published - 2018

Publication series

Name	arXiv.org
No.	1805.03496
ISSN (Print)	2331-8422

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.48550/arXiv.1805.03496

Cite this

@techreport{b03e0f1031de48bda28aa054bc2ebff8,

title = "Revisiting Decision Diagrams for SAT",

abstract = "Symbolic variants of clause distribution using decision diagrams to eliminate variables in SAT were shown to perform well on hard combinatorial instances. In this paper we revisit both existing ZDD and BDD variants of this approach. We further investigate diﬀerent heuristics for selecting the next variable to eliminate. Our implementation makes further use of parallel features of the open source BDD library Sylvan.",

author = "{Van Dijk}, Tom and R{\"u}diger Ehlers and Armin Biere",

year = "2018",

doi = "10.48550/arXiv.1805.03496",

language = "English",

series = "arXiv.org",

number = "1805.03496",

type = "WorkingPaper",

}

TY - UNPB

T1 - Revisiting Decision Diagrams for SAT

AU - Van Dijk, Tom

AU - Ehlers, Rüdiger

AU - Biere, Armin

PY - 2018

Y1 - 2018

N2 - Symbolic variants of clause distribution using decision diagrams to eliminate variables in SAT were shown to perform well on hard combinatorial instances. In this paper we revisit both existing ZDD and BDD variants of this approach. We further investigate diﬀerent heuristics for selecting the next variable to eliminate. Our implementation makes further use of parallel features of the open source BDD library Sylvan.

AB - Symbolic variants of clause distribution using decision diagrams to eliminate variables in SAT were shown to perform well on hard combinatorial instances. In this paper we revisit both existing ZDD and BDD variants of this approach. We further investigate diﬀerent heuristics for selecting the next variable to eliminate. Our implementation makes further use of parallel features of the open source BDD library Sylvan.

U2 - 10.48550/arXiv.1805.03496

DO - 10.48550/arXiv.1805.03496

M3 - Preprint

T3 - arXiv.org

BT - Revisiting Decision Diagrams for SAT

ER -