SymChaff
swMATH ID:  938 
Software Authors:  Sabharwal, Ashish 
Description:  SymChaff: Exploiting symmetry in a structureaware satisfiability solve. his article presents a new lowoverhead framework for representing and utilizing problem symmetry in propositional satisfiability algorithms. While many previous approaches have focused on symmetry extraction as a key component, the novelty in the proposed strategy lies in using high level problem description to pass on symmetry information to the SAT solver in a simple and concise form, in addition to the usual conjunctive normal form formula. This information, comprising of the socalled symmetry sets and variable classes, captures variable semantics relevant to “complete multiclass symmetry” and is utilized dynamically to prune the search space. This allows us to address many limitations of alternative approaches like symmetry breaking predicates, implicit pseudoBoolean representations, general grouptheoretic methods, and zerosuppressed binary decision diagrams. We demonstrate the efficacy of our technique through a solver called SymChaff, which achieves exponential speedup over one of the best systematic SAT solvers on problems from both theory and practice, often by simply using natural tags or annotation in the problem specification 
Homepage:  http://www.cs.cornell.edu/~sabhar/software/symchaff/ 
Related Software:  MiniSat; Shatter; Chaff; Walksat; Traces; nauty; Velev SAT Benchmarks; Jerusat; DIMACS; BerkMin; SAT competition; PBS; SATO; March_eq; Graphplan; IPC4; MPI; YalSAT; reduce; Lingeling 
Referenced in:  6 Publications 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

SymChaff: Exploiting symmetry in a structureaware satisfiability solver. Zbl 1186.68442 Sabharwal, Ashish 
2009

all
top 5
Referenced by 15 Authors
Referenced in 4 Serials
1  Journal of Symbolic Computation 
1  Constraints 
1  INFORMS Journal on Computing 
1  Logical Methods in Computer Science 
Referenced in 2 Fields
5  Computer science (68XX) 
1  Operations research, mathematical programming (90XX) 