Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:homework08 [2008/09/17 23:03] 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. | ||