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.