Dear Mike TRICK,

   We send to you as an attached file, a generator "gensathard.c" of contradictory 3-SAT instances which seem to us very difficult for solving by any general method which is not specially devoted to these SAT instances. "gensathard.c" constructs instances according to a process which makes them contradictory.
We give below information for using "gensathard.c".

"gensahard.c" is a source C file. When "gensathard.c" runs, it is asking as input for an integer called degree "d". it constructs a 3-SAT contradictory instance with 3d variables and 8d clauses, each of them having 3 literals. The resultant instances is written in the output file "in.dat" which is generated automatically. The format of "in.dat" is as it follows:

  . the first line contains the degree: d = xx,
  . the second line contains the number of variables: n = xx,
  . the third line contains the number of clauses: p = xx,
  . the fourth line contains the number of literals per clause: r = 3,
  . each of the next p lines contains the values of the r literals per clause, separated wirth a blank; each literal is represented by an integer value between -n and n (except 0).

  
                                             Yours sincerely,

                                              Olivier Dubois.