TU Wien:Formale Methoden der Informatik VU (Egly)/Ausarbeitung Prüfung 2023-10-31 (fmi235)

Block 1

Recall from the lecture the NP-complete problem SAT and its specialization 3-SAT, that is also NP-complete:

• SATINSTANCE: A propositional formula $\varphi$. QUESTION: Is $\varphi$ satisfiable?
• 3-SATINSTANCE: A propositional formula $\varphi$ in 3-CNF, i.e. of the form $\bigwedge _{i=1}^{n}(l_{i1}\lor l_{i2}\lor l_{i3})$. QUESTION: Is $\varphi$ satisfiable?

For this exercise, assume that instances of 3-SAT are restricted to those in which no variable occurs twice in the same clause (the problem remains NP-complete under this restriction). Consider now the following variant of SAT:

• (<=3,3)-SATINSTANCE: A propositional formula $\varphi$ in CNF, where each clause consists of at most 3 literals over pairwise distinct variables and each variable has at most 3 occurrences. QUESTION: Is $\varphi$ satisfiable?

1a) Reduction Proof

The following describes a polynomial-time many-one reduction from 3-SAT to (<=3,3)-SAT: Consider $\varphi =\bigwedge _{i=1}^{n}(l_{i1}\lor l_{i2}\lor l_{i3})$ over variables V. Let $V'\subseteq V$ be the set of all variables that occur more than 3 times in $\varphi$. For each $x\in V'$, we do the following. Let k be the number of occurrences of x in $\varphi$:

1. Introduce k new variables $x_{1},\dots ,x_{k}$ and replace the i'th occurrence of x in $\varphi$ with $x_{i}\forall i=1,\dots ,k$
2. Append clauses $(x_{i}\lor \neg x_{i+1}),i=1,\dots ,k-1$ as well as $(x_{k}\lor \neg x_{1})$ to the resulting formula of step 2.

Let $\varphi '$ be the formula obtained from $\varphi$ by applying the two steps listed above, for each $x\in V'$.

It holds that $\varphi$ is a positive instance of 3-SAT iff $\varphi '$ is a positive instance of (<=3,3)-SAT. Show the => direction of the claim.

Proposed solution

Assume we have a positive instance of 3-SAT, i.e. there exists a truth assignment ${\mathcal {T}}(v)\,\forall v\in V$ s.t. $\varphi$ evaluates to true.

We show that every instance $\varphi '$ resulting from the reduction is a positive instance of (<=3,3)-SAT, i.e. there exists a truth assignment ${\mathcal {T'}}$such that $\varphi '$ evaluates to true:

• We construct ${\mathcal {T'}}$ by copying ${\mathcal {T}}$ and expanding it for variables newly introduced in step 1 of the reduction, where every newly introduced variable is assigned the same value as the variable they replace:
  • ${\mathcal {T'}}(y)={\mathcal {T}}(y)\forall y\in V\setminus V'$
  • ${\mathcal {T'}}(x_{i})={\mathcal {T}}(x)\forall x\in V'$ for all i = 1,...,k where k is the number of occurrences of x in the original formula (c.f. reduction step 1)
• For $\varphi '$ to evaluate to true under ${\mathcal {T'}}$ every clause it contains has to evaluate to true under ${\mathcal {T'}}$. These clauses can be split into two groups which we analyse separately:
  • Clauses that were already present in $\varphi$, with some variables potentially replaced by step 1 of the reduction: Because by construction of ${\mathcal {T'}}$ replacement variables have the same truth value as the variables they replaced, and we know from the assumption that these clauses evaluate to true under ${\mathcal {T}}$, we know that they also evaluate to true under ${\mathcal {T'}}$ - any of them not evaluating to true would contradict our assumption.
  • Clauses that have been appended in Step 2 of the reduction: By construction of ${\mathcal {T'}}$ we know that ${\mathcal {T'}}(x_{i})={\mathcal {T'}}(x_{j})\forall 1\leq I\leq j\leq k$, because all such replacement variables were assigned the truth value of the variables they replaced. Therefore any clause $(x_{i}\lor \neg x_{i+1})$ is trivially true because it is equal to $(x_{i}\lor \neg x_{i})$("Tertium non datur").

We have therefore shown that by construction of $\varphi '$ and ${\mathcal {T'}}$ and under the assumption that the original problem instance is a positive instance of 3-SAT, any instance resulting from the reduction is a positive instance of (<=3,3)-SAT, q.e.d.

1b) Multiple Choice

• The correctness of the reduction in (a) proves that (<=3,3)-SAT is NP-hard
  • true: Since 3-SAT is NP-complete (NP-hard + NP-membership), (<=3,3)-SAT is also NP-hard because of the reduction.
• The correctness of the reduction in (a) proves that (<=3,3)-SAT is in NP
  • false: The reduction does not show NP-membership.
• Every instance of (<=3,3)-SAT is an instance of 3-SAT
  • false: (<=3,3)-SAT may contain clauses with only 2 literals, which are not available in 3-SAT.

• Every instance of (<=3,3)-SAT is an instance of SAT
  • true: It is written on the first page of the problem description, that (<=3,3)-SAT is a variant of SAT, and since the question (Is $\varphi$ satisfiable?) is the same, it is also a special case of SAT.
• If we can show (<=3,3)-SAT to be in P, we would also show P=NP
  • true: Every problem in NP can be reduced to 3-SAT, since it is NP-hard. If (<=3,3)-SAT was in P, 3-SAT would also be in P, and thus also all other problems in NP=P.
• Any problem that can be reduced to (<=3,3)-SAT in polynomial time is in NP
  • true: Since (<=3,3)-SAT is in NP, every problem reduced to it is also in NP.

Block 3

3a) Prove or disprove Inductive Loop Invariants

Let p be the following IMP program loop, containing the integer-valued program variables x, y:

while x != x + 1 do

x := x + 1;

y := y + 6 ∗ x − 3;

od

Which of the following program assertions are inductive loop invariants of p?

• I1 : y > x

• I2 : y = 3 ∗ x^2

• I3 : y < x

Give formal details justifying your answer. That is, if an assertion is an inductive loop invariant, provide a formal proof of it based on Hoare logic or using weakest liberal preconditions. If an assertion is not an inductive loop invariant, give a counterexample and justify your answer.

Answer:

(I && b) -> wlp(p, I) (Rule for proving inductive loop variants)

b = x != x + 1 => b = true

p = p1; p2;

p1 = x := x + 1;

p2 = y := y + 6x - 3;

I1:

(y > x && x != x + 1) -> wlp(p1; p2, y > x)

(y > x && true) -> wlp(p1, wlp(p2, y > x))

y > x -> wlp(p1, y + 6x - 3 > x)

y > x -> y + 6 * (x + 1) - 3 > x + 1

y > x -> y > -5x - 2

Counterexample: x := -1, y := 0

0 > -1 -> 0 > 3

true -> false 🗲

I2:

(y = 3 ∗ x^2 && true) -> wlp(p1, wlp(p2, y = 3 ∗ x^2))

y = 3 ∗ x^2 -> wlp(x := x + 1, y + 6 ∗ x − 3 = 3 ∗ x^2 )

y = 3 * x^2 -> y + 6 * (x + 1) - 3 = 3 * (x + 1)^2

y = 3 * x^2 -> y + 6x + 6 - 3 = 3 * x^2 + 6x + 3

y = 3 * x^2 -> y = 3 * x^2 ✔

I3:

(y < x && true) -> wlp(p1, wlp(p2, y < x))

y < x -> wlp(x := x + 1, y + 6 ∗ x − 3 < x)

y < x -> y + 6 ∗ (x + 1) − 3 < x + 1

y < x -> y + 6x + 6 - 3 < x + 1

y < x -> y < -5x - 2

Counterexample: x := 0, y := -1

-1 < 0 -> -1 < -2

true -> false 🗲

Block 4

4a) Create minimal bisimulating Kripke Structure

Given a Kripke structure M, provide a minimal (i.e. minimal amount of states) Kripke Structure K such that there is a Bisimulation, and a bisimulation relation.

4c) LTL Tautologies

Give formal proof showing that the LTL formula is a tautology, or a counterexample in form of a Kripke structure:

AFGa => AFAGa / AFAGa => AFGa

Counterexample for AFGa => AFAGa: S = {s0, s1, s2}, S0 = {s0}, L = {s0 -> a, s2 -> a}, R = {(s0, s0), (s0, s1), (s1, s2), (s2, s2)}