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 [2009/09/24 15:23] vkuncak |
||
|---|---|---|---|
| Line 64: | Line 64: | ||
| * $m$ is number of constraints | * $m$ is number of constraints | ||
| * $n$ is number of variables | * $n$ is number of variables | ||
| + | |||
| ===== Extending Theorem to QFPA ===== | ===== Extending Theorem to QFPA ===== | ||
| Line 70: | Line 71: | ||
| We therefore obtain a "small model theorem": if there are solutions, there are "small" solutions. In this case, small means "polynomially many bits". | We therefore obtain a "small model theorem": if there are solutions, there are "small" solutions. In this case, small means "polynomially many bits". | ||
| + | |||
| + | We obtain a **polynomial-time reduction** from **quantifier-free Presburger arithmetic** to **SAT**. | ||
| ===== Reduction to SAT ===== | ===== Reduction to SAT ===== | ||
| Line 84: | Line 87: | ||
| 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}} | ||