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:39] vkuncak |
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:40] vkuncak |
||
---|---|---|---|
Line 41: | Line 41: | ||
Each QFPA formula can be reduced to a disjunction of linear integer inequations. | Each QFPA formula can be reduced to a disjunction of linear integer inequations. | ||
+ | |||
Line 63: | Line 64: | ||
* $m$ is number of constraints | * $m$ is number of constraints | ||
* $n$ is number of variables | * $n$ is number of variables | ||
- | We obtain a **polynomial-time** reduction from quantifier-free Presburger arithmetic to SAT. | + | |
===== 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 ===== |