The OKgenerator-package has been removed since it is included in the OKlibrary which will become available beginning of 2008.
Current: Release 1.0 of Version 1.3.
For the release history see here .
OKgenerator is intended to be a strong and reliable formula generator for random clause-sets (conjunctive normal forms) with mixed clause-sizes, and also generalised random clause-sets (conjunctive normal forms for constraint satisfaction problems) can ge generated.
The underlying random source is AES (the Advanced Encryption Standard, that is, the Rijndael algorithm; see the Rijndael Page ) using 128 bits and the implementation by Brian Gladman. I want to create a (large) database for random formulas generated by OKgenerator, containing whether they are satisfiable or unsatisfiable, and also running times of solvers for them. This database will be accessible over the Internet, and should serve the following purposes (at least):
- Studying the phenomenon of phase transition.
- Developping better heuristics for SAT solvers (see the report below).
- Finding exceptionally hard random formulas.
The source code can be downloaded by clicking here .
Installation (on Linux/Unix systems)
- Go to the directory where the package OKRandGen1_38.tar.gz has been downloaded.
- If you are using a graphical desktop environment (like KDE or Gnome) you should be able to unpack the package by pointing the mouse to it, pressing the right mouse button, and choosing the "unpack" option. Otherwise give the following instructions to the shell:
- gunzip OKRandGen1_38.tar.gz
- tar -xf OKRandGen1_38.tar
- The directory OKRandGen1_3 has been generated in your working directory. Change into this directory (from the command line by cd OKRandGen1_3).
- Now you must issue the command make (if you are using KDE, then you can choose the menu option "execute command" (or something like that) from the file manager Konqueror). Hopefully the executable OKgenerator is created.
- To test the program, issue the command OKgenerator -h (you should get the list of possible options/actions; if you are using KDE and you don't know how to open a console for issuing commands: use the menu option "open terminal window" (or something like that) in Konqueror).
- In the file README you will find a first bit of information --- more of that you get in the sub-directory Documentation. A technical report describing OKgenerator (and also a general adaptive heuristics for SAT solvers based on evaluating random formulas) you find in Documentation/OKRandGen.pdf.
- Finally, by issuing the command make interprete_descriptor you can generate the program interprete_descriptor, which is also described in OKRandGen.pdf, and is a (first) tool for using OKgenerator.
- First technical report on the project as pdf-file, ps-file, dvi-file.
Last modified: Fri Dec 21 14:21:56 GMT 2007