Propagation based local search for bit-precise reasoning

DOI10.1007/s10703-017-0295-6zbMath1377.68134DBLPjournals/fmsd/NiemetzPB17OpenAlexW2764059762WikidataQ59065410 ScholiaQ59065410MaRDI QIDQ1688546

Aina Niemetz, Armin Biere, Mathias Preiner

Publication date: 8 January 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0295-6

zbMATH Keywords

local searchsatisfiability modulo theoriesbit-vector reasoning

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (5)

Propagation based local search for bit-precise reasoning ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ Wombit: a portfolio bit-vector solver using word-level propagation

Uses Software

• Yices
• z3
• SATzilla
• Plingeling
• OpenSMT
• CVC4
• MathSAT5
• Treengeling
• Splatz
• Lingeling
• YalSAT
• STP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Propagation based local search for bit-precise reasoning
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Deciding Bit-Vector Formulas with mcSAT
• Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break
• A Model-Constructing Satisfiability Calculus
• Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
• An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic Circuits
• Constraint-Based Verification
• The MathSAT5 SMT Solver
• A Decision Procedure for Bit-Vectors and Arrays

This page was built for publication: Propagation based local search for bit-precise reasoning