New techniques for linear arithmetic: cubes and equalities

DOI10.1007/S10703-017-0278-7MaRDI QIDQ1688532zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Martin Bromberger, Christoph Weidenbach

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://hal.inria.fr/hal-01656397/file/paper.pdf

zbMATH Keywords

SMTinteger arithmeticcombination of theoriesconstraint solvinglinear arithmeticequalities

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

• Fast cube tests for LIA constraint solving
• Equality detection for linear arithmetic constraints
• Solving Sparse Linear Constraints
• SAT modulo linear arithmetic for solving polynomial constraints
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers

Cites work

• scientific article; zbMATH DE number 4006346 (Why is no real title available?)
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 1302474 (Why is no real title available?)
• scientific article; zbMATH DE number 2107836 (Why is no real title available?)
• scientific article; zbMATH DE number 3209723 (Why is no real title available?)
• scientific article; zbMATH DE number 3089575 (Why is no real title available?)
• A new polynomial-time algorithm for linear programming
• A practical approach to satisfiability modulo linear integer arithmetic
• A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
• Applying Linear Quantifier Elimination
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Cutting to the chase.
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• Efficient Heuristic Procedures for Integer Linear Programming with an Interior
• Fast cube tests for LIA constraint solving
• Identifying Redundant Constraints and Implicit Equalities in Systems of Linear Constraints
• Linear integer arithmetic revisited
• On the complexity of integer programming
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Standard forms for rational linear arithmetic in constraint logic programming.
• The MathSAT5 SMT solver

Cited in

(6)

• A New Algorithm for Long Integer Cube Computation with Some Insight into Higher Powers
• On Incremental Pre-processing for SMT
• Solving Sparse Linear Constraints
• SPASS-SATT. A CDCL(LA) solver
• Fast cube tests for LIA constraint solving
• A reduction from unbounded linear mixed arithmetic problems into bounded problems

Describes a project that uses

Uses Software

• Yices
• z3
• CVC4
• MathSAT5

This page was built for publication: New techniques for linear arithmetic: cubes and equalities

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