The input to SymChaff is a traditional CNF file in the DIMACS format as well as an optional (much smaller) SYM file that captures the semantic nature of the symmetry or equivalence present in the given domain and instance. In this sense, SymChaff breaks away from the commonly used "black-box" nature of SAT solvers while at the same time enjoying the tremendous advances in propositional satisfiability we have witnessed in the last decade.
For a detailed description of its strengths, key features, and implementation details, please refer to the paper mentioned below.
(SymChaff was developed by Ashish Sabharwal as part of his Ph.D. thesis at the University of Washington, Seattle.)
Important note: As README-SymChaff points out, this version of SymChaff is based on the Nov 2003 version of zChaff. Since then, better versions of zChaff have been made available. For correctly evaluating the strength of the SymChaff approach, we suggest comparing against the older version of zChaff, linked below for convenience. This should be equivalent to not using the "--sym" switch with SymChaff.
(included in the code package)
|Tar, bzipped file||symchaff2005.12.07d.tar.bz2|
|Tar, gzipped file||symchaff2005.12.07d.tar.gz|
|zChaff version from Nov/Dec 2003||zchaff.2003.12.04.tar.gz|
Ashish Sabharwal. SymChaff: A Structure-Aware Satisfiability Solver. In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI), pp. 467-474, Pittsburgh, PA, July 2005. (pdf paper, ppt talk)