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 70: Line 62:
  
 We therefore obtain a "small model theorem":​ if there are solutions, there are "​small"​ solutions. ​ In this case, small means "​polynomially many bits". We therefore obtain a "small model theorem":​ if there are solutions, there are "​small"​ solutions. ​ In this case, small means "​polynomially many bits".
 +
 +We obtain a **polynomial-time reduction** from **quantifier-free Presburger arithmetic** to **SAT**.
  
 ===== 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 84: 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}}