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
Next revision Both sides next revision
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:39]
vkuncak
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:40]
vkuncak
Line 41: Line 41:
  
 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.
 +
  
  
Line 63: Line 64:
   * $m$ is number of constraints   * $m$ is number of constraints
   * $n$ is number of variables   * $n$ is number of variables
-We obtain a **polynomial-time** reduction from quantifier-free Presburger arithmetic to SAT.+
  
 ===== Extending Theorem to QFPA ===== ===== Extending Theorem to QFPA =====
Line 70: Line 71:
  
 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 =====