Propagation based local search for bit-precise reasoning

DOI10.1007/S10703-017-0295-6MaRDI QIDQ1688546zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Aina Niemetz, Mathias Preiner, Armin Biere

Publication date 8 January 2018

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

Copyright license Creative Commons Attribution 4.0 International

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

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

Recommendations

• Precise and complete propagation based local search for satisfiability modulo theories
• Local-search techniques for propositional logic extended with cardinality constraints
• Approximation of Boolean functions by local search
• Improved local search for circuit satisfiability
• Complete Boolean satisfiability solving algorithms based on local search
• Using stochastic local search to solve quantified Boolean formulae
• Efficient local search for pseudo Boolean optimization
• scientific article; zbMATH DE number 1538058

Cites work

• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• scientific article; zbMATH DE number 1033831 (Why is no real title available?)
• A Decision Procedure for Bit-Vectors and Arrays
• A model-constructing satisfiability calculus
• An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic Circuits
• Choosing probability distributions for stochastic local search and the role of make versus break
• Constraint-Based Verification
• Deciding Bit-Vector Formulas with mcSAT
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Propagation based local search for bit-precise reasoning
• SATzilla: portfolio-based algorithm selection for SAT
• Stochastic local search for SMT: combining theory solvers with WalkSAT
• The MathSAT5 SMT solver

Cited in

(10)

• Wombit: a portfolio bit-vector solver using word-level propagation
• Exploiting binary floating-point representations for constraint propagation
• A bit-vector solver with word-level propagation
• Abstraction of bit-vector operations for BDD-based SMT solvers
• On solving quantified bit-vector constraints using invertibility conditions
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Optimization modulo the theories of signed bit-vectors and floating-point numbers
• Propagation based local search for bit-precise reasoning
• Precise and complete propagation based local search for satisfiability modulo theories
• Bitwuzla

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1688546)