An Improved Generator for 3-CNF Formulas
| Autor: | S. I. Uvarov |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Discrete mathematics
Phase transition Control and Systems Engineering Computer Science::Logic in Computer Science Computer Science::Artificial Intelligence Computer Science::Computational Complexity Electrical and Electronic Engineering Conjunctive normal form Boolean satisfiability problem Boolean data type Mathematics |
| Zdroj: | Automation and Remote Control. 81:130-138 |
| ISSN: | 1608-3032 0005-1179 |
| DOI: | 10.1134/s0005117920010117 |
| Popis: | We consider the satisfiability problem (SAT) for Boolean formulas given in conjunctive normal form with the restriction that each clause contains three literals (3-CNF). Generation of random formulas with a fixed clause length is widely used in empirical studies. An interesting phenomenon of this method is the repeatedly confirmed linear dependence of the number of clauses in the formula on the number of Boolean variables at the point of the “phase transition” from satisfiable to unsatisfiable formulas (when the fraction of unsatisfiable formulas becomes prevailing). We propose and study a method for generating random formulas that has a smaller coefficient (3.49) of proportionality between the number of clauses and the number of variables at the point of the “phase transition” (for the previously known generation method this coefficient is 4.23). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|