A practical approach to satisfiability modulo linear integer arithmetic

zbMATH Open1331.68207MaRDI QIDQ2786906FDOQ2786906

Alberto Griggio

Publication date: 23 February 2016

Published in: Journal of Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)

zbMATH Keywords

SMTdecision procedureslinear integer arithmetic

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Boolean programming (90C09)

Cited In (20)

• Fast Cube Tests for LIA Constraint Solving
• Minimal counterexamples for linear-time probabilistic verification
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Title not available (Why is that?)
• Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
• Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• SPASS-SATT. A CDCL(LA) solver
• Optimization Modulo Theories with Linear Rational Costs
• Satisfiability modulo transcendental functions via incremental linearization
• A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
• Solving Nonlinear Integer Arithmetic with MCSAT
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Linear Integer Arithmetic Revisited
• New techniques for linear arithmetic: cubes and equalities
• Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
• A complete and terminating approach to linear integer solving
• From simplification to a partial theory solver for non-linear real polynomial constraints
• Improving IntSat by expressing disjunctions of bounds as linear constraints

This page was built for publication: A practical approach to satisfiability modulo linear integer arithmetic

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