Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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