As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
We present new complexity results on the compilation of CNFs into DNNFs and OBDDs. In particular, we introduce a new notion of width, called CV-width, which is specific to CNFs and that dominates the treewidth of the CNF incidence graph. We then show that CNFs can be compiled into structured DNNFs in time and space that are exponential only in CV-width. Not only does CV-width dominate the incidence graph treewidth, but the former width can be bounded when the latter is unbounded. We also introduce a restricted version of CV-width, called linear CV-width, and show that it dominates both pathwidth and cutwidth, which have been used to bound the complexity of OBDDs. We show that CNFs can be compiled into OBDDs in time and space that are exponential only in linear CV-width. We also show that linear CV-width can be bounded when pathwidth and cutwidth are unbounded. The new notion of width significantly improves existing upper bounds on both structured DNNFs and OBDDs, and is motived by a new decomposition technique that combines variable splitting with clause splitting.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.