Differences

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

--- sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:36]
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.
@@ Line 52: / Line 55: @@
 Proof uses duality in integer linear programming and is given here:
   * [[http://doi.acm.org/10.1145/322276.322287|On the complexity of integer programming]], {{:papadimitriou81complexityintegerprogramming.pdf|pdf}}
+Consequence: it suffices to search for those solutions whose variables denote integers with the number of bits bounded by:
+\[
+   \log (n(ma)^{2m+1}) = (2m+1) (\log(ma)) + \log n
+\]
+here
+  * $a$ is the maximum of values of integers occuring in the problem
+  * $m$ is number of constraints
+  * $n$ is number of variables
 ===== Extending Theorem to QFPA =====
@@ Line 58: / 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 obtain a **polynomial-time reduction** from **quantifier-free Presburger arithmetic** to **SAT**.
 ===== Reduction to SAT =====