• English only

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] (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 =====