
This directory contains SAT solvers and input generators, contributed to
the Second DIMACS Challenge.
Further informations and some preliminary experimental results can be
found in: 
  "Solving Satisfiability Problems: An Algorithm Implementation Challenge?"
   by D. pretolani,
submitted for presentation at the conference. 

CONTENTS:

Generators ------------------------------------------------------------------

DCNF.c 
        A generator of k-SAT formulas, and formulas where the number of
        literals per clause varies in the interval [l..r] with a Discrete
        Uniform Distribution (DUD). It takes as input a file with the
        following data:

          n            number of variables;
          m            number of clauses;
          type         0 = k-SAT;  1 = DUD;
          l            left bound (k if type = 0);
          r            right bound (k if type = 0);
          seed         seed -  if equal to 0, the actual seed is obtained using
                               the "time(0)" function;

        The output is in "cnf" format.

trisat.c 
        A generator of 3-SAT problems in a class defined by Urquhart, 
        encoding a 'graph 2-coloring with parity constraints' problem in
        terms of satisfiability. Problems are satisfiable if the parity value
        (Charge) is 0, and unsatisfiable otherwise.
        Usually, unsatisfiable instances are much harder.
        Input is interactive; the program asks for:

        number of nodes in the graph (even);
        parity value "Charge";
        percent of Horn clauses in the formula;

        The output is in "cnf" format, and is written in the file "formule1".



Solvers ------------------------------------------------------------------
        
NA1     Sparc-2 executable file of a DPL algorithm. This algorithm uses the
        following well known branching strategy: select a variable with
        maximum number of occurrences in clauses of minimum length.
        Input and output are in "cnf" format.

NV      Sparc-2 executable file of a version of NA1 including a pruning
        technique.

       
       WARNING: the submitted code is still under testing.
                Reports on errors or inconsistencies are welcome.
                Source code may be made available on request.


-------------------------------------------------------------------------------

Daniele Pretolani
e-mail		daniele@crt.umontreal.ca
Tel.            +1 - 514 - 343 6111 # 8708 
Fax             +1 - 514 - 343 7121

