About: Four Flavors of Entailment

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

About: Four Flavors of Entailment 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	Four Flavors of Entailment
Creator	Biere, Armin Möhle, Sibylle Sebastiani, Roberto
Source	PMC
abstract	We present a novel approach for enumerating partial models of a propositional formula, inspired by how theory solvers and the SAT solver interact in lazy SMT. Using various forms of dual reasoning allows our CDCL-based algorithm to enumerate partial models with no need for exploring and shrinking full models. Our focus is on model enumeration without repetition, with potential applications in weighted model counting and weighted model integration for probabilistic inference over Boolean and hybrid domains. Chronological backtracking renders the use of blocking clauses obsolete. We provide a formalization and examples. We further discuss important design choices for a future implementation related to the strength of dual reasoning, including unit propagation, using SAT or QBF oracles.
has issue date	2020-06-26(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51825-7_5
has license	no-cc
sha1sum (hex)	02d880b3d68991c64defe27f9e9324e11d5dd66d
schema:url	https://doi.org/10.1007/978-3-030-51825-7_5
resource representing a document's title	Four Flavors of Entailment
has PubMed Central identifier	PMC7326472
schema:publication	Theory and Applications of Satisfiability Testing - SAT 2020
resource representing a document's body	covid:02d880b3d68991c64defe27f9e9324e11d5dd66d#body_text
is schema:about of	named entity 'provide' named entity 'enumerating' named entity 'model' named entity 'unit propagation' named entity 'clauses' named entity 'models' named entity 'exploring' named entity 'model' named entity 'SAT solver' named entity 'theory' named entity 'Entailment' named entity 'QBF' named entity 'CDCL' named entity 'SAT solver' named entity 'SAT' named entity 'lazy' named entity 'entailment' named entity 'DPLL' named entity 'Boolean' named entity 'DNF' named entity 'CNF' named entity 'algorithm' named entity 'implication graph' named entity 'subsequence' named entity 'quantifier elimination' named entity 'negation' named entity 'truth values' named entity 'syntactic' named entity 'negation' named entity 'Satisfiability Modulo Theories' named entity 'CNF' named entity 'disjunction' named entity 'QBF' named entity 'unsatisfiable' named entity 'oracle' named entity 'syntactic' named entity 'CDCL' named entity 'disjunction' named entity 'truth values' named entity 'SAT solver' named entity 'CDCL' named entity 'preimage' named entity 'line 17' named entity 'algorithm' named entity 'CDCL' named entity 'QBF' named entity 'logical entailment' named entity 'DPLL' named entity 'backtracking' named entity 'SAT solver' named entity 'oracle' named entity 'oracle' named entity 'theory solver' named entity 'recursively' named entity 'CNF' named entity 'quantifiers' named entity 'entailment' named entity 'entailment' named entity 'SAT solver' named entity 'algorithm' named entity 'subset' named entity 'model checking' named entity 'oracle' named entity 'computational cost' named entity 'Sum-of-Products' named entity 'Gebser' named entity 'CNF' named entity 'CNF' named entity 'CNF' named entity 'search space' named entity 'UIP' named entity 'CNF' named entity 'unit propagation' named entity 'predicate abstraction' named entity 'CDCL' named entity 'concatenated' named entity 'SAT solver' named entity 'existential quantification' named entity 'Boolean' named entity 'preimage' named entity 'SAT solver'

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