Loading...
Loading...

Go to the content (press return)

BDDs for Pseudo-Boolean Constraints

Author
Abío, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.
Type of activity
Presentation of work at congresses
Name of edition
SAT 2001. 14th International Conference Theory and Applications of Satisfiability Testing
Date of publication
2011
Presentation's date
2011-06-21
Book of congress proceedings
SAT 2011 - Theory and Applications of Satisfiability Testing
First page
61
Last page
75
Publisher
Springer Verlag
DOI
https://doi.org/10.1007/978-3-642-21581-0_7 Open in new window
Repository
http://hdl.handle.net/2117/14739 Open in new window
URL
http://www.springerlink.com/content/l76mt89727133500/ Open in new window
Abstract
Pseudo-Boolean constraints are omnipresent in practical applications, and therefore a significant effort has been devoted to the development of good SAT encoding techniques for these constraints. Several of these encodings are based on building Binary Decision Diagrams (BDDs) and translating these into CNF. Indeed, BDD-based encodings have important advantages, such as sharing the same BDD for representing many constraints. Here we first prove that, unless NP = Co-NP, there are Pseudo- Boolean c...
Citation
Abío, I. [et al.]. BDDs for Pseudo-Boolean Constraints. A: International Conference on Theory and Applications of Satisfiability Testing. "SAT 2011 - Theory and Applications of Satisfiability Testing". Ann Arbor, MI, USA: Springer Verlag, 2011, p. 61-75.
Group of research
LOGPROG - Logic and Programming

Participants