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 [2009/04/23 10:40]
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.
  
-Conversely, if variables range over non-negative integers, then we can rewrite $A x \le b$ as $Ax + u = b$.+Conversely, ​**if** variables range over non-negative integers, then we can rewrite $A x \le b$ as $Ax + u = b$.
  
 Relatively well studied problem Relatively well studied problem
Line 41: 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 57: 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 76: 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 =====
Line 87: Line 76:
 But other solvers use solutions over rational numbers to help find solutions over integers, using techniques from integer linear programming. But other solvers use solutions over rational numbers to help find solutions over integers, using techniques from integer linear programming.
   * {{projects:​simplexdplltreport.pdf|Integrating Simplex with DPLL(T)}}   * {{projects:​simplexdplltreport.pdf|Integrating Simplex with DPLL(T)}}
 +
 +===== Extensions =====
 +
 +Models get bigger if we allow bitvector operations:
 +  * {{sav08:​pa_bitvectors.pdf|PABitvectors}}