LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2012/05/21 09:57]
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 ++
  
Line 22: Line 22:
  
 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 49: 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