Cutting to the Chase Solving Linear Integer Arithmetic

DOI10.1007/978-3-642-22438-6_26zbMath1314.90054MaRDI QIDQ5200035

Leonardo de Moura, Dejan Jovanović

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_26

Mathematics Subject Classification ID

90C10: Integer programming

90C05: Linear programming

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Related Items

The Strategy Challenge in SMT Solving, Semantically-guided goal-sensitive reasoning: model representation, Deciding floating-point logic with abstract conflict driven clause learning, Conflict-driven satisfiability for theory combination: transition system and completeness, SPASS-SATT. A CDCL(LA) solver, A complete and terminating approach to linear integer solving, Generating invariants for non-linear hybrid systems

Uses Software

• SCIP
• MIPLIB
• z3
• Chaff
• Sat4j
• MIPLIB2003

Cites Work

• Unnamed Item
• Unnamed Item
• SCIP: solving constraint integer programs
• MIPLIB 2003
• Edmonds polytopes and a hierarchy of combinatorial problems
• Conflict Resolution
• Outline of an algorithm for integer solutions to linear programs
• Solving SAT and SAT Modulo Theories
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Natural Domain SMT: A Preliminary Assessment
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Generalizing DPLL to Richer Logics
• GRASP: a search algorithm for propositional satisfiability
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving