Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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:
  
 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