Number of the records: 1

Bounds on the Size of PC and URC Formulas

SYSNO ASEP	0536433
Document Type	J - Journal Article
R&D Document Type	Journal Article
Subsidiary J	Článek ve WOS
Title	Bounds on the Size of PC and URC Formulas
Author(s)	Kučera, P. (CZ) Savický, Petr (UIVT-O)_{SAI, RID, ORCID}
Source Title	Journal of Artificial Intelligence Research. - : AAAI Press - ISSN 1076-9757 Roč. 69, 24 December (2020), s. 1395-1420
Number of pages	26 s.
Publication form	Print - P
Language	eng - English
Country	US - United States
Keywords	automated reasoning ; knowledge representation ; satisfiability
Subject RIV	IN - Informatics, Computer Science
OECD category	Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
R&D Projects	GA19-19463S GA ČR - Czech Science Foundation (CSF)
Method of publishing	Open access
Institutional support	UIVT-O - RVO:67985807
UT WOS	000606811900034
EID SCOPUS	85099380435
DOI	10.1613/JAIR.1.12006
Annotation	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.
Workplace	Institute of Computer Science
Contact	Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800
Year of Publishing	2021
Electronic address	http://hdl.handle.net/11104/0314210

Number of the records: 1