# Enumerating Satisfiable Propositional Formulae

From International Center for Computational Logic

# Enumerating Satisfiable Propositional Formulae

##### Nachum DershowitzNachum Dershowitz, Mitchell A. HarrisMitchell A. Harris

Nachum Dershowitz, Mitchell A. Harris

**Enumerating Satisfiable Propositional Formulae***Eurocomb*, 2003**Kurzfassung****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. 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:**Automatentheorie

```
@inproceedings{ DerschowitzHarris-Eurocomb2003,
author = {Nachum {Dershowitz} and Mitchell A. {Harris}},
booktitle = {Eurocomb},
title = {Enumerating Satisfiable Propositional Formulae},
year = {2003},
}
```