This is an annotated description of the files and subdirectories in the ftp directory pub/challenge at dimacs.rutgers.edu. For more recent files, see the file NEW_FILES. Last Update: July 11, 1993 MT INDEX: This file. Contains a description of the files and subdirectories of the ftp directory pub/challenge at dimacs.rutgers.edu. call.tex: LaTeX source of the one page Call for Participation. call.ps: PostScript version of the one page Call for Participation. call.asc: ASCII version of the one page Call for Participation. call_abstract.asc Instructions for submitting abstracts for review (due date January 15, 1993). call_paper.asc Call for Papers for the October 11-13 workshop (due date August 3, 1993). gen_info.tex: General information on the Challenge including participating instructions and suggestions for research projects. (LaTeX source). gen_info.ps: General information on the Challenge including participating instructions and suggestions for research projects. (PostScript). *.UPD: Various messages mailed to participants. The file name gives date of mailing. contributed/: A subdirectory containing programs, documentation and other files concerning general issues. graph/: A subdirectory containing programs, documentation, and other files for finding cliques and graph coloring. satisfiability/:A subdirectory containing programs, documentation, and other files for the satisfiability problem. sat/: Another name for the above subdirectory (for those who don't like typing). submit/: A publically writeable directory for sending programs and other materials to the Challenge. proposals/: The set of proposals submitted in January (seven other proposals did not want to be made available for ftp). These are divided into "graph" (for clique and coloring proposals) and "sat" (for satisfiability proposals). A file with a one paragraph description of each proposal is being prepared, as is a complete list of files. ---------------------------------------------------------------------- Index contributed/: Index of contributed/hooker/: empirical.tex,empirical.dvi: A very nice paper from John Hooker (jh38+@andrew.cmu.edu) entitled "Needed: An Empirical Science of Algorithms" that I found to be very relevant to the Challenge. ---------------------------------------------------------------------- Index of graph/: doc/: Documentation regarding cliques and graph coloring. contributed/: Items contributed by participants on clique and graph coloring. solvers/: Programs to solve clique and coloring problems. translators/: Programs to translate from one format to another. benchmarks/: Some instances to benchmark algorithms and heuristics. ---------------------------------------------------------------------- Index of graph/doc: graph/doc/ccreview.tex: A review of past work on finding cliques and coloring graphs. This is a work in progress that will be updated as more information becomes available. This paper also has more than a dozen suggested research projects. Please write to challenge@dimacs.rutgers.edu if you have additional references or suggested research topics. graph/doc/ccreview.dvi, graph/doc/review.ps: dvi and postscript versions of above document. graph/doc/ccreview.bib: A BibTeX file of the references in the above. graph/doc/ccannote.tex: A TeX file that prints out all of the references along with a one or two line annotation on most of them. Requires BibTeX (a program normally bundled with TeX and LaTeX) and annotate.bst (below). graph/doc/annotate.bst: A BibTeX style file required for ccannote.tex. graph/doc/ccformat.tex: Suggested graph format consistent with the format used in the First Computational Challenge on networks and matchings. A fairly verbose but flexible format suitable for a variety of graph and network algorithms. Not yet the "official" format, but likely to become so unless strong objections are made. graph/doc/ccformat.dvi, graph/doc/format.ps: dvi and postscript versions of the above document. ---------------------------------------------------------------------- Index of graph/contributed: graph/contributed/culberson: Submitted by Joe Culberson of the University of Alberta (joe@cs.ualberta.ca). Includes an extensive bibliography on coloring. graph/contributed/jagota/: Work from Arun Jagota of SUNY Buffalo on using neural nets for cliques. graph/contrbuted/pardalos/: Work from Panos Pardalos of the University of Florida, including an extensive bibliography for cliques and a number of clique generators. graph/contributed/mannino/: Work from Carlo Mannino of the Universit\'a di Roma La Spienza. A joint paper with Antonio Sassano on an exact algorithm for stable sets. graph/contributed/morgenstern/: Work from Craig Morgenstern (morgenst@riogrande.cs.tcu.edu) containing generators and algorithms for graph coloring. graph/contributed/shor/: Work from Peter Shor (shor@research.att.com). Program and clique instances generated from that program related to the Keller conjecture. graph/contributed/lewandowski: generators and test problems for coloring register allocation graphs from Gary Lewandowski (gary@cs.wisc.edu). graph/contributed/soriano/: generators for clique instances from Patrick Soriano (patrick@crt.umontreal.edu). ---------------------------------------------------------------------- Index of graph/contributed/culberson/: color.bib: An extensive bibliography on graph coloring algorithms and applications. color.tex,color.dvi: Document that prints entire bibliography. ---------------------------------------------------------------------- Index of graph/contributed/jagota: KCC.dvi,KCC.ps: paper by Jagota and Reganon the average performance of several neural-net heuristics for the clique problem. nlt.README: Contains documentation and instructions for their compressible string generation code nlt_source.shar:C code related to the above report ijcnn92.tex: Latex source of IJCNN'92 paper on Approximating MAX-CLIQUE newgenerators.shar: Shar file containing new generators, seeds, and other information. ---------------------------------------------------------------------- Index of graph/contributed/pardalos: pardalos1.tex: A very complete bibliography and review of the clique problem by Pardalos and Xue. pardalos2.tex: A paper by Hassleberg, Pardalos, and Vairaktarakis on generating test clique problems. pardalos3.f: FORTRAN code for a partial enumeration routine for finding maximum cliques in graphs. pardalos4.f: FORTRAN code for a quadratic 0-1 based method for finding maximum cliques in graphs. c-fat.f, hamming.f, johnson.f, keller.f: FORTRAN codes for generators described in pardalos2.tex. ---------------------------------------------------------------------- Index of graph/contributed/mannino/: stable.tex: A paper by Carlo Mannino entitled "An Exact Algorithm for the Maximum Cardinality Stable Set Problem". stable.bib: Bibliography for above paper. stable.dvi, stable.ps: dvi and postscript versions of above. clut2graph.c: C program to generate instances of MAX CLIQUE from instances of minimum set covering. Uses dim_def.c. ---------------------------------------------------------------------- Index of graph/contributed/morgenstern/: Submitted by Craig Morgenstern of TCU (morgenst@riogrande.cs.tcu.edu). A tremendous number of generators and algorithms for graph coloring. The easiest way to get these is to get the" tarred and compressed" files that end .tar.Z morgenstern.tar.Z morgenstern1.tar.Z morgenstern3.tar.Z morgenstern4.tar.Z On a unix system, you need only then type uncompress morgenstern.tar.Z tar xvf morgenstern.tar to get the morgenstern subdirectory. The morgenstern 1, 3, and 4 subdirectories are then handled similarly. Alternatively, the subdirectories are currently expanded in this subdirectory. Here are the appropriate README files: graph/contributed/morgenstern/morgenstern: egen : Code to generate very large, maximally planar graphs using the expansion method. mpggen : Original planar graph generator that implements several methods. saturation.tex : Tech report C. Morgenstern and H. Shapiro. 1991. Improved Implementations of Dynamic Sequential Coloring Algorithms. Tech Report CoSc-1991-4, Texas Christian University, Fort Worth, Texas. graph/contributed/morgenstern/morgenstern1 mpggen : "Algorithmica" planar graph generator, modified to produce maps in dimacs challenge format. ggen : A graph generator to construct some known types of graphs, including random graphs, K-partite graphs, Leighton graphs, and geometric graphs. Graphs are dumped to a specified file in dimacs format. Leighton_in : Input files to build Leighton graphs using ggen. graph/contributed/morgenstern/morgenstern3: This directory contains an implementation of a localized backtracking heuristic for 4-coloring planar graphs and very sparse general graphs. This code is based on methods discussed in C. Morgenstern and H. Shapiro. 1991. Improved Implementations of Dynamic Sequential Coloring Algorithms. Tech Report CoSc-1991-4, Texas Christian University, Fort Worth, Texas. C. Morgenstern, 1992. A New Backtracking Heuristic for Rapidly Four-Coloring Large Planar Graphs. Tech Report CoSc-1992-2, Texas Christian University, Fort Worth, Texas. (Under revision, to be made available soon). graph/contributed/morgenstern/morgenstern4: This is the code used to produce the 4-coloring data given in C. Morgenstern and H. Shapiro. 1991. Heuristics for Rapidly Four-Coloring Large Planar Graphs. Algorithmica, 6, 869-891. Sample maps files are given in Rgo/MAPS/R002.Z and Ego/MAPS/E002.Z; the remaining maps described in the paper can be obtained from anon ftp in pub/morgenstern/maps on red.cs.tcu.edu (138.237.7.8). The entire map set requires 35 Megs compressed. Each map file contains 10 maps, and the res executable does a batch run and gathers statistics on all the maps in a file. ---------------------------------------------------------------------- Index of graph/contributed/shor: From Peter Shor (AT&T Bell Labs): shor@research.att.com shor.c: Here is my generator for Keller graphs. These graphs come from attempts at computer disproofs of Keller's conjecture (and were defined first by Corradi and Szabo). There's a size parameter (SIZE) defined in the program, and the most interesting case is probably when it's set to 6. For SIZE=6, I have found a large clique (by "hand") which is larger than any computer program has found so far. For 5 or less, computer programs have found the largest clique, so we know what it is. For SIZE=7, the graph is probably too big to put in the DIMACS challenge (14000 nodes, and reasonably dense). I would recommend putting at least the SIZE=5 and SIZE=6 graphs in. The SIZE=4 graph might be too small (Only 171 nodes, and the largest clique is size 11). Anyway, if somebody finds a clique larger than 59 vertices for SIZE=6, I'd be interested. keller4.clq: An instance generated from the above with SIZE=4. keller5.clq: An instance generated from the above with SIZE=5. ---------------------------------------------------------------------- Index of graph/contributed/lewandowski/: reg.shar: a shar file (recreate with the command "sh reg.shar" that contains code and test problems for coloring problems from register allocation graphs. The below describes the resulting directory structure: code/ contains Preston Briggs's code to pull out register allocation graphs from iloc files. Read the README file in code/ to get more information on his work. You must compile this code before you can construct any graphs. datafiles/ contains many iloc files, courtesy of Preston Briggs. bin/ contains Make_register_graphs. This is a shell script which takes a list of iloc file names (just the names, not the path, unless you change the file) and outputs the interference graphs that result from running Briggs's igraph program on the files. These files are constructed in DIMACS challenge format. testfiles/ results of Make_register_graphs are stored here. The files with .dat suffixes are the DIMACS format graphs. The .i files are the output of Brigg's program. I've got some examples in there right now so you can see what the output looks like. Questions, comments? email gary@cs.wisc.edu ---------------------------------------------------------------------- Index of graph/contributed/soriano/: gen_p_hat.p: PASCAL source for a generator of P_HAT clique From the code: (* Random graph generator that generates graph instances according to *) (* the P_HAT generation scheme as described in: *) (* Gendreau, M., P. Soriano and L. Salvail, "Solving the maximum clique *) (* problem using a tabu search approach", Annals of Operations Research *) (* 41, 385-403 *) (* *) (* Author: Patrick Soriano *) (* Date: 29-07-1993 *) (* *) ---------------------------------------------------------------------- Index of graph/solvers/: (From the README): To aid in comparisons between papers on the clique problem, the DIMACS Challenge Steering Committee is making available two benchmark programs, dfmax.c and dmclique.c. PROGRAM 1: dfmax.c implements a simple-minded branch-and-bound algorithm very similar to that of Carraghan and Paradalos [Oper.Res.Lett. 9 (1990), 375-382]. Subproblems are pruned only when the number of vertices still eligible for the clique is not enough to unseat the current champion. This C code, written by David Applegate and David Johnson, has a somewhat tighter inner loop than does the C&P Fortran code, and runs significantly faster on a variety of architectures. It assumes a 32-bit word length, but otherwise should be reasonably portable. It appears to compile successfully under both ANSI and non-ANSI C-compilers and has been run on a VAX-8550, various SGI machines, and SPARCstations. On an SGI Challenge computer (comparable to a DEC Alpha or a Sun SPARCstation 10), it can handle a 500 vertex, p=0.5 random graph in 3 minutes. A summary of results of the SGI Challenge for random graphs and the DIMACS benchmarks is in the file results.dfmax. INPUT: dfmax is designed to take as input the compressed "clq.b" format used in the DIMACS benchmark directories. Usage: "dfmax filename". OUTPUT: To indicate that dfmax is making progress (always useful in a potentially exponential time algorithm), it prints a line of output each time a vertex is eliminated from further consideration, giving the current biggest clique found and the current running time (assuming your computer's clock ticks 100 times per second). It also reports input time at the beginning of a run and outputs the clique at the end. PROGRAM 2: dmclique.c is a variant on the simple "semi-exhaustive greedy" scheme for finding large independent sets used in the graph coloring algorithm XRLF described in Johnson, Aragon, McGeoch, and Schevon [Oper.Res. 39 (1991), 378-406], originally suggested by Matula and Johri. dmclique has four integer input parameters, SETLIM, TRIALNUM, CANDNUM, and ITERATIONS, of which the key parameters are SETLIM and CANDNUM. The algorithm proceeds as follows: At any given time there is a set C (initially empty) of vertices in the current clique, and a set U consisting of all those remaining vertices that are adjacent to all members of C. If |U| <= SETLIM, the branch-and-bound code of dfmax (without the initial C&P pre-ordering) is invoked to find the maximum clique in U, and this is added to C. Otherwise, we sample CANDNUM vertices (with replacement) and choose one with maximum degree (ties broken in favor of the earlier index). The chosen vertex is then added to C, U is updated, and we repeat. We then repeat the entire process TRIALNUM*ITERATIONS times. Algorithm dmclique algorithm has much in common with the "GRASP" algorithm of Feo and Resende, except the latter sets SETLIM = 0 and uses a final local optimization phase to improve the clique found, typically with slightly better results than are obtained with dmclique. The value of dmclique as a benchmark code (as with dfmax) is that it represents what can be obtained by a (relatively) efficient implementation of the most straightforward of ideas. As with dfmax.c, dmclique.c should compile successfully on a variety of machines. A summary of results on an SGI Challenge for random graphs and the DIMACS Challenge benchmarks is given in the file "results.dmclique" These tests were all done with TRIALNUM = 1 and ITERATIONS = 1000, and the file reports the distributions of clique sizes found over those 1000 runs. Setting the parameters SETLIM and CANDNUM was by trial and error, but as a rule of thumb, take CANDNUM between |V|/5 and |V|/4, and start with SETLIM = 100 for density <= 0.5, SETLIM = 50 for density = 0.7, and SETLIM = 30 for density = 0.9. INPUT: dmclique, like dfmax, is designed to take as input the compressed "clq.b" format used in the DIMACS benchmark directories. Usage: "dmclique filename SETLIM TRIALNUM CANDNUM ITERATIONS". OUTPUT: An initial output line reports the parameter settings. The second output line gives the input time. Then there is one output line for each successive set of TRIALNUM runs, giving the size of the best clique found during those runs as well as the total time taken for those runs. The best clique found is currently NOT output, although it would be a simple matter to modify the code so it was. ---------------------------------------------------------------------- Index of graph/translators/: binformat/: Description and code for a more compact representation of graphs. ---------------------------------------------------------------------- Index of graph/translators/binformat/: README.binformat: A description of the compact graph representation. ANSI/binformat.shar: Shar file containing ANSI C source code for converting to and from binary format. These codes include: bin2asc: convert from binary (.b) to ascii asc2bin: convert from ascii to binary showpreamble: show preamble of a binary file NotANSI/binformat.shar: Shar file containing K&R C source code for the above. ---------------------------------------------------------------------- Index of graph/benchmarks/: clique/: Some clique instances to benchmark algorithms and heuristics color/: Some graph coloring instances to benchmark algorithms and heuristics Since these directories will change, please check for current contents. The file contents.tex (which requires use of supertab.sty) outlines the currently used instances. ---------------------------------------------------------------------- Index of sat/: doc/: Documentation regarding satisfiability and maximum satisfiability contributed/: Items contributed by participants on satisfiability and maximum satisfiability. translators/: Code to translate from one format to another. benchmarks/: Some instances to benchmark algorithms and heuristics. ---------------------------------------------------------------------- Index of sat/doc/: satreview.tex: Document containing problem definitions, suggested readings and possible projects. satreview.dvi,satreview.ps: DVI and PostScript versions of above. ---------------------------------------------------------------------- Index of sat/contributed/: selman/: Work of Bart Selman (AT&T) Bell Laboratories on methods for generating and solving hard satisfiability problems. gent/: Work of Ian Gent (University of Edinburgh) on Hill Climbing Procedures for SAT. dubois/: Work of Olivier Dubois (dubois@laforia.ibp.fr) on generating and solving satisfiability problems. naylor/: Work of William Naylor (naylor@research.canon.oz.au) on a program which translates integer questions into satisfiability instances. barth/: Work of Peter Barth (barth@mpi-sb.mpg.de) on an implementation of the Davis Putnam procedure. UCSC/: Work of Allen Van Gelder and others at UCSC (avg@cs.ucsc.edu) including a parser for DIMACS format cnf files. stamm-wilbrandt/: Work of Hermann Stamm-Wilbrandt (hermann@holmium.informaik.uni-bonn.de) that gives a number of reductions from hard and easy problems to satisfiability. crawford/: Work of James Crawford (jc@research.att.com) that describes how to generate sat problems from parity learning and described the behavior of satisfiabilty problems as a function of problem size. iwama/: Work of Kazuo Iwama (iwama@csce.kyushu-u.ac.jp) on generators for satisfiability. ---------------------------------------------------------------------- Index of sat/contributed/selman/: This directory contains two papers and one C program. Papers: hsat.ps --- on how to generate *hard* random formulas. gsat.ps --- on a randomized local search method that solves satisfiable instances that are one order larger than that can be solved with backtrack style methods. Program: mwff.c --- formula generator. ---------------------------------------------------------------------- Index of sat/contributed/gent This directory contains two files. They are postscript versions of two recent reports. These papers will soon be available as Technical Reports from Dept of AI, University of Edinburgh, Scotland. enigma.ps "The Enigma of SAT Hill-climbing Procedures" In this paper, we investigate a family of hill-climbing procedures related to GSAT, a greedy random hill-climbing procedure for satisfiability. These procedures are able to solve large and difficult satisfiability problems beyond the range of conventional procedures like David-Putnam. We explore the role of greediness, randomness and hill-climbing in the effectiveness of these procedures. In addition, we observe some quite remarkable and universal features of their search for a satisfying truth assignment. gensat.ps "Towards an Understanding of Hill-climbing Procedures for SAT" Recently several local hill-climbing procedures for propositional satisfiability have been proposed which are able to solve large and difficult problems beyond the reach of conventional algorithms like Davis-Putnam. By the introduction of some new variants of these procedures, we provide strong experimental evidence to support the conjecture that neither greediness nor randomness is important in these procedures. One of the variants introduced seems to offer significant improvements over earlier procedures. In addition, we investigate experimentally how performance depends on their parameters. Our results suggest that run-time scales less than simply exponentially in the problem size. ---------------------------------------------------------------------- Index of sat/contributed/dubois: A collection of routines submitted by Prof O. Dubois (dubois@laforia.ibp.fr) for generating and solving satisfiability problems. The abstract dubois.tex explains how these programs can be used. Note: Asat is a binary executable that can only run on Sun workstations. gensathard.c: A generator that provides hard satisfiability problems. ---------------------------------------------------------------------- Index of sat/contributed/naylor: This directory contains a program which translates integer questions into satisfiability problems. To translate a question into a satisfiability problem, you must 1) Pose the problem in main.c (see examples already there). Use the C subroutines defined below. 2) Type "make" to cause the C compiler to compile your question. 3) Type main > problem.txt to produce your satisfiability problem. stderr gets a message like i1: int 1-3 i2: int 4-6 i3: int 7-12 This means that problem integer variable "i1" has been allocated satisfiability problem boolean variables v1-v3. "i2" has been allocated v4-v6, etc. You need this information to intepret the solution to the satisfiability problem. problem.txt contains the generated satisfiability problem. It contains text such as this: 7 8 -9 -10 -11 12 -1 2 3 -4 5 6 1 -7 4 -7 -1 -4 7 This means (v7)&(v8)&(~v9)&(~v10)&(~v11)&(v12)&(~v1|v2|v3)&(~v4|v5|v6)&(v1|~v7)& (v4|~v7)&(~v1|~v4|v7) See the README file for more details. ---------------------------------------------------------------------- Index of sat/contributed/barth/: dp.tar: Tar file of implementation of Davis Putnam procedure implementation. README.dp: corresponding README file dp02.tar: New an improved version including a number of heuristics to improve the implementation. README.dp02: corresponding README file (partially listed below) This package contains the ANSI C sources of an implementation of the well known Davis Putnam procedure for solving propositional satisfiability problems. It should compile without any warnings. HEURISTICS: Up to now 6 variable choosing heuristics: none (-h0) first variable left is chosen positive (default) Jeroslow/Wang (-h1) as described in their paper: "Solving propositional satisfiability problems" R.E. Jeroslow and J. Wang Annals of {M}athematics and {AI} Pages 167-187; Volume 1; 1990 max. number of occurrences (-h2) The *variable* with the maximal number of occurrences is selected with sign of the maximal number of occurrences with this sign. A variant of JW (-h3) We use the same evaluation function as in JW, but we evaluate not each literal on its own but the sum of pos. and neg. sign as in (h2). random (-h4) select randomly a literal. At each invocation there should be another result as the random number generator is initialized with the current time. A variant from h2 (-h5) The *variable* with the maximal number of occurrences *in binary clauses* is selected with sign of the maximal number of occurrences with this sign. If there are several maximal variables use h2. This heuristic comes from Andreas Eisele . Another variant of h2 (-h6) literal X with max. vector under lexicographic order (H_2(X),H_3(X),....) where H_i(X) is 1*max(h_i(X),h_i(-X)) + 2*min(h_i(X),h_i(-X)) where h_i(X) is the number of clauses of length i containing X Idea of heuristic from Max Boehm : boehm@engels1.cs.uni-duesseldorf.de ---------------------------------------------------------------------- Index of sat/contributed/stamm-wilbrandt/: IAI-TR-93-3.ps: A technical report that gives a number of reductions from hard and easy problems to satisfiability. These reductions might be an interesting source of instances. ---------------------------------------------------------------------- Index of sat/contributed/UCSC/: instances/: A large number of instances based on circuit verification. There is also a parser, replacing the code in the former parser/ directory. From the README: Three tar files contributed, 2 compressed, from UCSC. July 9, 1993 Each is a directory when untarred. Be sure to use binary mode on ftp. Cnfparse REPLACES our earlier contributed parser for cnf, and includes a new program cnfsqueeze. Cnfgen gives programs and scripts to generate formulas, with careful attention to producing reproducible and comparable experiments. See its README for details. cnf-ssa is a directory of cnf formulas from Larrabee's test pattern generator. Each formula is compressed within the directory so you can "open" a few at a time and conserve disk space. Again, details in README. cnf-bf is a directory of cnf formulas from Larrabee's test pattern generator. Each formula is compressed within the directory so you can "open" a few at a time and conserve disk space. Details in README-bf. See also README in cnf-ssa. Note that "ssa" means "single-stuck-at" and "bf" means "bridge fault". ---------------------------------------------------------------------- Index of sat/contributed/crawford: README: Describes how to generate satisfiability problems from parity learning problems. Parity problems: Propositional versions of parity learning problems. These theories are guaranteed to be SAT (assuming my generator is bug free !) but seem to be difficult for both systematic and local search based methods (there is some theoretical indication that they might be quite hard in general). Details are given in the README file. tableau.ps: Description of an experiment to examine the cross-over point in randomly generated 3-SAT problems. This is the post-script version of our paper from AAAI. It reports on a large collection of experiments to determine as precisely as possible the location of the cross-over point in randomly generated 3-SAT problems. The main result is that at cross-over the number of clauses seems empirically to be a *linear* function of the number of variables. ---------------------------------------------------------------------- Index of sat/contributed/iwama/: From kazuo Iwama (iwama@csce.kyushu-u.ac.jp) iwama_prog.sh: Shell file (extracted by "sh iwama_prog.sh") for two generators (one for satisfiable and one for unsatisfiable instances) with control on attributes of instances. ---------------------------------------------------------------------- Index of sat/contributed/pretolani/: From Daniele Pretolani (daniele@crt.umontreal.edu) pretolani.tar: tar file ("tar xvf pretolani.tar" will restore files) containing two generators (source) and two solution codes (SUN Sparc binaries) for satisfiability. From the README: 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. ---------------------------------------------------------------------- Index of sat/contributed/zhang/: From Hantao Zhang (hzhang@cs.uiowa.edu) sato.tar.Z: Contains source for "sato", a decision procedure for propositional logic. From the README: This file contains instructions to install sato, a decision procedure for propositional logic written in C by Hantao Zhang. 1. Copy the file sato.tar.Z into your directory. 2. Extract the Files: % zcat sato.tar.Z | tar xvf - The following files will be generated: README macros.h main.c proto.h defs.h makefile search.c tree.c 3. Install Sato: % make The following messages will appear on a sunworkstation: cc -O -DBSD -target sun4 -c main.c cc -O -DBSD -target sun4 -c clocks.c cc -O -DBSD -target sun4 -c tree.c cc -O -DBSD -target sun4 -c search.c cc -O -DBSD main.o clocks.o tree.o search.o -lc -o sato size sato text data bss dec hex 24576 8192 0 32768 8000 4. Run Sato: % sato Usage: sato [] Options are: -f : use the input format suggested by DIMACS -p : preprocess (sort) input clauses -m : set the number of expected models (0 for all) -l : set the the number of variables printed per line -t : set the trace level (2-4: search; 5-8: build; 9: all) -s : select an atom in clauses for branching: n = 0: the first minimal atom; n = 1: an atom in shortest positive clauses (default); n = 2: a variant of n = 1; n = 3: an atom with most occurrences; n = 4: an atom with most occurrences in all/binary clauses; n = 5: an atom with most Jeroslow-Wang weight. -B : Bennett's quasi group problem of order n -P : The Pigeonhole problem (n holes, n+1 pigeons) -Q : The Queen problem (n queens on an n by n chessboard) -R : The Ramsey number r(p, q) = n with -P

and -Q Input_file is either `-' (denotes the standard input) or a file name. The input consists of a list of clauses, each of which is a list of nonzero integers surrounded by parentheses. When -p is not set, the integers in each list must be in the increasing order of absolute values, e.g. (1 -2 3 -4); otherwise, (-1 1) is parsed as (1 1), and (1 -1) as (-1 -1). 5. Benchmarks: With the options -P, -Q, and -B, sato generates the input clauses for pigeonhole problems, queen problems, and Bennett quasigroups, respectively. The following input files are also enclosed: jobs The job assignment puzzle latinsq The latin-square puzzle lion Raymond Smullyan's lion and unicorn puzzle nonobv Pelletier and Rudnicki's nontrivial problem salt Lewis Carroll's salt-mustard puzzle school Raymond Smullyan's school boys puzzle zebra Raymond Smullyan's zebra puzzle ---------------------------------------------------------------------- Index of sat/translators/: This directory contains translators to convert from one format to another. cnf2sat.c: Convert from the DIMACS standard .cnf format to the .sat format sat2cnf.c: Convert a conjunctive normal form formula in DIMACS standard .sat format to .cnf format sample.sat: Sample .sat format file sample.cnf: Sample .cnf format file ---------------------------------------------------------------------- Index of sat/benchmarks/: sat/: Instances in .sat format cnf/: Instances in .cnf format Since these directories will change, please check for current contents. The file contents.tex (which requires use of supertab.sty) outlines the currently used instances. ---------------------------------------------------------------------- ----------------------------------------------------------------------