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/09/24 15:23]
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 =====