Zur Seitenansicht
 

Titelaufnahme

Titel
On Compiling Structured CNFs to OBDDs
VerfasserBova, Simone ; Slivovsky, Friedrich
Erschienen in
Theory of computing systems, 2016,, S. 1-19
Erschienen2016
Ausgabe
Published version
SpracheEnglisch
DokumenttypAufsatz in einer Zeitschrift
Schlagwörter (EN)Knowledge compilation / Ordered binary decision diagram / Conjunctive normal
URNurn:nbn:at:at-ubtuw:3-2794 Persistent Identifier (URN)
DOI10.1007/s00224-016-9715-z 
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
On Compiling Structured CNFs to OBDDs [0.37 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

We present new results on the size of OBDD representations of structurally characterized classes of CNF formulas. First, we prove that variable convex formulas (that is, formulas with incidence graphs that are convex with respect to the set of variables) have polynomial OBDD size. Second, we prove an exponential lower bound on the OBDD size of a family of CNF formulas with incidence graphs of bounded degree. We obtain the first result by identifying a simple sufficient conditionwhich we call the few subterms propertyfor a class of CNF formulas to have polynomial OBDD size, and show that variable convex formulas satisfy this condition. To prove the second result, we exploit the combinatorial properties of expander graphs; this approach allows us to establish an exponential lower bound on the OBDD size of formulas satisfying strong syntactic restrictions.

Notiz
Lizenz
CC-BY-Lizenz (4.0)Creative Commons Namensnennung 4.0 International Lizenz