Name                    Last modified       Size  Description

 Parent Directory        06-May-2002 15:06      -  
 2bitadd_10.cnf          22-Apr-1996 11:45    31k  
 2bitadd_11.cnf          22-Apr-1996 11:45    34k  
 2bitadd_12.cnf          15-Jan-1996 13:50    37k  
 2bitcomp_5.cnf          15-Jan-1996 13:50     6k  
 2bitmax_6.cnf           22-Apr-1996 11:45    14k  
 3bitadd_31.cnf          22-Apr-1996 11:45   671k  
 3bitadd_32.cnf          15-Jan-1996 13:50   693k  
 3blocks.cnf             22-Apr-1996 11:45   207k  
 4blocks.cnf             22-Apr-1996 11:46   933k  
 4blocksb.cnf            22-Apr-1996 11:46   530k  
 all_examples.gz.uu      23-Feb-1996 10:42   2.2M  
 call-final.txt          17-Jan-1996 10:54     3k  
 call.final              01-Aug-1996 11:18     3k  
 e0ddr2-10-by-5-1.cnf    15-Jan-1996 13:50   1.8M  
 e0ddr2-10-by-5-4.cnf    22-Apr-1996 11:46   1.8M  
 enddr2-10-by-5-1.cnf    15-Jan-1996 13:50   1.9M  
 enddr2-10-by-5-8.cnf    22-Apr-1996 11:46   1.9M  
 ewddr2-10-by-5-1.cnf    15-Jan-1996 13:50   2.0M  
 ewddr2-10-by-5-8.cnf    22-Apr-1996 11:46   2.1M  
 guide.ps                15-Jan-1996 14:11    40k  
 guide.tex               15-Jan-1996 13:49     3k  
 max_num                 29-Feb-1996 12:16     1k  

This directory contains files for the International Competition and
Symposium on Satisfiability Testing.  The call for participation is in
call.final, and the guidelines for the SAT contest are in guide.tex
and guide.ps.  There are also six sample satisfiability problems.  All
are in the "dimacs" format:
	
	- any line starting with a "c" is a comment
	- at the top of the file is a line of form "p cnf <max_var> <clauses>",
	  where <max_var> is the number of the largest variable, and
	  <clauses> is the total number of clauses in the theory.
	- Clauses are separated by a zero ("0").

The files are in two groups.  The first group is the sample problems
that were given out before the contest, and the second group is
the problems used in the actual contest.

The sample problems are the following:
	
	2bitadd_12.cnf		- VLSI design -- 2 bit adder
	2bitcomp_5.cnf		- VLSI design -- 2 bit comparator
	3bitadd_32.cnf		- VLSI design -- 3 bit adder
	3blocks.cnf		- Block world planning -- Sussman anomaly on 3 blocks
	4blocks.cnf		- Block world planning -- Sussman anomaly on 4 blocks (version 1)
	4blocksb.cnf		- Block world planning -- Sussman anomaly on 4 blocks (version 2)
	e0ddr2-10-by-5-1.cnf    - Job shop scheduling -- 10 jobs of 5 tasks each, uniform deadlines
	enddr2-10-by-5-1.cnf	- Job shop scheduling -- 10 jobs of 5 tasks each, tight deadlines
	ewddr2-10-by-5-1.cnf	- Job shop scheduling -- 10 jobs of 5 tasks each, wide deadlines

The "real" problems are the following.  They are quite similar to the samples:

	2bitadd_11.cnf		- VLSI design -- 2 bit adder
	2bitmax_6.cnf		- VLSI design -- 2 bit max
	3bitadd_31.cnf		- VLSI design -- 3 bit adder
	3blocks.cnf		- Block world planning (different start and end states
				  than the sample)
	4blocks.cnf		- Block world planning (different start and end states)
	4blocksb.cnf		- Block world planning (different start and end states)
	e0ddr2-10-by-5-4.cnf    - Job shop scheduling -- 10 jobs of 5 tasks each, uniform deadlines
	enddr2-10-by-5-8.cnf	- Job shop scheduling -- 10 jobs of 5 tasks each, tight deadlines
	ewddr2-10-by-5-8.cnf	- Job shop scheduling -- 10 jobs of 5 tasks each, wide deadlines