LATPub259: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| Zeile 20: | Zeile 20: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=It is known experimentally that there is a threshold for | |Abstract=It is known experimentally that there is a threshold for satisfiability in 3-CNF formulas around the value 4.25 for the ratio of variables to clauses. It is also known that the threshold is sharp, but that proof does not give a value for the threshold. | ||
satisfiability in 3-CNF formulas around the value 4.25 for the | We use purely combinatorial techniques to count the number of satisfiable boolean formulas given in conjunctive normal form. The intention is to provide information about the relative frequency of boolean functions with respect to statements of a given size, and to give a closed form formula for any number of variables, literals and clauses. We describe a correspondence between the syntax of propositions to the semantics of functions using a system of equations and show how to solve such a system. | ||
ratio of variables to clauses. It is also known that the threshold | |||
is sharp, but that proof does not give a value for the | |||
threshold. | |||
We use purely combinatorial techniques to count the number of | |||
satisfiable boolean formulas given in conjunctive normal form. | |||
The intention is to provide information about the relative | |||
frequency of boolean functions with respect to statements of a | |||
given size, and to give a closed form formula for any number of | |||
variables, literals and clauses. We describe a correspondence | |||
between the syntax of propositions to the semantics of functions | |||
using a system of equations and show how to solve such a system. | |||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 49: | Zeile 36: | ||
year = {2003}, | year = {2003}, | ||
} | } | ||
}} | }} | ||
Version vom 23. März 2015, 13:24 Uhr
Enumerating Satisfiable Propositional Formulae
Nachum DershowitzNachum Dershowitz, Mitchell A. HarrisMitchell A. Harris
Nachum Dershowitz, Mitchell A. Harris
Enumerating Satisfiable Propositional Formulae
Eurocomb, 2003
Enumerating Satisfiable Propositional Formulae
Eurocomb, 2003
- KurzfassungAbstract
It is known experimentally that there is a threshold for satisfiability in 3-CNF formulas around the value 4.25 for the ratio of variables to clauses. It is also known that the threshold is sharp, but that proof does not give a value for the threshold. We use purely combinatorial techniques to count the number of satisfiable boolean formulas given in conjunctive normal form. The intention is to provide information about the relative frequency of boolean functions with respect to statements of a given size, and to give a closed form formula for any number of variables, literals and clauses. We describe a correspondence between the syntax of propositions to the semantics of functions using a system of equations and show how to solve such a system. - Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@inproceedings{ DerschowitzHarris-Eurocomb2003,
author = {Nachum {Dershowitz} and Mitchell A. {Harris}},
booktitle = {Eurocomb},
title = {Enumerating Satisfiable Propositional Formulae},
year = {2003},
}
