cse-logo Ashish Sabharwal's home page
UW CSE home page

SymChaff: A Structure-Aware Satisfiability Solver

SymChaff is a structure-aware propositional satisfiability solver (SAT solver) that uses a novel low-overhead framework for encoding and utilizing structural symmetry in the underlying problem domain. It is implemented as an extension of the popular state-of-the-art SAT solver zChaff. It uses semantic symmetry sets to partition the variables into several classes and to maintain and utilize symmetry information dynamically.

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.)

Download

The source code of SymChaff is available for download for personal or research use. The implementation (and the associated documentation) is "in progress" and is supplied "as is" without any warranties; see the full notice in the downloaded files. Please do not distribute it without the explicit permission of the author, including the authors of zChaff on which SymChaff is based.

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.

README-SymChaff
(included in the code package)		 README-SymChaff
Tar, bzipped file symchaff2005.12.07d.tar.bz2
Tar, gzipped file symchaff2005.12.07d.tar.gz
Zip file symchaff2005.12.07d.zip
zChaff version from Nov/Dec 2003 zchaff.2003.12.04.tar.gz

References, Publications

Ashish Sabharwal. SymChaff: Exploiting Symmetry in a Structure-Aware Satisfiability Solver. Preliminary version, under review for the Constraints journal. (pdf)

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)

Bug Reports and Comments

Please send an email to Ashish Sabharwal at .