Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
From MaRDI portal
Publication:2818024
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
Related Items
Uses Software
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