[Created by Ashish Sabharwal, Cornell University, 2007]

April 12, 2007

This package has assorted scripts to work with XOR constraints for
model counting, sampling, and streamlining for Boolean satisfiability
(SAT) problems. The SAT solver Minisat is also included here, although
one may want to use other SAT solvers or model counters.

There are three scripts in the package, the first of which uses the
other two as subroutines and expects them to be in the path:

 gen-wff    : MAIN SHELL SCRIPT for adding XORs to a CNF formula

 randxor.pl : perl script for generating random XORs

 merge-cnfs : shell script for merging two CNF files


USAGE FOR GEN-WFF:

 gen-wff name_wff #vars #dummyvar #xors min_length max_length [num_output_wff]
         arg1     arg2  arg3      arg4  arg5       arg6       [arg7]

Here, arg1 is the name of the CNF file *without* the .cnf extension.
arg2 is the number of variables in the CNF formula, and in standard
usage, arg3=arg2. More generally, if you have a 150 var formula, but
you want to streamline only on the first 100 vars, you set #vars = 100
and #dummyvar = 150 randxor will now start numbering auxiliary vars at
151.

This will create arg4 random XORs of length between arg5 and arg6,
convert them to CNF form, and append them to the original formula. The
output is called file-str.cnf if the original filename was file.cnf.
When the optional arg7 is specified, the output file name is
file-str-<arg7>.cnf.

Internally, the random XORs are generated using randxor.pl and merged
with the original CNF file using merge-cnfs.


USAGE FOR RANDXOR.PL:

 randxor.pl -n <numvars> -k <numcons> [-c] [-p] [-h]
            [-f <xorfile>] [-s <seed>] [-z <maxnumvars>]
            [-l <avglength>] [-m <minlength>] [-M <maxlength>]

This is a stand-alone script (also used by gen-wff) that creates k
random XOR constraints on n variables using the specified parameters.
A dummy variable, always forced to be 1, is used to enforce even
parity. The constraints are output in a .xor file, and converted in
CNF form (using auxiliary variables) if the -c option is specified.
The -p option generates a different CNF translation that does not use
auxiliary variables but has size that is exponential in the length of
the XORs.

The desired filename can be given as an option using -f. For an
explanation of other parameters, see randxor.pl -h.


 
USAGE EXAMPLES:

Consider the included file example.cnf with 500 variables. We can add
to it 20 random XORs of length between 8 and 10 over all 500
variables, and have the resulting file be called
example-str-test1.cnf, using the following:

  gen-wff example 500 500 20 8 10 test1

This also generates example-str-test1.xor, which contains the 20 XOR
constraints in the natural non-CNF form.

If we instead wanted to append 20 random XORs as before but only
involving the first 100 variables of example.cnf and have the result
in example-str-test2.cnf, we would do:

  gen-wff example 100 500 20 8 10 test2



---

Please report bugs and send comments/questions to
  Ashish Sabharwal, sabhar at cs dot cornell dot edu.