LARA

Homework 08 - Due 23 April or until professor or teaching assistant solves it (whichever comes later)

Problem 1

(Problem 7.10 at the end of Chapter 7 of Calculus of Computation Textbook.)

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) \} \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

  • if $y^* = -\infty$ then $S=\emptyset$
  • if $y^* = +\infty$ then $S$ contains arbitrarily large elements (for each integer $y$, there exists $y' \in S$ such that $y < y'$)
  • if $y^* \in \mathbb{Z}$ then $y^* \in S$ and $\forall y \in S. y \le y^*$

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) \} \end{equation*}

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 \} \end{equation*}

By generalizing the objective function to reals, we can solve non-linear but polynomial optimization problems using quantifier elimination over reals.

Problem 2

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} \forall x.\forall y. x \le y \land y \le x \rightarrow x=y \\ \forall x.\forall y.\forall z. x \le y \land y \le z \rightarrow x \le z \\ \forall x.\forall y. x \le y \lor y \le x \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.

Describe an algorithm that, given a sentence $F$ in this language, decides whether $F \in T$. Explain why your algorithm is correct.

If you cannot solve the problem in its entirety, write observations that you could obtain. You are allowed (but not required) to use any references (books, papers) that you can find (but it may be easier to solve the problem on your own). You must cite any references that you used. You need not write down in great detail explanations of simple facts, but if you omit any proof steps make sure that they indeed simple.

Solution (added afterwards):

Somewhat related papers: