Learning a Propagation Complete Formula
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F22%3A10452217" target="_blank" >RIV/00216208:11320/22:10452217 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-031-08011-1_15" target="_blank" >https://doi.org/10.1007/978-3-031-08011-1_15</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-08011-1_15" target="_blank" >10.1007/978-3-031-08011-1_15</a>
Alternative languages
Result language
angličtina
Original language name
Learning a Propagation Complete Formula
Original language description
Propagation complete formulas were introduced by Bordeaux and Marques-Silva (2012) as a possible target language for knowledge compilation. A CNF formula is propagation complete (PC) if for every partial assignment, the implied literals can be derived by unit propagation. Bordeaux and Marques-Silva (2012) proposed an algorithm for compiling a CNF formula into an equivalent PC formula which is based on incremental addition of so-called empowering implicates. In this paper, we propose a compilation algorithm based on the implicational structure of propagation complete formulas described by Kucera and Savicky (2020) and the algorithm for learning a definite Horn formula with closure and equivalence queries introduced by Atserias et al. (2021). We have implemented both approaches and compared them experimentally. Babka et al. (2013) showed that checking if a CNF formula admits an empowering implicate is an NP-complete problem. We propose a particular CNF encoding which allows us to use a SAT solver to check propagation completeness, or to find an empowering implicate.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA19-19463S" target="_blank" >GA19-19463S: Boolean Representation Languages Complete for Unit Propagation</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
INTEGRATION OF CONSTRAINT PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND OPERATIONS RESEARCH, CPAIOR 2022
ISBN
978-3-031-08010-4
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
18
Pages from-to
214-231
Publisher name
SPRINGER INTERNATIONAL PUBLISHING AG
Place of publication
CHAM
Event location
Los Angeles
Event date
Jun 20, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000876685700015