\texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver

DOI10.1007/s10601-008-9060-1zbMath1186.68442MaRDI QIDQ1037644

Ashish Sabharwal

Publication date: 16 November 2009

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-008-9060-1

zbMATH Keywords

planning; Boolean satisfiability; SAT; global symmetry; complete multi-class symmetry; high-level representation; SymChaff

Mathematics Subject Classification ID

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Related Items

SymChaff

Uses Software

• March_eq
• Walksat
• SATO
• PBS
• SAT competition
• Chaff
• BerkMin
• DIMACS
• Jerusat
• Velev SAT Benchmarks
• Shatter

Cites Work

• On the complexity of cutting-plane proofs
• An accurate and scalable collaborative recommender
• Short proofs for tricky formulas
• The intractability of resolution
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Resolution cannot polynomially simulate compressed-BFS
• Accelerating bounded model checking of safety properties
• The symmetry rule in propositional logic
• STRIPS: A new approach to the application of theorem proving to problem solving
• BerkMin: A fast and robust SAT-solver
• Dynamic Lex Constraints
• General Symmetry Breaking Constraints
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Theory and Applications of Satisfiability Testing
• Resolution lower bounds for the weak pigeonhole principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2003
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item