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:35] vkuncak |
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:40] 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 ++ | ||
+ | |||
===== Integer Linear Ineqautions ===== | ===== Integer Linear Ineqautions ===== | ||
Line 30: | Line 31: | ||
\] | \] | ||
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$. | ||
Relatively well studied problem | Relatively well studied problem | ||
Line 38: | 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 46: | Line 53: | ||
**Theorem (Papadimitriou):** Let $A$ be $m \times n$ matrix and $b$ an $m$-vector, both with entries from $\{0,\pm 1,\ldots, \pm a\}$. Then if $Ax = b$ has a solution in $x \in \mathbb{N}^n$, it also has a solution in $\{0,1,\ldots,n(ma)^{2m+1}\}^n$. | **Theorem (Papadimitriou):** Let $A$ be $m \times n$ matrix and $b$ an $m$-vector, both with entries from $\{0,\pm 1,\ldots, \pm a\}$. Then if $Ax = b$ has a solution in $x \in \mathbb{N}^n$, it also has a solution in $\{0,1,\ldots,n(ma)^{2m+1}\}^n$. | ||
- | Proof uses duality in integer 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 | ||
+ | |||
===== Extending Theorem to QFPA ===== | ===== Extending Theorem to QFPA ===== | ||
Line 54: | 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 ===== |