Differences

This shows you the differences between two versions of the page.

--- sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2010/05/03 11:06]
vkuncak
+++ sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Small Solutions for Quantifier-Free Presburger Arithmetic ======
-We next consider satisfiability of quantifier-free formulas of Presburger arithmetic (denoted QFPA).
-We have seen that, by existentially quantifying over all variables, this problem can be solved using [[QE for Presburger Arithmetic|quantifier elimination for Presburger Arithmetic]].
-However, this approach can be expensive.
-We next quote a result that allows us to reduce this problem to a polynomially sized SAT formula.  This result implies that the satisfiability of QFPA is in NP.  The problem is also NP-hard (why?), so it is NP-complete.
-QFPA is just PA without quantifiers:
-\[\begin{array}{l}
-    F ::= A \mid F_1 \land F_2 \mid \lnot F_1 \mid F_1 \lor F_2 \\
-    A ::= T_1 = T_2 \mid T_1 \le T_2 \mid (K|T) \\
-    T ::= K \mid T_1 + T_2 \mid K \cdot T \\
-    K ::= \ldots -2 \mid -1 \mid 0 \mid 1 \mid 2 \ldots
- \end{array}
-\]
-We also do not need divisibility constraints: $K|t$  is satisfiable iff ++| $t= K q$ is satisfiable, for $q$ fresh ++
-===== Integer Linear Ineqautions =====
-In matrix form, integer linear inequation is
-\[
-      A \vec x \leq \vec b
-\]
-where $A \vec x$ denotes matrix $A$ multiplied by vector $\vec x$.  When $A$ is $m \times n$ matrix, this denotes the system of inequations:
-\[
-    \bigwedge_{j=1}^m \sum_{i=1}^n a_{ij} x_i \le b_j
-\]
-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
-  * [[http://www.gnu.org/software/glpk/|GLPK tool]]
-  * [[wk>Integer Linear Programming]]
-===== Reduction of QFPA to Integer Linear Programming =====
-Each QFPA formula can be reduced to a disjunction of linear integer inequations.
-===== Theorem on Solution Bounds =====
-**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 linear programming and is given here:
-  * [[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 =====
-Note that coefficients in the $A,b$ of the disjuncts are polynomially bounded by coefficients in the QFPA from which they are obtained.
-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 =====
-We observed before that if we have bounded integers we can encode formula into SAT.
-===== Implementation =====
-In practice these bounds are not small enough to be useful.  More refined bounds exist for special cases:
-  * [[http://www.cs.cmu.edu/~uclid/|UCLID tool]]
-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)}}
-===== Extensions =====
-Models get bigger if we allow bitvector operations:
-  * {{sav08:pa_bitvectors.pdf|PABitvectors}}