Tutorial 5

Boolean SAT

Exercise sheet 13 questions

Truth-function representations

Apply both techniques from Chapter 5 · Boolean SAT to each function below:

Use $INPUT₁$ for the input down the left and $INPUT₂$ for the input across the top.

Describe each row with output $1$ by a conjunction, then disjoin the descriptions to obtain DNF (glossary, opens in a new tab) .
Exclude each row with output $0$ by a disjunction, then conjoin these clauses to obtain CNF (glossary, opens in a new tab) .
Simplify where possible. Explain why the two descriptions have the same truth-values.

AND	0	1
0	0	0
1	0	1

XOR	0	1
0	0	1
1	1	0

XNOR	0	1
0	1	0
1	0	1

NOR	0	1
0	1	0
1	0	0

Check your descriptions below. Both fully bracketed formulas and the chapter’s bracketing conventions are accepted. Equivalent answers count, provided they are in the requested normal form.

Choose a level to begin.

Solution

The descriptions read directly from the rows are:

Function	DNF	CNF
$AND$	$INPUT₁ \land INPUT₂$	$(INPUT₁ \lor INPUT₂) \land (INPUT₁ \lor \negINPUT₂) \land (\negINPUT₁ \lor INPUT₂)$
$XOR$	$(\negINPUT₁ \land INPUT₂) \lor (INPUT₁ \land \negINPUT₂)$	$(INPUT₁ \lor INPUT₂) \land (\negINPUT₁ \lor \negINPUT₂)$
$XNOR$	$(\negINPUT₁ \land \negINPUT₂) \lor (INPUT₁ \land INPUT₂)$	$(INPUT₁ \lor \negINPUT₂) \land (\negINPUT₁ \lor INPUT₂)$
$NOR$	$\negINPUT₁ \land \negINPUT₂$	$(INPUT₁ \lor \negINPUT₂) \land (\negINPUT₁ \lor INPUT₂) \land (\negINPUT₁ \lor \negINPUT₂)$

The CNF for $AND$ simplifies to $INPUT₁ \land INPUT₂$ ; that for $NOR$ simplifies to $\negINPUT₁ \land \negINPUT₂$ . Both are also DNFs. The XOR and XNOR descriptions already have two clauses or terms. DNF includes exactly the rows requiring $1$ ; CNF excludes exactly the rows requiring $0$ . They therefore describe the same function.

Circuit representations

Read each circuit from its inputs to its lamp. Write a formula using only $\neg$ and $\land$ to describe the lamp’s output. A default-off relay conjoins its magnet input and signal supply; a powered default-on relay negates its magnet input. Treat the fixed supply as $1$ .

Use the level buttons to move between the five circuits. Enter your description above the circuit; Check compares it with the lamp on every input. You can also try the switches yourself. Which descriptions are already in DNF or CNF?

Choose a level to begin.

Solution

The default-off relay gives $INPUT₁ \land INPUT₂$ . This is both DNF and CNF.
The first relay gives $INPUT₁ \land INPUT₂$ . The powered default-on relay negates it, giving $\neg(INPUT₁ \land INPUT₂)$ . This is neither normal form as written. De Morgan’s law gives $\negINPUT₁ \lor \negINPUT₂$ , which is both DNF and CNF.
The default-on relay gives $\negINPUT₁$ . This becomes the magnet input of the default-off relay, whose signal supply is $INPUT₂$ . The output is $\negINPUT₁ \land INPUT₂$ , both DNF and CNF.
The first two relays give $\neg(INPUT₁ \land INPUT₂)$ . Conjoining this with $INPUT₃$ gives $\neg(INPUT₁ \land INPUT₂) \land INPUT₃$ . De Morgan gives the CNF $(\negINPUT₁ \lor \negINPUT₂) \land INPUT₃$ .
The two branches give $\neg(INPUT₁ \land INPUT₂)$ and $\neg(INPUT₂ \land INPUT₃)$ . Their outputs feed the final default-off relay, giving $\neg(INPUT₁ \land INPUT₂) \land \neg(INPUT₂ \land INPUT₃)$ . De Morgan gives the CNF $(\negINPUT₁ \lor \negINPUT₂) \land (\negINPUT₂ \lor \negINPUT₃)$ .

Equivalence

The $XNOR$ function returns $1$ iff its inputs agree. What happens when we change the inputs, or use it to compare more than two values?

Negate one input of $SUN \leftrightarrow RAIN$ . Describe the resulting function using $\neg$ , $\land$ , and $\lor$ .
Negate both inputs. How does the resulting function compare with the original? Give a formula for it.
Find a formula which is true iff $SUN$ , $RAIN$ , and $WIND$ all have the same value. Does $(SUN \leftrightarrow RAIN) \leftrightarrow WIND$ do this? If not, give an assignment on which it fails.

The three levels show the required tables. Enter your formula in the final column heading to check it. Explain your answers on paper as well.

Choose a level to begin.

Solution

Negating one input switches agreement and disagreement. We obtain XOR, described by $(SUN \land \negRAIN) \lor (\negSUN \land RAIN)$ .
Negating both preserves agreement: $\negSUN \leftrightarrow \negRAIN$ is equivalent to $SUN \leftrightarrow RAIN$ .
One answer is $(SUN \leftrightarrow RAIN) \land (RAIN \leftrightarrow WIND)$ . If both comparisons hold, all three values agree. Another is $(SUN \land RAIN \land WIND) \lor (\negSUN \land \negRAIN \land \negWIND)$ . Chaining $\leftrightarrow$ does something different: when all three values are $0$ , $(SUN \leftrightarrow RAIN) \leftrightarrow WIND$ evaluates to $1 \leftrightarrow 0$ , hence $0$ . The values agree, but the chained formula is false.

Working with pseudocode

The algorithms in this chapter use a few ideas beyond the first parsing example. Practise them here before combining them in a SAT algorithm.

while condition: repeats its indented instructions while the condition holds. Something in the loop must bring us closer to stopping.
empty_list() creates a list with no entries. add(list, item) adds one item at its end; add_all(list, items) adds each supplied item.
first_member(pair) and second_member(pair) return the two members of a pair, one at a time. For example, the members of (1, 2) are $1$ and $2$ .
record_name(node, name) keeps a name beside a tree node; name_of(node) reads it back. This lets later steps use an earlier result.

Remember: = assigns a value, while == tests equality. The app prompts explain the helpers used in each example.

Complete the four examples. Explain what each takes as input and returns.
Trace count_down(3) by writing down which calculation steps it performs. Include the value of number after each assignment. What happens with input $0$ ? What happens with input $3$ if we remove the assignment inside the loop?
Write a procedure count_ones(values) which returns the number of ones in a finite list of zeros and ones. Use a counter, for, and if. Trace it on [0, 1, 1] and on an empty list. Why does it finish?
Trace check_pairs on [(1, 2), (1, 3)]. What is in checked after each iteration? What would change if return checked were indented inside the loop?
Trace name_parts on $\negSUN \lor RAIN$ , visiting the left child before the right and using fresh names $u₁$ , $u₂$ , … . List the nodes in visit order and their names. Does naming them alone make the original formula true?

Solution

The gaps, in order, are:
- Repeat while needed: while, =. It takes a nonnegative whole number and returns $0$ .
- Collect matching values: empty_list, ==, add. It takes a list of zeros and ones and returns a list containing its ones.
- Record checked pairs: for, in, add. It takes pairs of clause numbers, checks each, and returns the list of checked pairs.
- Name the parts first: for, if, else. It takes a parse tree, records names for its nodes, and returns the root’s name.
The successive values are $2$ , $1$ , and $0$ . The procedure returns $0$ . With input $0$ , the loop is skipped. Without the assignment, input $3$ keeps satisfying number > 0, so the procedure never finishes.

One solution is:

python

1
2
3
4
5
6


def count_ones(values):
    count = 0
    for value in values:
        if value == 1:
            count = count + 1
    return count

The counter starts at $0$ , then has values $0$ , $1$ , and $2$ after the three iterations. The answer is $2$ . An empty list gives $0$ . Each iteration handles one entry of a finite list.

The list is first [(1, 2)], then [(1, 2), (1, 3)]. A return inside the loop would finish after the first pair, leaving the second unchecked. With an empty input, that misplaced return would never be reached.
The visit order and names are $SUN$ : $SUN$ ; $\negSUN$ : $u₁$ ; $RAIN$ : $RAIN$ ; $\negSUN \lor RAIN$ : $u₂$ . The procedure returns $u₂$ . Names alone impose no truth-value requirements. Tseytin (glossary, opens in a new tab) conversion must also add the local constraints and the root clause.

Truth tables

Use the app to construct a truth-table (glossary, opens in a new tab) for each of the formulas shown in its level buttons. First identify the distinct variables: enter their names separated by commas, for example SUN, RAIN. How many rows do we need?

The app supplies these rows and the parse tree. Match each empty column heading to a compound node in the tree, working from the smallest subformulas upward. Then calculate the entries yourself. Selecting a cell highlights its subformula and shows that row’s variable values in the tree. Which formulas are satisfiable? Which are tautologies?

Choose a level to begin.

Solution

There are four rows for levels 1–4 and 6, and eight for level 5. The formulas in levels 1–5 are satisfiable; level 6 is unsatisfiable. None is a tautology (glossary, opens in a new tab) . Here are the completed tables, with variables in the same alphabetical order as the app:

Level 1:

$RAIN$	$SUN$	$\negRAIN$	$SUN \land \negRAIN$
$0$	$0$	$1$	$0$
$0$	$1$	$1$	$1$
$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$

Level 2:

$RAIN$	$SUN$	$SUN \land RAIN$	$\neg(SUN \land RAIN)$
$0$	$0$	$0$	$1$
$0$	$1$	$0$	$1$
$1$	$0$	$0$	$1$
$1$	$1$	$1$	$0$

Level 3:

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

Level 4:

$RAIN$	$SUN$	$SUN \leftrightarrow RAIN$
$0$	$0$	$1$
$0$	$1$	$0$
$1$	$0$	$0$
$1$	$1$	$1$

Level 5:

$RAIN$	$SUN$	$WIND$	$\negRAIN$	$\negRAIN \land WIND$	$SUN \lor (\negRAIN \land WIND)$
$0$	$0$	$0$	$1$	$0$	$0$
$0$	$0$	$1$	$1$	$1$	$1$
$0$	$1$	$0$	$1$	$0$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$1$
$1$	$1$	$1$	$0$	$0$	$1$

Level 6:

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$	$\negRAIN$	$(SUN \lor RAIN) \land \negSUN \land \negRAIN$
$0$	$0$	$0$	$1$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$	$1$	$0$
$1$	$0$	$1$	$1$	$1$	$0$	$0$
$1$	$1$	$1$	$0$	$0$	$0$	$0$

Missing truth-values

Complete the gaps. The given entries are correct. For each missing value, identify the connective whose function table determines it.

Choose a level to begin.

Select a formula above the table to change levels. Selecting a missing entry highlights the corresponding part of the parse tree.

Solution

Negation switches $0$ and $1$ . Conjunction gives $1$ iff both inputs are $1$ ; disjunction gives $1$ iff at least one is $1$ . The biconditional gives $1$ iff its inputs agree. Applying these rules gives:

Level 1:

$RAIN$	$SUN$	$SUN \land RAIN$	$\neg(SUN \land RAIN)$
$0$	$0$	$0$	$1$
$0$	$1$	$0$	$1$
$1$	$0$	$0$	$1$
$1$	$1$	$1$	$0$

Level 2:

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

Level 3:

$RAIN$	$SUN$	$\negRAIN$	$SUN \leftrightarrow \negRAIN$
$0$	$0$	$1$	$0$
$0$	$1$	$1$	$1$
$1$	$0$	$0$	$1$
$1$	$1$	$0$	$0$

Level 4:

$RAIN$	$SUN$	$WIND$	$SUN \land WIND$	$\negRAIN$	$(SUN \land WIND) \lor \negRAIN$
$0$	$0$	$0$	$0$	$1$	$1$
$0$	$0$	$1$	$0$	$1$	$1$
$0$	$1$	$0$	$0$	$1$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$0$
$1$	$1$	$1$	$1$	$0$	$1$

Mystery formula

Find a formula for each table. Any formula with the right truth-values counts; different spellings can describe the same function. Try to find a short one. You may leave out variables that do not affect the result. Enter your formula in the final column heading. The app gives a counterexample whenever it disagrees with the table.

Choose a level to begin.

Solution

One answer for each level is:

$\negSUN$
$SUN \land RAIN$
$SUN \lor RAIN$
$\neg(SUN \land RAIN)$
$(SUN \land \negRAIN) \lor (\negSUN \land RAIN)$
$SUN \leftrightarrow RAIN$
$SUN \lor \negWIND$
$(SUN \land RAIN) \lor WIND$

For level 7, changing $RAIN$ never changes the result. This is why it need not occur in the answer. Reading off DNF or CNF gives an answer for every level, though it need not be the shortest one.

Normal Forms

Rewrite each formula into DNF and CNF. Name the laws you use. You may simplify repetitions, contradictions, and tautological clauses (glossary, opens in a new tab) , but these simplifications are not required merely to reach normal form.

$RAIN \land \neg(SUN \lor \negRAIN)$
$\negRAIN \lor \neg(\negRAIN \lor WIND)$
$(RAIN \land \negSUN) \lor (\negRAIN \land \negSUN)$
$SUN \lor (RAIN \land WIND)$
$(SUN \lor RAIN) \land (\negSUN \lor WIND)$
$\neg(SUN \leftrightarrow RAIN)$

Solution

De Morgan and double negation give $RAIN \land \negSUN \land RAIN$ . Idempotence gives $RAIN \land \negSUN$ , both DNF and CNF.
De Morgan and double negation give the DNF $\negRAIN \lor (RAIN \land \negWIND)$ . Distribution gives the CNF $(\negRAIN \lor RAIN) \land (\negRAIN \lor \negWIND)$ . Its first clause is a tautology, so $\negRAIN \lor \negWIND$ is also an answer in both forms.
Factoring out $\negSUN$ gives $(RAIN \lor \negRAIN) \land \negSUN$ , equivalent to $\negSUN$ . This is both DNF and CNF. The original is already a DNF.
The original is DNF. Distribution gives the CNF $(SUN \lor RAIN) \land (SUN \lor WIND)$ .
The original is CNF. Distribution gives the DNF
$(SUN \land \negSUN) \lor (SUN \land WIND) \lor (RAIN \land \negSUN) \lor (RAIN \land WIND).$
The first term can be removed because it is always false.
Eliminate $\leftrightarrow$ , then push the negation inward. The result is the DNF $(SUN \land \negRAIN) \lor (\negSUN \land RAIN)$ . Distribution gives four clauses; discard the two tautologies to obtain the CNF $(SUN \lor RAIN) \land (\negSUN \lor \negRAIN)$ .

Resolution

Each level starts with a CNF. Its conjuncts appear as numbered disjunctive clauses (glossary, opens in a new tab) . Select two clauses, choose one pivot (glossary, opens in a new tab) , and apply resolution (glossary, opens in a new tab) . Keep going until you derive $⊥$ , or until every possible resolution has been checked. In the latter case, use the Saturated? button. The app keeps the parents and records checks which give tautologies or clauses already present.

Choose a level to begin.

For each satisfiable input, also give a satisfying valuation on paper.

Solution

Resolve $SUN \lor RAIN$ with $\negSUN$ on $SUN$ , obtaining $RAIN$ . Resolve with $\negRAIN$ to derive $⊥$ .
Resolve the two input clauses on $RAIN$ , obtaining $SUN \lor \negWIND$ . There are no further complementary pairs. A satisfying valuation is $SUN = 1$ , $RAIN = 0$ , $WIND = 0$ .
Resolve on $WIND$ , obtaining $\negSUN \lor \negRAIN$ . There are no further complementary pairs. Take $SUN = RAIN = WIND = 0$ .
Resolve the first two clauses on $RAIN$ to obtain $SUN$ , and the last two on $RAIN$ to obtain $\negSUN$ . Resolving these gives $⊥$ .
No clauses contain complementary literals. The input is already saturated; take $SUN = RAIN = 1$ .
Resolving on $SUN$ gives $RAIN \lor \negRAIN$ ; resolving on $RAIN$ gives $SUN \lor \negSUN$ . Both are tautologies and impose no new requirement. After both checks, the input is saturated. Take $SUN = 1$ , $RAIN = 0$ . Removing both complementary pairs in one step would be unsound.
The first two clauses have two possible pivots, but either choice gives a tautology. A shorter route uses the units: resolve $\negSUN \lor \negRAIN$ with $SUN$ to get $\negRAIN$ , then with $RAIN$ to get $⊥$ .
Resolve $\negWIND \lor SNOW$ with $\negSNOW$ to get $\negWIND$ . Resolving this with $\negSUN \lor WIND$ and with $\negRAIN \lor WIND$ gives $\negSUN$ and $\negRAIN$ . Resolve $SUN \lor RAIN$ with $\negSUN$ to get $RAIN$ , then with $\negRAIN$ to get $⊥$ .

Countermodels after resolution

The following refutation searches are complete. Every possible resolution has been checked, and none adds a new non-tautological clause. No search derives $⊥$ .

For each inference, use the final clauses to find a countermodel (glossary, opens in a new tab) . Begin with any unit clauses (glossary, opens in a new tab) , then choose values for the remaining atoms. Check that all the clauses are true, all the original premises are true, and the conclusion is false. You don’t need to construct a full truth-table.

$SUN \to RAIN, \negSUN ∴ \negRAIN$

Line Clause Source

1 $\negSUN \lor RAIN$ First premise
2 $\negSUN$ Second premise
3 $RAIN$ Negated conclusion

There are no complementary literals between clauses.
$SUN \leftrightarrow RAIN ∴ SUN$

Line Clause Source

1 $\negSUN \lor RAIN$ Premise, in CNF
2 $SUN \lor \negRAIN$ Premise, in CNF
3 $\negSUN$ Negated conclusion
4 $\negRAIN$ Lines 2 and 3, pivot $SUN$

The other resolutions produce tautologies or clauses already listed.
$SUN \lor RAIN ∴ SUN \land RAIN$

Line Clause Source

1 $SUN \lor RAIN$ Premise
2 $\negSUN \lor \negRAIN$ Negated conclusion, in CNF

Resolving on either variable gives a tautology. There are no unit clauses. Find both countermodels. Why does setting both atoms false fail? Why does setting both true fail?

Line	Clause	Source
1	$\negSUN \lor RAIN$	First premise
2	$\negSUN$	Second premise
3	$RAIN$	Negated conclusion

Line	Clause	Source
1	$\negSUN \lor RAIN$	Premise, in CNF
2	$SUN \lor \negRAIN$	Premise, in CNF
3	$\negSUN$	Negated conclusion
4	$\negRAIN$	Lines 2 and 3, pivot $SUN$

Line	Clause	Source
1	$SUN \lor RAIN$	Premise
2	$\negSUN \lor \negRAIN$	Negated conclusion, in CNF

Would finding no contradiction after just a few resolution steps have been enough to conclude that these inferences are invalid? Explain.

Solution

Line 2 fixes $SUN = 0$ ; line 3 fixes $RAIN = 1$ . Line 1 is true because both its literals are true. In the original inference, $SUN \to RAIN$ and $\negSUN$ are true, but $\negRAIN$ is false.
Line 3 fixes $SUN = 0$ . Line 2 then requires $RAIN = 0$ , which line 4 also tells us. Line 1 is true because $\negSUN$ is true. The two atoms agree, so the premise $SUN \leftrightarrow RAIN$ is true, while the conclusion $SUN$ is false.
The first clause requires at least one atom to be true. The second requires at least one to be false. Choose $SUN = 1, RAIN = 0$ , or $SUN = 0, RAIN = 1$ . Each choice makes the premise true and the conclusion false. Setting both false violates line 1; setting both true violates line 2. We cannot choose values independently for each clause: one valuation must satisfy them all.

An unfinished search might still derive $⊥$ later. Saturation without $⊥$ establishes satisfiability; a checked countermodel directly establishes invalidity, even if we haven’t completed the search.

Valid inference

Check each inference shown in the app by truth-table and by resolution. Decide which SAT problem will tell you whether the inference is valid. For an invalid inference, give a countermodel (glossary, opens in a new tab) .

For resolution, convert your SAT formula to CNF and enter its clauses in the input field. You can join them with $\land$ , or separate them with commas. For example, (SUN ∨ RAIN), ¬SUN supplies two clauses. The app checks that your clauses express the right SAT problem; you then choose the resolution steps yourself.

Choose a level to begin.

You may use the rewriting app below to help with conversion. Decide which formula to put in before you start.

CNF rewriting

Ex.

The interactive example is loading.

Solution

Test $\negRAIN \land \neg(RAIN \lor (\negRAIN \land SUN))$ . Its CNF simplifies to $\negRAIN \land (RAIN \lor \negSUN)$ . Resolution gives $\negSUN$ and then saturates (glossary, opens in a new tab) . The countermodel $RAIN = SUN = 0$ makes the premise true and conclusion false.
Test $(RAIN \lor (RAIN \land WIND)) \land \neg(RAIN \lor SUN)$ . Its CNF is $RAIN \land (RAIN \lor WIND) \land \negRAIN \land \negSUN$ . Resolve $RAIN$ and $\negRAIN$ to obtain $⊥$ . The inference is valid.
The SAT formula is already CNF: $(SUN \lor RAIN) \land (\negSUN \lor WIND) \land (\negRAIN \lor WIND) \land \negWIND$ . Resolve the second and third clauses with $\negWIND$ to get $\negSUN$ and $\negRAIN$ . These refute the first clause. The inference is valid.
The CNF is $(SUN \lor RAIN) \land (\negSUN \lor WIND) \land \negWIND$ . Resolution gives $\negSUN$ , then $RAIN$ , and saturates. Take $SUN = WIND = 0$ and $RAIN = 1$ : both premises are true, but the conclusion is false.
The CNF is $(SUN \lor RAIN) \land (\negSUN \lor WIND) \land (\negRAIN \lor SNOW) \land \negWIND \land \negSNOW$ . The last two clauses give $\negSUN$ and $\negRAIN$ by resolution with the second and third. These refute $SUN \lor RAIN$ . The inference is valid.

For the truth-table check, the final columns of these two SAT formulas are as follows. A $1$ marks a countermodel:

$RAIN$	$SUN$	First SAT formula
$0$	$0$	$1$
$0$	$1$	$0$
$1$	$0$	$0$
$1$	$1$	$0$

The second SAT formula is $0$ on all eight assignments to $RAIN$ , $SUN$ , and $WIND$ : its first part requires $RAIN = 1$ , while its second requires $RAIN = 0$ . The third and fifth SAT formulas are likewise always $0$ . The fourth has just one satisfying row: $RAIN = 1$ , $SUN = WIND = 0$ .

Comparing the algorithms

Does resolution always outperform truth-table search? Explain the difference between a worst-case bound and the work on a particular input.
Suppose truth-table search tries the all-zero assignment first. Compare it with resolution on $(\negSUN \lor RAIN) \land (SUN \lor \negRAIN)$ and on $\negSUN \lor \negRAIN$ . Count rows examined and resolution steps separately. Is that enough to compare running times?
A formula has $10$ variables. How many rows does its full table have? What if we add $5$ variables? Must a SAT search always examine them all?
Why can an input with few symbols still be expensive to prepare for resolution? Use $(SUN \land WARM) \lor (RAIN \land WIND)$ as a starting point.

Solution

No. Both algorithms have expensive worst cases, but that does not determine which is faster on a given input. Resolution may find a short refutation; truth-table search may find a satisfying row early. General results about SAT do not give all algorithms identical costs.
For the first formula, $00$ already succeeds, so truth-table search examines one row. Resolution checks the two pivots; both resolvents are tautologies, so it saturates. For the second formula, the first row already satisfies it. Resolution has one clause and no pair to examine. Neither count includes all the work: parsing, evaluation, CNF preparation, and finding or checking clause pairs also take time. These examples give no universal speed ranking.
The tables have $2¹⁰ = 1024$ and $2¹⁵ = 32768$ rows, respectively. A SAT search can stop at a satisfying row. If none exists, the chapter’s straightforward table search examines every row.
Distribution copies parts of formulas. The displayed input gives four CNF clauses. Adding another disjunct consisting of two fresh atoms doubles this to eight. With $n$ such pairs, there are $2ⁿ$ clauses, although the input grows only by one pair at a time.

Tseytin transformation

Apply the Tseytin transformation (glossary, opens in a new tab) to the formulas below. Work from the leaves upward, visiting the left child before the right. Use fresh names $u₁$ , $u₂$ , … in that order. Write the local constraints and the final clause which requires the root to be true.

$\neg(SUN \land RAIN)$
$(SUN \lor RAIN) \land \negWIND$
$(SUN \land RAIN) \lor (\negSUN \land WIND)$
$(SUN \land RAIN) \lor (WIND \land SNOW)$
$(SUN \lor RAIN) \land (\negSUN \land \negRAIN)$

For each satisfiable formula, extend one satisfying valuation to the fresh variables. Explain why we cannot omit the final root clause, and why the result is equisatisfiable (glossary, opens in a new tab) rather than logically equivalent over the expanded vocabulary. For formula 4, also compare the result with the CNF obtained by distribution: which uses fewer clauses here? What if we keep adding disjuncts consisting of two fresh atoms?

Solution

Each row below gives one naming step and its local constraints. Conjoin all the constraints for that formula and add the stated root clause.

For $\neg(SUN \land RAIN)$ :

Name Subformula, using earlier names Local constraints

$u₁$ $SUN \land RAIN$ $(\negu₁ \lor SUN) \land (\negu₁ \lor RAIN) \land (u₁ \lor \negSUN \lor \negRAIN)$
$u₂$ $\negu₁$ $(\negu₂ \lor \negu₁) \land (u₂ \lor u₁)$

Add the root clause $u₂$ . Take $SUN = RAIN = 0$ , $u₁ = 0$ , and $u₂ = 1$ .

For $(SUN \lor RAIN) \land \negWIND$ :

Name	Subformula, using earlier names	Local constraints
$u₁$	$SUN \lor RAIN$	$(u₁ \lor \negSUN) \land (u₁ \lor \negRAIN) \land (\negu₁ \lor SUN \lor RAIN)$
$u₂$	$\negWIND$	$(\negu₂ \lor \negWIND) \land (u₂ \lor WIND)$
$u₃$	$u₁ \land u₂$	$(\negu₃ \lor u₁) \land (\negu₃ \lor u₂) \land (u₃ \lor \negu₁ \lor \negu₂)$

Add the root clause $u₃$ . Take $SUN = 1$ , $RAIN = WIND = 0$ , and $u₁ = u₂ = u₃ = 1$ .

For $(SUN \land RAIN) \lor (\negSUN \land WIND)$ :

Name	Subformula, using earlier names	Local constraints
$u₁$	$SUN \land RAIN$	$(\negu₁ \lor SUN) \land (\negu₁ \lor RAIN) \land (u₁ \lor \negSUN \lor \negRAIN)$
$u₂$	$\negSUN$	$(\negu₂ \lor \negSUN) \land (u₂ \lor SUN)$
$u₃$	$u₂ \land WIND$	$(\negu₃ \lor u₂) \land (\negu₃ \lor WIND) \land (u₃ \lor \negu₂ \lor \negWIND)$
$u₄$	$u₁ \lor u₃$	$(u₄ \lor \negu₁) \land (u₄ \lor \negu₃) \land (\negu₄ \lor u₁ \lor u₃)$

Add the root clause $u₄$ . Take $SUN = RAIN = 0$ , $WIND = 1$ , $u₁ = 0$ , and $u₂ = u₃ = u₄ = 1$ .

For $(SUN \land RAIN) \lor (WIND \land SNOW)$ :

Name	Subformula, using earlier names	Local constraints
$u₁$	$SUN \land RAIN$	$(\negu₁ \lor SUN) \land (\negu₁ \lor RAIN) \land (u₁ \lor \negSUN \lor \negRAIN)$
$u₂$	$WIND \land SNOW$	$(\negu₂ \lor WIND) \land (\negu₂ \lor SNOW) \land (u₂ \lor \negWIND \lor \negSNOW)$
$u₃$	$u₁ \lor u₂$	$(u₃ \lor \negu₁) \land (u₃ \lor \negu₂) \land (\negu₃ \lor u₁ \lor u₂)$

Add the root clause $u₃$ . Take $SUN = RAIN = 1$ , $WIND = SNOW = 0$ , $u₁ = u₃ = 1$ , and $u₂ = 0$ .

For $(SUN \lor RAIN) \land (\negSUN \land \negRAIN)$ :

Name	Subformula, using earlier names	Local constraints
$u₁$	$SUN \lor RAIN$	$(u₁ \lor \negSUN) \land (u₁ \lor \negRAIN) \land (\negu₁ \lor SUN \lor RAIN)$
$u₂$	$\negSUN$	$(\negu₂ \lor \negSUN) \land (u₂ \lor SUN)$
$u₃$	$\negRAIN$	$(\negu₃ \lor \negRAIN) \land (u₃ \lor RAIN)$
$u₄$	$u₂ \land u₃$	$(\negu₄ \lor u₂) \land (\negu₄ \lor u₃) \land (u₄ \lor \negu₂ \lor \negu₃)$
$u₅$	$u₁ \land u₄$	$(\negu₅ \lor u₁) \land (\negu₅ \lor u₄) \land (u₅ \lor \negu₁ \lor \negu₄)$

Add the root clause $u₅$ . The root requires both $u₁ = 1$ and $u₄ = 1$ . The latter requires $u₂ = u₃ = 1$ , hence $SUN = RAIN = 0$ . But this makes $u₁ = 0$ . There is no satisfying valuation.

For formula 4, distribution gives just four clauses:

(SUN \lor WIND) \land (SUN \lor SNOW) \land (RAIN \lor WIND) \land (RAIN \lor SNOW).

Tseytin uses ten clauses here, so it is not the shorter answer on this input. With $n$ disjuncts each containing two fresh atoms, distribution gives $2ⁿ$ clauses. Tseytin gives $3(2n - 1) + 1 = 6n - 2$ clauses: three for each of the $n$ conjunctions and $n - 1$ disjunctions, plus the root. The difference matters as $n$ grows.

Without the root clause, all five groups of local constraints are satisfiable: assign each name the calculated value of its subformula, even when the whole formula is false. The original formulas say nothing about the fresh names, whereas the constraints restrict them. Every satisfying valuation of the original can be extended to satisfy the encoding; every model of the encoding restricts to a model of the original. That gives equisatisfiability. For the first four formulas, arbitrary values of the fresh variables can violate the encoding while the original remains true, so they are not logically equivalent over the expanded vocabulary. The fifth is a special case: both formulas are unsatisfiable, and hence equivalent.

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

$RAIN$	$SUN$	$WIND$	$\negRAIN$	$\negRAIN \land WIND$	$SUN \lor (\negRAIN \land WIND)$
$0$	$0$	$0$	$1$	$0$	$0$
$0$	$0$	$1$	$1$	$1$	$1$
$0$	$1$	$0$	$1$	$0$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$1$
$1$	$1$	$1$	$0$	$0$	$1$

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$	$\negRAIN$	$(SUN \lor RAIN) \land \negSUN \land \negRAIN$
$0$	$0$	$0$	$1$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$	$1$	$0$
$1$	$0$	$1$	$1$	$1$	$0$	$0$
$1$	$1$	$1$	$0$	$0$	$0$	$0$

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

$RAIN$	$SUN$	$WIND$	$SUN \land WIND$	$\negRAIN$	$(SUN \land WIND) \lor \negRAIN$
$0$	$0$	$0$	$0$	$1$	$1$
$0$	$0$	$1$	$0$	$1$	$1$
$0$	$1$	$0$	$0$	$1$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$0$
$1$	$1$	$1$	$1$	$0$	$1$

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

$RAIN$	$SUN$	$WIND$	$\negRAIN$	$\negRAIN \land WIND$	$SUN \lor (\negRAIN \land WIND)$
$0$	$0$	$0$	$1$	$0$	$0$
$0$	$0$	$1$	$1$	$1$	$1$
$0$	$1$	$0$	$1$	$0$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$1$
$1$	$1$	$1$	$0$	$0$	$1$

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$	$\negRAIN$	$(SUN \lor RAIN) \land \negSUN \land \negRAIN$
$0$	$0$	$0$	$1$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$	$1$	$0$
$1$	$0$	$1$	$1$	$1$	$0$	$0$
$1$	$1$	$1$	$0$	$0$	$0$	$0$

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

$RAIN$	$SUN$	$WIND$	$SUN \land WIND$	$\negRAIN$	$(SUN \land WIND) \lor \negRAIN$
$0$	$0$	$0$	$0$	$1$	$1$
$0$	$0$	$1$	$0$	$1$	$1$
$0$	$1$	$0$	$0$	$1$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$0$
$1$	$1$	$1$	$1$	$0$	$1$

Boolean SAT

Truth-function representations lamp Show solution

Solution

Circuit representations lamp Show solution

Solution

Equivalence lamp Show solution

Solution

Working with pseudocode lamp Show solution

Solution

Truth tables lamp Show solution

Solution

Missing truth-values lamp Show solution

Solution

Mystery formula lamp Show solution

Solution

Normal Forms lamp Show solution

Solution

Resolution lamp Show solution

Solution

Countermodels after resolution lamp Show solution

Solution

Valid inference lamp Show solution

Solution

Comparing the algorithms lamp Show solution

Solution

Tseytin transformation lamp Show solution

Solution

Truth-function representations

Circuit representations

Equivalence

Working with pseudocode

Truth tables

Missing truth-values

Mystery formula

Normal Forms

Resolution

Countermodels after resolution

Valid inference

Comparing the algorithms

Tseytin transformation

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

$RAIN$	$SUN$	$WIND$	$\negRAIN$	$\negRAIN \land WIND$	$SUN \lor (\negRAIN \land WIND)$
$0$	$0$	$0$	$1$	$0$	$0$
$0$	$0$	$1$	$1$	$1$	$1$
$0$	$1$	$0$	$1$	$0$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$1$
$1$	$1$	$1$	$0$	$0$	$1$

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$	$\negRAIN$	$(SUN \lor RAIN) \land \negSUN \land \negRAIN$
$0$	$0$	$0$	$1$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$	$1$	$0$
$1$	$0$	$1$	$1$	$1$	$0$	$0$
$1$	$1$	$1$	$0$	$0$	$0$	$0$

$RAIN$	$SUN$	$SUN \lor RAIN$	$\negSUN$	$(SUN \lor RAIN) \land \negSUN$
$0$	$0$	$0$	$1$	$0$
$0$	$1$	$1$	$0$	$0$
$1$	$0$	$1$	$1$	$1$
$1$	$1$	$1$	$0$	$0$

$RAIN$	$SUN$	$WIND$	$SUN \land WIND$	$\negRAIN$	$(SUN \land WIND) \lor \negRAIN$
$0$	$0$	$0$	$0$	$1$	$1$
$0$	$0$	$1$	$0$	$1$	$1$
$0$	$1$	$0$	$0$	$1$	$1$
$0$	$1$	$1$	$1$	$1$	$1$
$1$	$0$	$0$	$0$	$0$	$0$
$1$	$0$	$1$	$0$	$0$	$0$
$1$	$1$	$0$	$0$	$0$	$0$
$1$	$1$	$1$	$1$	$0$	$1$