Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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