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 [2012/05/21 09:57]
vkuncak
Line 18: Line 18:
 \] \]
 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 =====
Line 32: Line 31:
 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 64: Line 56:
   * $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}}