Cutting to the Chase Solving Linear Integer Arithmetic
From MaRDI portal
Publication:5200035
DOI10.1007/978-3-642-22438-6_26zbMath1314.90054OpenAlexW113043827MaRDI 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
Integer programming (90C10) Linear programming (90C05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Semantically-guided goal-sensitive reasoning: model representation, Deciding floating-point logic with abstract conflict driven clause learning, The Strategy Challenge in SMT Solving, 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
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