========================== | SymChaff version 2005.03 | ========================== Created by Ashish Sabharwal, University of Washington, Seattle. Now at Cornell University. http://www.cs.cornell.edu/~sabhar http://www.cs.cornell.edu/~sabhar/software/symchaff Reference: "SymChaff: A Structure-Aware Satisfiability Solver." In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI), pp 467-474, Pittsburgh, PA, July 2005. The base code for this version of SymChaff is the version of zChaff from Nov 2003 (see file README-zChaff). The key new feature supported is symmetry as described in the paper referenced above. Most of the modifications/additions to the original zChaff code are marked by the word "Ashish" in the comments just before or after the change. The directory "EXAMPLES" contains some sample CNF, SYM, and ORD files (see below). The directory "extra-stuff" contains original features/files of zChaff that are not used in the current version of SymChaff. This code also contains work in progress towards supporting pseudo-Boolean input formats (i.e. inequalities over Boolean variables). It's not finished yet, so please ignore those command line options and code snippets. ------------------------------------------------------------------------- Compilation: Tested with GNU g++ 2.95, 3.2-3.4, and 4.0. NOTE: You will need the GNU getopt library. Run "make" from within this directory to compile. The output is an executable file called "symchaff." ------------------------------------------------------------------------- Runtime error codes (1-10 as in zChaff) - 0 : program exited normally 1 : can't open input file 2 : input line too long 3 : can't read header of input file 4 : ?? 6 : solution verification failed 10 : a fatal error occurred 11 : command-line error 12 : syntax error in input file 13 : consistency check failed when reading input files 14 : currently unsupported feature 15 : there is something wrong either with the code or with the input! ------------------------------------------------------------------------- Usage examples: 1) symchaff -t 60 php-030-029.cnf (symmetry info NOT used) 2) symchaff --sym --ord -f php.ord php-030-029 3) symchaff --version 4) symchaff --sym -r -m 256 log-rotate-07t6 5) symchaff --sym --printsoln log-rotate-05t7 6) symchaff -h 7) symchaff --sym --nolrn --ord -f clqcolor.ord clqcolor-30-18-21 ------------------------------------------------------------------------- Usage: symchaff [options] cnf_file[.cnf] Feature options [--pb] [--sym] [-f , --ord] General options [--nofb] [--nolrn] [--printsoln] [-r, --restarts] [-m ] [-t ] [-h, --help] [-v, --version] Debugging and tracing options [-d ] --pb Enables pseudo-Boolean processing. Default: disabled. Must use a .pbcnf file as input. NOTE: the implementation of this is currently in progress. --sym Enables the use of symmetry information. Default: disabled. Requires file .sym to be present. -f file, --ord Uses a domain specific ordering file to give priority to various variable classes and/or symindexes when selecting a variable to branch on. The default file used is .ord. It can be overridden with the -f option. Can only be used in conjunction with --sym. --nofb Disables fast backtracking. Default: enabled. NOTE: currently this option can be used *only* in conjunction with --sym. --nolrn Disables clause learning. Default: enabled. NOTE: I am not too confident that this is implemented correctly at the moment. --printsoln Enables printing of solution if SAT. Default: disabled. -r, --restarts Enables random restarts. Default: disabled. -m limit Sets the memory limit in MB. NOTE: there may be a bug in this at the moment. -t limit Sets the time limit in minutes. Default: 6 hours. -h, --help Prints usage. -v, --version Prints out the version of SymChaff. -d level Takes a value from 0 to 3. More debugging information is printed at higher debug levels. ------------------------------------------------------------------------- Examples: The directory "EXAMPLES" contains some sample CNF, SYM, and ORD files. A) php/php-005-004.sym is a symmetry file for the PHP formula with 5 pigeons and 4 holes. It specifies 2 symindex sets, [1-5] and [6-9] for the pigeons and the holes, respectively. There is a single varclass (also referred to as vartype in some places) indexed by these two symindex sets. The symindex map says, e.g., that variable 5 belongs to the first varclass and corresponds to mapping pigeon 2 to hole 6. B) clqcolor/clqcolor.ord is an ordering file for the clique coloring formulas. Its last section specifies that the three varclasses/vartypes should be prioritized in the order 3,2,1 in the branching heuristic. Its middle section says, e.g., that the second vartype should use its second index for multiway branching in preference to its first index; the reverse is true for the third vartype. C) channel-routing/chnl-004x005.sym is the symmetry file for a channel routing problem with 4 tracks and 5 nets. It specifies two symindex sets, for the left and right end points of the nets, resp. Although all nets as well as all tracks are symmetric, this file only considers tracks to be symmetric. Therefore, there are 2x5=10 varclasses instead of 2. -------------------------------------------------------------------------