\texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
From MaRDI portal
Publication:1037644
Recommendations
Cites work
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Accelerating bounded model checking of safety properties
- An accurate and scalable collaborative recommender
- BerkMin: A fast and robust SAT-solver
- Dynamic Lex Constraints
- Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
- General Symmetry Breaking Constraints
- Generic SBDD using computational group theory
- scientific article; zbMATH DE number 3976991 (Why is no real title available?)
- scientific article; zbMATH DE number 477971 (Why is no real title available?)
- scientific article; zbMATH DE number 2084698 (Why is no real title available?)
- scientific article; zbMATH DE number 2084699 (Why is no real title available?)
- scientific article; zbMATH DE number 1926658 (Why is no real title available?)
- scientific article; zbMATH DE number 2243370 (Why is no real title available?)
- scientific article; zbMATH DE number 2243377 (Why is no real title available?)
- Lower bounds for resolution and cutting plane proofs and monotone computations
- On the complexity of cutting-plane proofs
- Resolution cannot polynomially simulate compressed-BFS
- Resolution lower bounds for the weak pigeonhole principle
- Short proofs for tricky formulas
- STRIPS: A new approach to the application of theorem proving to problem solving
- The intractability of resolution
- The symmetry rule in propositional logic
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
Cited in
(21)- SymChaff
- Symmetries of quantified Boolean formulas
- Symmetric explanation learning: effective dynamic symmetry handling for SAT
- Formula simplification via invariance detection by algebraically indexed types
- CDCLSym: introducing effective symmetry breaking in SAT solving
- How to find symmetries hidden in combinatorial problems
- Modeling with metaconstraints and semantic typing of variables
- Improved static symmetry breaking for SAT
- Speeding up SAT solver by exploring CNF symmetries: Revisited
- Expressing symmetry breaking in DRAT proofs
- Exploiting symmetry in SMT problems
- Symmetry breaking for pseudo-Boolean formulas
- Theory and Applications of Satisfiability Testing
- Recent Advances in Constraints
- An adaptive prefix-assignment technique for symmetry reduction
- An adaptive prefix-assignment technique for symmetry reduction
- Exploiting symmetries within constraint satisfaction search
- Certified dominance and symmetry breaking for combinatorial optimisation
- Satsuma: structure-based symmetry breaking in SAT
- Breaking the symmetries of indistinguishable objects
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
Describes a project that uses
Uses Software
This page was built for publication: \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1037644)
