Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:40] vkuncak |
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2010/05/03 11:06] vkuncak |
||
|---|---|---|---|
| Line 18: | Line 18: | ||
| \] | \] | ||
| We also do not need divisibility constraints: $K|t$ is satisfiable iff ++| $t= K q$ is satisfiable, for $q$ fresh ++ | We also do not need divisibility constraints: $K|t$ is satisfiable iff ++| $t= K q$ is satisfiable, for $q$ fresh ++ | ||
| + | |||
| Line 32: | Line 33: | ||
| Note that equations can be expressed as well by stating two inequations. | Note that equations can be expressed as well by stating two inequations. | ||
| - | Conversely, if variables range over non-negative integers, then we can rewrite $A x \le b$ as $Ax + u = b$. | + | Conversely, **if** variables range over non-negative integers, then we can rewrite $A x \le b$ as $Ax + u = b$. |
| Relatively well studied problem | Relatively well studied problem | ||
| Line 87: | Line 88: | ||
| But other solvers use solutions over rational numbers to help find solutions over integers, using techniques from integer linear programming. | But other solvers use solutions over rational numbers to help find solutions over integers, using techniques from integer linear programming. | ||
| * {{projects:simplexdplltreport.pdf|Integrating Simplex with DPLL(T)}} | * {{projects:simplexdplltreport.pdf|Integrating Simplex with DPLL(T)}} | ||
| + | |||
| + | ===== Extensions ===== | ||
| + | |||
| + | Models get bigger if we allow bitvector operations: | ||
| + | * {{sav08:pa_bitvectors.pdf|PABitvectors}} | ||