This page is out-dated; see the OKlibrary which will become available beginning of 2008.

OKdatabase

Yet only some extracted statistics for random 3-CNF are available in SatStatistics_23052003.csv . The format is suitable for example for the R system: The first line is "n,d1,sat,c", where

"n" is the number of variables
"d1" is the density ("1" because only one clause-size is involved)
"sat" is the fraction of satisfied formulas
"c" (like "count") is the number of formulas at all

while the folloing lines contain corresponding 4-tuples of data, separated by commas.

Attention: The density is the standardised density, which basically is given by calculating the true density (number of clauses) / (number of variables), and then taking the minimal part of the decimal expension of this fraction, which after rounding yields the given number of clauses. This format is a good choice for storing densities in the database, but for statistical evaluation one should use the normal floating point approximation of the (true) density.

The number of variables is a positive integer, while the fraction of satisfied formulas and the number of formulas at all are floating point numbers (using double precision).

Oliver Kullmann

Last modified: Fri Dec 21 14:23:52 GMT 2007