Fast Cube Tests for LIA Constraint Solving

DOI10.1007/978-3-319-40229-1_9zbMath1475.68337OpenAlexW2491318681MaRDI QIDQ2817914

Christoph Weidenbach, Martin Bromberger

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01403200/file/IJCAR2016.pdf

zbMATH Keywords

linear arithmeticconstraint solvinginteger arithmeticSMT

Mathematics Subject Classification ID

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

Related Items (5)

Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ New techniques for linear arithmetic: cubes and equalities ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ SPASS-SATT. A CDCL(LA) solver ⋮ An efficient subsumption test pipeline for BS(LRA) clauses

Uses Software

• Yices
• z3
• CVC4
• MathSAT5

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new polynomial-time algorithm for linear programming
• Cutting to the chase.
• A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
• 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
• 50 Years of Integer Programming 1958-2008
• 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: Fast Cube Tests for LIA Constraint Solving