Bounds on the Size of PC and URC Formulas
Authors: Petr Kučera, Petr Savický
JAIR 2020 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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. |
| Researcher Affiliation | Academia | Petr Kučera EMAIL Department of Theoretical Computer Science and Mathematical Logic Faculty of Mathematics and Physics, Charles University Malostranské nám. 25, 118 00 Praha 1, Czech Republic Petr Savický EMAIL Institute of Computer Science of the Czech Academy of Sciences Pod Vodárenskou Věží 2, 182 07 Praha 8, Czech Republic |
| Pseudocode | Yes | Input: q-Horn formula ϕ(x), valuation γ satisfying γ(x) { 1/2, 1} for all x x Output: SAT if ϕ is satisfiable, UNSAT otherwise ... Algorithm 1: Satisfiability checking of a q-Horn formula (Boros et al., 1990) |
| Open Source Code | Yes | One of the algorithms implemented in this program uses the correspondence between dual rail encoding of a PC formula and a specific Horn function presented in Section 7 in this paper. By the results of Section 5, there is no guarantee for the existence of a reasonably sized PC formula equivalent to a given CNF, even if it belongs to a tractable class of Horn or q-Horn formulas. On the other hand, preliminary experiments (Kučera, 2019) with the program pccompile demonstrate that a compilation into a PC formula not introducing new auxiliary variables is frequently tractable for encodings of a few hundreds of clauses that appear as benchmarks in knowledge compilation. Further research is needed to clarify the conditions under which such a compilation is tractable. ... Kučera, P. (2020). Program pccompile. http://ktiml.mff.cuni.cz/~kucerap/ pccompile. Accessed: 2020-12-21. |
| Open Datasets | No | The paper investigates CNF encodings and proves theoretical bounds. It uses constructed formulas like ψn for proofs (e.g., in Section 5) rather than existing datasets for experimental evaluation. |
| Dataset Splits | No | The paper focuses on theoretical proofs and constructions of logical formulas, not on empirical experiments with datasets. Therefore, there is no mention of dataset splits. |
| Hardware Specification | No | The paper focuses on theoretical concepts and mathematical proofs concerning the size of logical formulas. There are no mentions of specific hardware used for any computational experiments. |
| Software Dependencies | No | While a program pccompile is mentioned as being used for 'preliminary experiments', no specific version numbers for software libraries, programming languages, or other dependencies are provided. Kučera, P. (2020). Program pccompile. http://ktiml.mff.cuni.cz/~kucerap/pccompile. Accessed: 2020-12-21. |
| Experiment Setup | No | The paper provides theoretical proofs and analyses regarding the size and properties of logical formulas. It does not describe any empirical experiments or their setup, thus no hyperparameters or training configurations are mentioned. |