About: A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
Creator	De Colnet, Alexis
Source	PMC
abstract	Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Several encodings with propagation strength guarantees rely upon prior compilation of the constraints into DNNF (decomposable negation normal form), BDD (binary decision diagram), or some other sub-variants. However it has been shown that there exist PB-constraints whose ordered BDD (OBDD) representations, and thus the inferred CNF encodings, all have exponential size. Since DNNFs are more succinct than OBDDs, preferring encodings via DNNF to avoid size explosion seems a legitimate choice. Yet in this paper, we prove the existence of PB-constraints whose DNNFs all require exponential size.
has issue date	2020-06-26(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51825-7_22
has license	no-cc
sha1sum (hex)	e571f2083485f4116c4f65de4edd1c51503a7253
schema:url	https://doi.org/10.1007/978-3-030-51825-7_22
resource representing a document's title	A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
has PubMed Central identifier	PMC7326562
schema:publication	Theory and Applications of Satisfiability Testing - SAT 2020
resource representing a document's body	covid:e571f2083485f4116c4f65de4edd1c51503a7253#body_text
is schema:about of	named entity 'encoding' named entity 'Constraints' named entity 'Yet' named entity 'encoding' named entity 'paper' named entity 'Since' named entity 'unit propagation' named entity 'guarantee' named entity 'unit propagation' named entity 'size' named entity 'integer' named entity 'Boolean variables' named entity 'CNF' named entity 'Boolean function' named entity 'Boolean variables' named entity 'subgraphs' named entity 'Boolean function' named entity 'finite set' named entity 'Boolean' named entity 'knowledge compilation' named entity 'Boolean' named entity 'binary number' named entity 'binary numbers' named entity 'knowledge compilation' named entity 'fanin' named entity 'BDD' named entity 'Boolean function' named entity 'OBDD' named entity 'CNF' named entity 'Boolean variables' named entity 'bipartite graph' named entity 'maximal matching' named entity 'polynomial' named entity 'maximal matching' named entity 'CNF' named entity 'NNF' named entity 'integer' named entity 'unit propagation' named entity 'base case' named entity 'matchings' named entity 'AND' named entity 'constraint satisfaction problem' named entity 'general idea' named entity 'NNF' named entity 'satisfiable' named entity 'OBDD' named entity 'positive integers' named entity 'ith' named entity 'upper bound' named entity 'BDD' named entity 'Boolean circuit' named entity 'Boolean function' named entity 'NNF' named entity 'Boolean function' named entity 'maximal matching' named entity 'Boolean function' named entity 'matchings' named entity 'maximal matching' named entity 'SAT' named entity 'maximal matching' named entity 'exponential space' named entity 'SAT' named entity 'binary numbers' named entity 'arc consistency' named entity 'Boolean function' named entity 'CNF' named entity 'maximal matching' named entity 'Boolean variables' named entity 'positive integers' named entity 'maximal matching' named entity 'Knowledge compilation' named entity 'Boolean function' named entity 'Boolean' named entity 'matchings' named entity 'Boolean variables' named entity 'subset' named entity 'matchings' named entity 'two-steps' named entity 'Boolean' named entity 'matchings' named entity 'maximal matching' named entity 'bipartite graph' named entity 'Boolean function'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software