Learning a Propagation Complete Formula

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Learning a Propagation Complete Formula

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Learning a Propagation Complete Formula

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA19-19463S" target="_blank" >GA19-19463S: Reprezentace booleovských funkcí úplné vzhledem k jednotkové propagaci</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

INTEGRATION OF CONSTRAINT PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND OPERATIONS RESEARCH, CPAIOR 2022

ISBN

978-3-031-08010-4

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

18

Strana od-do

214-231

Název nakladatele

SPRINGER INTERNATIONAL PUBLISHING AG

Místo vydání

CHAM

Místo konání akce

Los Angeles

Datum konání akce

20. 6. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000876685700015