Deciding Disjunctive Linear Arithmetic with SAT
| dc.creator | Strichman, Ofer | |
| dc.date | 2004-02-01 | |
| dc.date.accessioned | 2026-07-07T03:20:51Z | |
| dc.date.available | 2026-07-07T03:20:51Z | |
| dc.description | Disjunctive Linear Arithmetic (DLA) is a major decidable theory that is supported by almost all existing theorem provers. The theory consists of Boolean combinations of predicates of the form $Σ_{j=1}^{n}a_j\cdot x_j \le b$, where the coefficients $a_j$, the bound $b$ and the variables $x_1 >... x_n$ are of type Real ($\mathbb{R}$). We show a reduction to propositional logic from disjunctive linear arithmetic based on Fourier-Motzkin elimination. While the complexity of this procedure is not better than competing techniques, it has practical advantages in solving verification problems. It also promotes the option of deciding a combination of theories by reducing them to this logic. Results from experiments show that this method has a strong advantage over existing techniques when there are many disjunctions in the formula. | |
| dc.identifier | https://arxiv.org/abs/cs/0402002 | |
| dc.identifier | http://arxiv.org/abs/cs/0402002 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/31979 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | B.1.4 | |
| dc.title | Deciding Disjunctive Linear Arithmetic with SAT | |
| dc.type | text |