Enumerating Satisfiable Propositional Formulae

Nachum DershowitzNachum Dershowitz, Mitchell A. HarrisMitchell A. Harris

Download

Nachum Dershowitz, Mitchell A. Harris
Enumerating Satisfiable Propositional Formulae
Eurocomb, 2003

Details
Bibtex

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},
}