INTRODUCTION
The program 'genRamsey.c' generates SAT or MAX SAT instances.
If you find a satisfying assignment for the SAT instance with parameters
(n, k, l), this implies that an n-vertex graph without k-clique and
l-independent set is found.
The format of the instance is the one used by M.G.C. Resende:
The first line: [the number of variables] [the number of clauses]
For each clasuse: [the number of literals] [weight] [literal] [literal]...
(negation is expressed by '-')
To get ordinary CNF format, please use the program 'msat2cnf.c'.
COMPILE
% gcc -O2 -o genRamsey genRamsey.c
% gcc -O2 -o msat2cnf msat2cnf.c
USAGE
To generate the instance of n=17, k=4 and l=4, input
% genRamsey n 17 k 4 l 4
then the instance is generated to stdout.
If you want to give random weights for clauses from the range [5, 100], input
% genRamsey n 17 k 4 l 4 weighted 1 weightmin 5 weightmax 100
The default values are: n=17, k=4, l=4, weighted=0, weightmin=1 and weightmax
=1000.
To get the CNF format, input
% genRamsey n 17 k 4 l 4 | msat2cnf
If you want to solve the weighted version, input
% genRamsey n 17 k 4 l 4 weighted 1 weightmin 5 weightmax 100 \
| msat2cnf keepweight 1
then the clause with weight w is generated w times to express the weight.