Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 =====
 
sav08/small_solutions_for_quantifier-free_presburger_arithmetic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice