SGT Sheet

Question 1

Greedy SAT Algorithm

This is an example of a greedy search algorithm:

1. Guess a variable assignment at random $P:=\top ,Q:=\perp ,R:=\perp$
2. Evaluate your guess by counting number of satisfied clauses.
3. Consider the effect of swapping a single variable from $\top$ to $\perp$ or vice-versa.
4. Update the assignment to the assignment that leads to the biggest increase in the number of satisfied clauses.
5. Repeat until no further improvements are possible.

We find that this algorithm runs in polynomial time:

• Selecting a random assignment and evaluating the ‘score’ of the assignment can both be done in linear time, $O(1)$.
• Each iteration involves evaluating at most $n$ assignments that different in a single variable, which requires at most a polynomial number of steps.
• We can never decrease ‘score’, so we iterate at most polynomial times.

This algorithm is not complete and may sometimes report unsatisfiable when it actually is. Despite this, it is a relatively quick algorithm and may be used as the first part of a SAT solver to help improve performance.

Link to original

1. Guess variable assignment $P:=\top ,Q:=\perp ,R:=\top$
2. Evaluate: all clauses are satisfied.
3. No further improvements can be made.

Question 2

DPLL Algorithm

The Davis-Putnam-Logemann-Loveland (DPPL) algorithm was proposed in the 1962. It is a divide-and-conquer backtrack-search type algorithm, it works as follows:

• Run pure literal elimination and unit clause propagation.
• If any clauses remain unsatisfied, we branch on any remaining variable $P$:
  • Choose to make $P:=\perp$ by adding $\neg P$ to $U$
  • Choose to make $P:=\top$ by adding $P$ to $U$
• We can achieve this by recursively calling the DPLL Algorithm until either:
  • all clauses are satisfied and $C=\varnothing$
  • a conflict is detected in the partial assignment $U$

Link to original

1. No unit clauses, no pure literals.
2. Branch on $P:=\perp$:
   1. $(Q),(R\vee S),(\neg Q\vee R\vee S),(\neg Q\vee \neg R\vee \neg S),(\neg Q\vee R\vee \neg S)$
   2. Unit clause elimination on $Q$: $(R\vee S),(R\vee S),(\neg R\vee \neg S),(R\vee \neg S)$
   3. Branch on $R:=\top$:
      1. $(\neg S)$
      2. Unit clause elimination on $\neg S$.
      3. All clauses are satisified.

Hence satisfying assignment is $P:=\perp ,Q:=\top ,R:=\top ,S:=\perp$.

Question 3

$$F=(P\vee Q)\wedge (\neg R\vee S)\wedge (\neg Q\vee S)\wedge (\neg P\vee \neg S)\wedge (\neg S\vee \neg Q)$$

1. Construct the implication graph for $F$:

$$\begin{array}{c}(\neg P\to Q)\wedge (\neg Q\to P)\\ (R\to S)\wedge (\neg S\to \neg R)\\ (Q\to S)\wedge (\neg S\to \neg Q)\\ (P\to \neg S)\wedge (S\to \neg P)\\ (Q\to \neg S)\wedge (S\to \neg Q)\end{array}$$

This produces the Scc graph:

To find the satisfying assignment, we need to find suitable assignments to ensure that the graph holds:

Question 4

$(P\vee \neg Q\vee \neg S),(\neg P\vee \neg S\vee T),(\neg Q\vee \neg R\vee \neg S\vee \neg W),(P\vee \neg R),$ $(Q),(T\vee \neg W),(\neg Q\vee S),(\neg P\vee \neg R\vee \neg T\vee \neg W)$

1. Unit clause elimination on $Q$: $(P\vee \neg S),(\neg P\vee \neg S\vee T),(\neg R\vee \neg S\vee \neg W),(P\vee \neg R),(T\vee \neg W),(S),(\neg P\vee \neg R\vee \neg T\vee \neg W)$
2. Unit clause elimination on $S$: $(P),(\neg P\vee T),(\neg R\vee \neg W),(P\vee \neg R),(T\vee \neg W),(\neg P\vee \neg R\vee \neg T\vee \neg W)$
3. Unit clause elimination on $P$: $(T),(\neg R\vee \neg W),(T\vee \neg W),(\neg R\vee \neg T\vee \neg W)$
4. Unit clause elimination on $T$: $(\neg R\vee \neg W),(\neg W),(\neg R\vee \neg W)$
5. Unit clause elimination on $\neg W$: $(R),(\neg R)$
6. Unit clause elimination on $\neg R$: Empty set of clauses.

Hence they are all satisfiable.