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:36] vkuncak |
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:39] 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 52: | Line 54: | ||
| Proof uses duality in integer linear programming and is given here: | Proof uses duality in integer linear programming and is given here: | ||
| * [[http://doi.acm.org/10.1145/322276.322287|On the complexity of integer programming]], {{:papadimitriou81complexityintegerprogramming.pdf|pdf}} | * [[http://doi.acm.org/10.1145/322276.322287|On the complexity of integer programming]], {{:papadimitriou81complexityintegerprogramming.pdf|pdf}} | ||
| + | |||
| + | Consequence: it suffices to search for those solutions whose variables denote integers with the number of bits bounded by: | ||
| + | \[ | ||
| + | \log (n(ma)^{2m+1}) = (2m+1) (\log(ma)) + \log n | ||
| + | \] | ||
| + | here | ||
| + | * $a$ is the maximum of values of integers occuring in the problem | ||
| + | * $m$ is number of constraints | ||
| + | * $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 ===== | ||