Name
Abstract | ||
|---|---|---|
This paper describes an implementation and experimental evaluation of a recently introduced bound propagation method for solving systems of linear inequalities over the reals and rationals. The implementation is part of the first-order theorem prover Vampire. The input problems are systems of linear inequalities over reals or rationals. Their satisfiability is checked by assigning values to the variables of the system and propagating the bounds on these variables. To make the method efficient, we use various strategies for representing numbers, selecting variable orderings, choosing variable values and propagating bounds. We evaluate our implementation on a large number of examples and compare it with state-of-the-art SMT solvers. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/SYNASC.2013.30 | SYNASC |
Keywords | Field | DocType |
linear real arithmetic, bound propagation method, conflict resolution, arithmetic reasoning, linear arithmetic,conflict resolution | Automated reasoning,Discrete mathematics,Rational number,Algebra,Computer science,Automated theorem proving,Satisfiability,Formal methods,Linear inequality,Vampire,Information and Computer Science | Conference |
ISSN | Citations | PageRank |
2470-8801 | 1 | 0.37 |
References | Authors | |
12 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ioan Dragan | 1 | 1 | 0.37 |
| Konstantin Korovin | 2 | 288 | 20.64 |
| Laura Kovács | 3 | 494 | 36.97 |
| Andrei Voronkov | 4 | 2670 | 225.46 |