Bounds on the Size of PC and URC Formulas

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F20%3A00536433" target="_blank" >RIV/67985807:_____/20:00536433 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/00216208:11320/20:10424839

Výsledek na webu

<a href="http://hdl.handle.net/11104/0314210" target="_blank" >http://hdl.handle.net/11104/0314210</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1613/JAIR.1.12006" target="_blank" >10.1613/JAIR.1.12006</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Bounds on the Size of PC and URC Formulas

Popis výsledku v původním jazyce

In this paper, we investigate CNF encodings, for which unit propagation is strong enough to derive a contradiction if the encoding is not consistent with a partial assignment of the variables (unit refutation complete or URC encoding) or additionally to derive all implied literals if the encoding is consistent with the partial assignment (propagation complete or PC encoding). We prove an exponential separation between the sizes of PC and URC encodings without auxiliary variables and strengthen the known results on their relationship to the PC and URC encodings that can use auxiliary variables. Besides of this, we prove that the sizes of any two irredundant PC formulas representing the same function differ at most by a factor polynomial in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.

Název v anglickém jazyce

Bounds on the Size of PC and URC Formulas

Popis výsledku anglicky

In this paper, we investigate CNF encodings, for which unit propagation is strong enough to derive a contradiction if the encoding is not consistent with a partial assignment of the variables (unit refutation complete or URC encoding) or additionally to derive all implied literals if the encoding is consistent with the partial assignment (propagation complete or PC encoding). We prove an exponential separation between the sizes of PC and URC encodings without auxiliary variables and strengthen the known results on their relationship to the PC and URC encodings that can use auxiliary variables. Besides of this, we prove that the sizes of any two irredundant PC formulas representing the same function differ at most by a factor polynomial in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.

Druh

J_imp - Článek v periodiku v databázi Web of Science

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

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2020

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 periodika

Journal of Artificial Intelligence Research

ISSN

1076-9757

e-ISSN

—

Svazek periodika

69

Číslo periodika v rámci svazku

24 December

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

26

Strana od-do

1395-1420

Kód UT WoS článku

000606811900034

EID výsledku v databázi Scopus

2-s2.0-85099380435