File	Date	Author	Commit
src	2012-12-18	Adrian Balint	[a74c18] Initial commit
license.txt	2012-12-18	adrianopol	[099f41] added license
readme.txt	2012-12-18	Adrian Balint	[a74c18] Initial commit

Read Me

Autor: Adrian Balint
Affiliation: Institute of Theoretical Computer Science, Ulm University, Germany 
Version: SAT Challenge 2012

UnifRandomKSATGenerator.java
----------------------------
--What is this?--

This class contains the generator function for the generation of 
uniform random k-SAT problems with a fixed clause length. 
The generator is guaranteed to not produce:
- clause containing the same variable twice
- duplicate clauses

The random number generator is the SHA1PRNG provided by SUN. 
It is a very good source of random numbers, though there are some drawbacks:
!!!! The generation process can drastically slow down if the entropy of the generated numbers decreases.!!!!
The best way to avoid this is by working on the machine that is used for the generation process.  
If everything slows down, then please be patient!

--How to use--

1. Generate an object of the UnifRandomKSATGenerator - this will start the generation process of the instance and create a header and comment string 
2. Create a file 
3. Call the method toDIMACS() to get the string representation of the generated instance together with the header and comments
4. write the string directly in the file


UnifKSATSeriesGenerator.java
----------------------------
--What is this?--
This is a generator for uniform random k-SAT instances using the UnifRandomKSATGenerator class.
It can generate a series of instances.

--How to use--
minimum set of parameters:
-clauseLength <int> 
-numVariables1 <int>
-ratio1 <double>

if you want to generate more than one instance:
-numInstances <int>

if you want to generate a series of instances between the points 
<numVariables1, ratio1> and <numVariables2,ratio2>
sampling
<numSamples> different combinations of <numVariables, ratio> 
then you also have to specify:
-numVariables2 <int>
-ratio2 <double>
-numSamples <int>

The sampled point will not be directly linear on the line but a ceratain step length
will be computed and then this will be used to sample <numSamples>.