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

DOI10.1007/s10601-008-9060-1zbMath1186.68442OpenAlexW2003590658MaRDI 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

planningBoolean satisfiabilitySATglobal symmetrycomplete multi-class symmetryhigh-level representationSymChaff

Mathematics Subject Classification ID

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

Related Items (5)

An adaptive prefix-assignment technique for symmetry reduction ⋮ Modeling with Metaconstraints and Semantic Typing of Variables ⋮ Improved Static Symmetry Breaking for SAT ⋮ SymChaff ⋮ Formula simplification via invariance detection by algebraically indexed types

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver