LARA

Differences

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

Link to this comparison view

Both sides previous 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 [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 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 65: 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 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 =====