Generating Models of a Matched Formula With a Polynomial Delay
Authors: Petr Savický, Petr Kučera
JAIR 2016 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We prove that the problem of counting the number of the models (satisfying assignments) of a matched formula is #P-complete. On the other hand, we define a class of formulas generalizing the matched formulas and prove that for a formula in this class one can choose in polynomial time a variable suitable for splitting the tree for the search of the models of the formula. As a consequence, the models of a formula from this class, in particular of any matched formula, can be generated sequentially with a delay polynomial in the size of the input. The main result of the paper is an algorithm which generates models of a matched formula with a polynomial delay. |
| Researcher Affiliation | Academia | Petr Savick y EMAIL Institute of Computer Science, The Czech Academy of Sciences Pod Vod arenskou Vˇeˇz ı 2, 182 07 Praha 8, Czech Republic. Petr Kuˇcera EMAIL Department of Theoretical Computer Science and Mathematical Logic Faculty of Mathematics and Physics, Charles University in Prague, Malostransk e n am. 25, 118 00 Praha 1, Czech Republic. |
| Pseudocode | Yes | Algorithm 1 Constructing pure literal sequence Require: A CNF formula ϕ. Ensure: A maximal strict pure literal sequence L for ϕ and the corresponding reduced formula. |
| Open Source Code | No | The paper does not provide any specific links or statements regarding the availability of open-source code for the methodology described. It discusses algorithms and theoretical complexity. |
| Open Datasets | No | This paper is theoretical and focuses on algorithms and proofs for boolean formulas. It does not conduct experiments using specific datasets, thus no information on publicly available datasets is provided. |
| Dataset Splits | No | The paper is theoretical and does not perform experiments on datasets. Therefore, it does not specify any training/test/validation dataset splits. |
| Hardware Specification | No | The complexity bounds are derived for the RAM model with the unit cost measure and the word size O(log ϕ ), where ϕ is the input formula. No specific hardware used for experiments is mentioned as the paper is theoretical. |
| Software Dependencies | No | The paper is theoretical and does not describe an implementation of its algorithms or present experimental results. Therefore, no specific software dependencies with version numbers are provided. |
| Experiment Setup | No | The paper describes theoretical algorithms and proofs, without presenting any experimental results. Consequently, there is no experimental setup, hyperparameters, or training configurations described. |