• English only

# Differences

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

sav08:homework08 [2008/09/15 15:56]
vkuncak
sav08:homework08 [2015/04/21 17:30] (current)
Line 6: Line 6:

Consider a language $L$ that contains some terms whose values are interpreted as integers (to be concrete, the language of Presburger arithmetic, or the BAPA language). ​ Consider formulas interpreted over some theory $T$ that has an effective quantifier elimination algorithm $qe$.  Then show that there is an algorithm for solving optimization problems such as Consider a language $L$ that contains some terms whose values are interpreted as integers (to be concrete, the language of Presburger arithmetic, or the BAPA language). ​ Consider formulas interpreted over some theory $T$ that has an effective quantifier elimination algorithm $qe$.  Then show that there is an algorithm for solving optimization problems such as
-$+\begin{equation*} \max \{ t(x_1,​\ldots,​x_n) \mid F(x_1,​\ldots,​x_n) \} \max \{ t(x_1,​\ldots,​x_n) \mid F(x_1,​\ldots,​x_n) \} -$+\end{equation*}
where $t(x_1,​\ldots,​x_n)$ denotes a term of the language whose value is an integer, and where $F(x_1,​\ldots,​x_n)$ is an arbitrary formula in language $L$.  The meaning of //​solution//​ for constraints is the following. ​ Let $S = \{ t(x_1,​\ldots,​x_n) \mid F(x_1,​\ldots,​x_n) \}$.  Then the solution is an element $y^*$ of $\mathbb{Z} \cup \{-\infty,​+\ifnty\}$ such that where $t(x_1,​\ldots,​x_n)$ denotes a term of the language whose value is an integer, and where $F(x_1,​\ldots,​x_n)$ is an arbitrary formula in language $L$.  The meaning of //​solution//​ for constraints is the following. ​ Let $S = \{ t(x_1,​\ldots,​x_n) \mid F(x_1,​\ldots,​x_n) \}$.  Then the solution is an element $y^*$ of $\mathbb{Z} \cup \{-\infty,​+\ifnty\}$ such that
* if $y^* = -\infty$ then $S=\emptyset$   * if $y^* = -\infty$ then $S=\emptyset$
Line 15: Line 15:

Your answer will show, given $qe$, how to solve optimization problems for any theory that has quantifier elimination. ​ For example, taking Presburger arithmetic, we can solve linear optimization problems such as Your answer will show, given $qe$, how to solve optimization problems for any theory that has quantifier elimination. ​ For example, taking Presburger arithmetic, we can solve linear optimization problems such as
-$+\begin{equation*} \max \{ 2x + 3y \mid x + y \le 10 \land (7 \mid y+1) \} \max \{ 2x + 3y \mid x + y \le 10 \land (7 \mid y+1) \} -$+\end{equation*}
Taking BAPA as a theory with QE, we can solve problems such as finding Taking BAPA as a theory with QE, we can solve problems such as finding
-$+\begin{equation*} \max \{ |A|+3|B|+|C|\ \mid\ C \subseteq A \cup B \land |A| \le |B| \land |C| \le 100 \} \max \{ |A|+3|B|+|C|\ \mid\ C \subseteq A \cup B \land |A| \le |B| \land |C| \le 100 \} -$+\end{equation*}
By generalizing the objective function to reals, we can solve non-linear but polynomial optimization problems using quantifier elimination over reals. By generalizing the objective function to reals, we can solve non-linear but polynomial optimization problems using quantifier elimination over reals.

Line 28: Line 28:

Consider language ${\cal L} = \{ {\le} \}$ and the theory $T = Conseq(T_0)$ where $T_0$ is the set of following axioms (axioms of linear order): Consider language ${\cal L} = \{ {\le} \}$ and the theory $T = Conseq(T_0)$ where $T_0$ is the set of following axioms (axioms of linear order):
-$+\begin{equation*} \begin{array}{l} \begin{array}{l} \forall x.\forall y. x \le y \land y \le x \rightarrow x=y \\ \forall x.\forall y. x \le y \land y \le x \rightarrow x=y \\ Line 34: Line 34: \forall x.\forall y. x \le y \lor y \le x \forall x.\forall y. x \le y \lor y \le x \end{array} \end{array} -$+\end{equation*}
Observe that these axioms are true in the structures of integers, natural numbers, and rational numbers, where $\le$ is interpreted as the usual less-than-equal relation on such numbers. Observe that these axioms are true in the structures of integers, natural numbers, and rational numbers, where $\le$ is interpreted as the usual less-than-equal relation on such numbers.

Line 42: Line 42: