Sharpening constraint programming approaches for bit-vector theory
DOI10.1007/978-3-319-59776-8_1zbMATH Open1489.68249OpenAlexW2619890504MaRDI QIDQ2011567FDOQ2011567
Authors: Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin 
Publication date: 4 August 2017
Full work available at URL: https://hal-cea.archives-ouvertes.fr/cea-01795779/file/bv-cpaior.pdf
Recommendations
- Towards satisfiability modulo parametric bit-vectors
- On solving quantified bit-vector constraints using invertibility conditions
- An alternative to SAT-based approaches for bit-vectors
- Bit-vector algorithms for binary constraint satisfaction and subgraph isomorphism
- An alternative eager encoding of the all-different constraint over bit-vectors
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Efficiently solving quantified bit-vector formulas
- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Abstraction of bit-vector operations for BDD-based SMT solvers
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Theory and Applications of Satisfiability Testing
- The MathSAT5 SMT solver
- A Decision Procedure for Bit-Vectors and Arrays
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Lazy Abstraction with Interpolants
- Boosting search with variable elimination in constraint optimization and constraint satisfaction problems
- Lazy abstraction
- Tools and Algorithms for the Construction and Analysis of Systems
- Solving quantified verification conditions using satisfiability modulo theories
- Title not available (Why is that?)
- Deciding Bit-Vector Arithmetic with Abstraction
- Social processes and proofs of theorems and programs
- Explaining Time-Table-Edge-Finding Propagation for the Cumulative Resource Constraint
- A constraint solver based on abstract domains
- A bit-vector solver with word-level propagation
- Taking satisfiability to the next level with Z3 (abstract)
- An alternative to SAT-based approaches for bit-vectors
Cited In (12)
- On the usefulness of linear modular arithmetic in constraint programming
- Wombit: a portfolio bit-vector solver using word-level propagation
- Exploiting binary floating-point representations for constraint propagation
- An alternative to SAT-based approaches for bit-vectors
- A bit-vector solver with word-level propagation
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Bit-vector algorithms for binary constraint satisfaction and subgraph isomorphism
- Deciding Bit-Vector Formulas with mcSAT
- A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints
- Improved Bit-Stuffing Bounds on Two-Dimensional Constraints
- Constraint satisfaction through GBP-guided deliberate bit flipping
- A bitopological view on cocompact extensions
Uses Software
This page was built for publication: Sharpening constraint programming approaches for bit-vector theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2011567)
