Exploiting Symmetry in SMT Problems

DOI10.1007/978-3-642-22438-6_18zbMath1341.68187OpenAlexW156574570MaRDI QIDQ5200027

Pascal Fontaine, Stephan Merz, David Déharbe, Bruno Woltzenlogel Paleo

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_18

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ Search-Space Partitioning for Parallelizing SMT Solvers ⋮ Automated reasoning with restricted intensional sets ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Symmetric blocking ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Refutation-based synthesis in SMT ⋮ Exploiting Symmetry in SMT Problems ⋮ Scalable fine-grained proofs for formula processing ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• MiniSat
• Darwin
• E-Darvin
• veriT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Short proofs for tricky formulas
• Computing finite models by reduction to function-free clause logic
• The intractability of resolution
• The complexity of resolution with generalized symmetry rules
• A Powerful Technique to Eliminate Isomorphism in Finite Model Search
• Polynomial size proofs of the propositional pigeonhole principle
• Exploiting Symmetry in SMT Problems
• Computer Aided Verification