Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
verfasst von : Isil Dillig, Thomas Dillig, Alex Aiken
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We propose a novel, sound, and complete Simplex-based algorithm for solving linear inequalities over integers. Our algorithm, which can be viewed as a semantic generalization of the
branch-and-bound
technique, systematically discovers and excludes entire subspaces of the solution space containing no integer points. Our main insight is that by focusing on the
defining constraints
of a vertex, we can compute a
proof of unsatisfiability
for the intersection of the defining constraints and use this proof to systematically exclude subspaces of the feasible region with no integer points. We show experimentally that our technique significantly outperforms the top four competitors in the QF-LIA category of the SMT-COMP ’08 when solving linear inequalities over integers.