1996 | OriginalPaper | Buchkapitel
Satisfiability Problems for OFDDs
verfasst von : Ralph Werchner, Thilo Harich, Rolf Drechsler, Bernd Becker
Erschienen in: Representations of Discrete Functions
Verlag: Springer US
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We investigate the complexity of problems on Ordered Functional Decision Diagrams (OFDDs) related to satisfiability, i.e. SAT-ONE, SAT-ALL, and SAT-COUNT. We prove that SAT-ALL has a running time linear in the product of the number of satisfying assignments and the size of the given OFDD. Counting the satisfying assignments in an OFDD is proved to be #P-complete, and thus not possible in polynomial time unless P=NP.