[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-.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 -k [-c] [-p] [-h] [-f ] [-s ] [-z ] [-l ] [-m ] [-M ] 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.