New techniques for linear arithmetic: cubes and equalities

DOI10.1007/s10703-017-0278-7zbMath1377.68128OpenAlexW2613671682WikidataQ59602500 ScholiaQ59602500MaRDI QIDQ1688532

Christoph Weidenbach, Martin Bromberger

Publication date: 8 January 2018

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

Full work available at URL: https://hal.inria.fr/hal-01656397/file/paper.pdf

zbMATH Keywords

linear arithmeticequalitiesconstraint solvinginteger arithmeticSMTcombination of theories

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 (1)

SPASS-SATT. A CDCL(LA) solver

Uses Software

• Yices
• z3
• CVC4
• MathSAT5

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new polynomial-time algorithm for linear programming
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• Standard forms for rational linear arithmetic in constraint logic programming.
• Cutting to the chase.
• Fast Cube Tests for LIA Constraint Solving
• A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
• Identifying Redundant Constraints and Implicit Equalities in Systems of Linear Constraints
• Applying Linear Quantifier Elimination
• Linear Integer Arithmetic Revisited
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• On the complexity of integer programming
• The MathSAT5 SMT Solver
• Efficient Heuristic Procedures for Integer Linear Programming with an Interior

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