Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
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] (current) |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| QFPA is just PA without quantifiers: | QFPA is just PA without quantifiers: | ||
| - | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
| F ::= A \mid F_1 \land F_2 \mid \lnot F_1 \mid F_1 \lor F_2 \\ | 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) \\ | A ::= T_1 = T_2 \mid T_1 \le T_2 \mid (K|T) \\ | ||
| Line 16: | Line 16: | ||
| K ::= \ldots -2 \mid -1 \mid 0 \mid 1 \mid 2 \ldots | K ::= \ldots -2 \mid -1 \mid 0 \mid 1 \mid 2 \ldots | ||
| \end{array} | \end{array} | ||
| - | \] | + | \end{equation*} |
| 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 ===== | ||
| In matrix form, integer linear inequation is | In matrix form, integer linear inequation is | ||
| - | \[ | + | \begin{equation*} |
| A \vec x \leq \vec b | A \vec x \leq \vec b | ||
| - | \] | + | \end{equation*} |
| 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: | 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: | ||
| - | \[ | + | \begin{equation*} |
| \bigwedge_{j=1}^m \sum_{i=1}^n a_{ij} x_i \le b_j | \bigwedge_{j=1}^m \sum_{i=1}^n a_{ij} x_i \le b_j | ||
| - | \] | + | \end{equation*} |
| Note that equations can be expressed as well by stating two inequations. | Note that equations can be expressed as well by stating two inequations. | ||
| Line 42: | Line 40: | ||
| 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. | ||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| ===== Theorem on Solution Bounds ===== | ===== Theorem on Solution Bounds ===== | ||
| Line 58: | Line 49: | ||
| Consequence: it suffices to search for those solutions whose variables denote integers with the number of bits bounded by: | Consequence: it suffices to search for those solutions whose variables denote integers with the number of bits bounded by: | ||
| - | \[ | + | \begin{equation*} |
| \log (n(ma)^{2m+1}) = (2m+1) (\log(ma)) + \log n | \log (n(ma)^{2m+1}) = (2m+1) (\log(ma)) + \log n | ||
| - | \] | + | \end{equation*} |
| here | here | ||
| * $a$ is the maximum of values of integers occuring in the problem | * $a$ is the maximum of values of integers occuring in the problem | ||
| * $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 77: | Line 67: | ||
| ===== Reduction to SAT ===== | ===== Reduction to SAT ===== | ||
| - | We observed before that if we have bounded integers we can encode formula into SAT. | + | Observe that if we have bounded integers we can encode the formula into SAT. |
| - | + | ||
| ===== Implementation ===== | ===== Implementation ===== | ||