Improved static symmetry breaking for SAT

DOI10.1007/978-3-319-40970-2_8MaRDI QIDQ2818005zbMATH OpenOpenAlexFDO

Authors Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, Marc Denecker

Publication date 5 September 2016

Published in Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL https://lirias.kuleuven.be/handle/123456789/542704

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• CDCLSym: introducing effective symmetry breaking in SAT solving
• Expressing symmetry breaking in DRAT proofs
• \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
• Symmetry Breaking for Maximum Satisfiability
• Symmetry and Satisfiability: An Update

Cites work

• scientific article; zbMATH DE number 1849958 (Why is no real title available?)
• Dynamic Symmetry Breaking by Simulating Zykov Contraction
• Generating effective symmetry-breaking predicates for search problems
• Hard examples for resolution
• Practical graph isomorphism. II.
• Symmetry and Satisfiability: An Update
• The intractability of resolution
• Theory and Applications of Satisfiability Testing
• \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver

Cited in

(26)

• Speeding up SAT solver by exploring CNF symmetries: Revisited
• Preprocessing of propagation redundant clauses
• Certified dominance and symmetry breaking for combinatorial optimisation
• SAT modulo symmetries for graph generation and enumeration
• Breaking instance-independent symmetries in exact graph coloring
• Preprocessing of propagation redundant clauses
• Exploiting symmetry in SMT problems
• CDCLSym: introducing effective symmetry breaking in SAT solving
• An adaptive prefix-assignment technique for symmetry reduction
• On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
• Automated mathematical discovery and verification: minimizing pentagons in the plane
• How constraint programming can help chemists to generate benzenoid structures and assess the local aromaticity of benzenoids
• Symmetry Breaking for Maximum Satisfiability
• SAT competition 2020
• Strong extension-free proof systems
• Efficient symmetry breaking for SAT-based minimum DFA inference
• \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
• Symmetric explanation learning: effective dynamic symmetry handling for SAT
• Formula simplification via invariance detection by algebraically indexed types
• Reducing symmetries to generate easier SAT instances
• Symmetry breaking for pseudo-Boolean formulas
• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 7455719 (Why is no real title available?)
• A study of symmetry breaking predicates and model counting
• The complexity of symmetry-breaking formulas
• Expressing symmetry breaking in DRAT proofs

Describes a project that uses

Uses Software

• GAP
• MiniSat
• nauty
• SymChaff
• Traces
• Shatter
• bliss

This page was built for publication: Improved static symmetry breaking for SAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2818005)