Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers

DOI10.1007/978-3-319-40970-2_19zbMath1475.68439OpenAlexW2460341801MaRDI QIDQ2818024

Armando Solar-Lezama, Jeevana Priya Inala, Rohit Singh

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: http://hdl.handle.net/1721.1/106008

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers

Uses Software

• Beaver
• Boolector
• MiniSat
• Paramils
• Yices
• z3
• Chaff
• StarExec
• CVC4
• Proteus
• Velev SAT Benchmarks
• Jalangi
• SMAC
• OpenTuner

Cites Work

• Unnamed Item
• Unnamed Item
• The configurable SAT solver challenge (CSSC)
• Generalising unit-refutation completeness and SLUR via nested input resolution
• Automatic Generation of Propagation Complete SAT Encodings
• Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
• Knowledge Compilation with Empowerment
• Generalising and Unifying SLUR and Unit-Refutation Completeness
• GAC Via Unit Propagation
• Encodings of the Sequence Constraint
• Ranking Function Synthesis for Bit-Vector Relations
• Constraint-Based Invariant Inference over Predicate Abstraction
• Applying Logic Synthesis for Speeding Up SAT
• ParamILS: An Automatic Algorithm Configuration Framework
• Clause Elimination Procedures for CNF Formulas
• From program verification to program synthesis
• A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification