• 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) Both sides previous revision Previous revision 2008/09/17 23:03 vkuncak 2008/09/15 15:56 vkuncak 2008/09/15 15:22 vkuncak 2008/09/15 15:06 vkuncak 2008/09/15 15:05 vkuncak 2008/09/15 15:03 vkuncak 2008/09/15 14:57 vkuncak 2008/09/14 00:12 vkuncak 2008/09/13 23:59 vkuncak 2008/04/24 13:36 vkuncak 2008/04/24 13:33 piskac 2008/04/23 21:09 vkuncak 2008/04/23 21:09 vkuncak 2008/04/23 18:23 vkuncak 2008/04/23 18:05 vkuncak 2008/04/23 17:55 vkuncak 2008/04/17 13:16 vkuncak 2008/04/17 13:15 vkuncak 2008/04/17 13:14 vkuncak 2008/04/16 18:19 vkuncak 2008/04/16 18:18 vkuncak 2008/04/16 17:21 vkuncak 2008/04/16 17:20 vkuncak 2008/04/16 17:15 vkuncak 2008/04/16 17:11 vkuncak 2008/04/16 17:10 vkuncak 2008/04/16 17:10 vkuncak Next revision Previous revision 2008/09/17 23:03 vkuncak 2008/09/15 15:56 vkuncak 2008/09/15 15:22 vkuncak 2008/09/15 15:06 vkuncak 2008/09/15 15:05 vkuncak 2008/09/15 15:03 vkuncak 2008/09/15 14:57 vkuncak 2008/09/14 00:12 vkuncak 2008/09/13 23:59 vkuncak 2008/04/24 13:36 vkuncak 2008/04/24 13:33 piskac 2008/04/23 21:09 vkuncak 2008/04/23 21:09 vkuncak 2008/04/23 18:23 vkuncak 2008/04/23 18:05 vkuncak 2008/04/23 17:55 vkuncak 2008/04/17 13:16 vkuncak 2008/04/17 13:15 vkuncak 2008/04/17 13:14 vkuncak 2008/04/16 18:19 vkuncak 2008/04/16 18:18 vkuncak 2008/04/16 17:21 vkuncak 2008/04/16 17:20 vkuncak 2008/04/16 17:15 vkuncak 2008/04/16 17:11 vkuncak 2008/04/16 17:10 vkuncak 2008/04/16 17:10 vkuncak 2008/04/16 17:09 vkuncak 2008/04/16 17:07 vkuncak 2008/04/16 16:44 vkuncak 2008/04/15 12:56 vkuncak 2008/04/15 12:54 vkuncak 2008/04/15 12:54 vkuncak 2008/04/15 12:51 vkuncak 2008/04/15 12:48 vkuncak 2008/04/15 12:48 vkuncak created 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: Solution (added afterwards):​ Solution (added afterwards):​ - * {{sav08:​laeuchlileonard66linearorder.pdf|Läuchli,​ H., Leonard, J.: On the elementary theory of linear order. Fund. Math. 59, 109–116 (1966)}} ​(Thanks to Yuri Gurevich, who also mentions that result follows from decidability of S2S) + * {{sav08:​laeuchlileonard66linearorder.pdf|Läuchli,​ H., Leonard, J.: On the elementary theory of linear order. Fund. Math. 59, 109–116 (1966)}} - * [[http://​www.jstor.org/​sici?​sici=0022-4812%28196806%2933%3A2%3C287%3AOTETOL%3E2%2E0%2ECO%3B2-I&​origin=euclid|review]], ​{{sav08:review-linearorder.pdf|review pdf}} + * {{sav08:rabin69s2s.pdf|Decidability of Second-Order Theories and Automata on Infinite Trees, by Michael O. Rabin}} Somewhat related papers: Somewhat related papers:

sav08/homework08.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice