Lecture 2

Propositional logic
syntax and semantics, the satisfiability problem, constraint
problems
Print version of the lecture in Logic and Proof

presented on 1 May 2019

by Dr Christoph Haase
2.1

1 Propositional logic
Propositional logic analyses how the truth values of compound sentences depend
on their constituents. The most basic kind of sentences are atomic propositions,
which can either be true or false independently of each other. Sentences are com-
bined using logical connectives, such as not (¬), or (∨), and implies (→). A prime
concern of propositional logic is, given a compound sentence, determine which truth
values of its atoms make it true. This question is key to formulating the notions of
logical consequence and valid argument.
For an example, consider the following atomic propositions and compound sen-
tences:
• Atomic propositions:
a “Alice is an architect”
b “Bob is a builder”
c “Charlie is a cook”
• Compound sentences:
¬c “Charlie is not a cook”
a∨b “Alice is an architect or Bob is a builder”
b→c “If Bob is a builder then Charlie is a cook”
The above three propositions entail that Alice is an architect, i.e., if the above
three propositions are all true then a must also be true. We denote this fact by the
entailment
¬c, a ∨ b, b → c  a .
The correctness of this entailment is independent of the meaning of the atomic
propositions. It has nothing to do with specific facts about buildings or architec-
ture, rather it is determined by the meaning of the logical connectives. As far as
propositional logic is concerned, atomic propositions are just things that are true
or false, independently of each other. To make this clear we have represented the
atomic propositions in this example by propositional variables a, b and c. In our
semantics for propositional logic each propositional variable takes either the value
1 or 0, standing for true and false respectively.
The above entailment was reasonably intuitive, but imagine trying to justify
an entailment involving tens or hundreds of sentences and variables. Clearly one

1
would quickly get confused. One of the main aims in this course is to introduce
systematic procedures supporting the calculation of such logical consequences.

2 Syntax and semantics of propositional logic

The syntax of propositional logic is given by rules for writing down well-formed
formulas.
Definition 1 (Syntax of propositional logic). Let X = {x1 , x2 , x3 , . . .} be a count-
ably infinite set of propositional variables. Formulas of propositional logic are
inductively defined as follows:
1. true and false are formulas.
2. Every propositional variable xi is a formula.
3. If F is a formula, then ¬F is a formula.
4. If F and G are formulas, then (F ∧ G) and (F ∨ G) are formulas.
Further to this definition, we introduce some additional notation:
• We often write x, y, z or p to denote propositional variables.
• We call ¬F the negation of F .
• Given formulas F and G, (F ∧ G) is the conjunction of F and G, and (F ∨ G)
is the disjunction of F and G.
• We call ¬, ∧ and ∨ logical connectives.
• We denote by F(X) the set of all formulas built from propositional variables
in X.
Having a small set of primitive connectives makes it easier to implement our
logic and to prove properties about it. However in applications it is typically helpful
to have a rich set of derived connectives to hand. These are not part of the official
language, but can be considered as macros.
• Implication: (F1 → F2 ) := (¬F1 ∨ F2 )
• Bi-implication: (F1 ↔ F2 ) := (F1 → F2 ) ∧ (F2 → F1 )
• Exclusive Or: (F1 ⊕ F2 ) V:= (F1 ∧ ¬F2 ) ∨ (¬F1 ∧ F2 )
n
• Indexed Conjunction:W i=1 Fi := (· · · ((F1 ∧ F2 ) ∧ F3 ) ∧ · · · ∧ Fn )
n
• Indexed Disjunction: i=1 Fi := (· · · ((F1 ∨ F2 ) ∨ F3 ) ∨ · · · ∨ Fn )
Note that implication and bi-implication are often also called conditional and
biconditional, respectively.
We adopt the following operator precedences: ↔ and → bind weaker than ∧
and ∨, which in turn bind weaker than ¬. Indexed conjunction and disjunction
bind weaker than any of the above operators. We also typically omit the outermost
parentheses. For example, we can write ¬x ∧ y → z instead of ((¬x ∧ y) → z).
However well-chosen parenthesis can often help to parse formulas.
Every formula F can be represented by a syntax tree, which is tree whose in-
ternal nodes are labelled by connectives, and whose leaves are labelled by propo-
sitional variables. The size of F is defined to be the number of nodes in its syntax
tree. Each node in the syntax tree determines a subformula of F whose syntax
tree is the subtree rooted at that node. Figure 1 illustrates the syntax tree of the
formula ¬((¬x4 ∨ x1 ) ∧ x3 ).
The inductive definition of formulas allows us to define functions on formulas
by structural induction, by defining the function
• For the base cases true, false and x (propositional variables), and
• For the induction step for ¬F , F ∧ G and F ∨ G, i.e., all logical connectives
We give two examples of functions defined by structural induction below.

2
 ¬

∨ x3

¬ x1

x4

Figure 1: Example of a syntax tree.

Example 2. The function size : F(X) → N returns for a given formula the number of
symbols required to write it down. Here, we assume that true and false account for
just one symbol, and that brackets are omitted:
1. size(true) = 1, size(false) = 1
2. size(x) = 1 for all x ∈ X
3. size(¬F ) = 1 + size(F )
4. size(F ∧ G) = 1 + size(F ) + size(G)
5. size(F ∨ G) = 1 + size(F ) + size(G)
The function sub : F(X) → 2F (X) returning the set of all subformulas of a given
formula can be defined by:
• sub(true) = {true}, sub(false) = {false}
• sub(x) = {x} for all x ∈ X
• sub(¬F ) = {¬F } ∪ sub(F )
• sub(F ∧ G) = {F ∧ G} ∪ sub(F ) ∪ sub(G)
• sub(F ∨ G) = {F ∨ G} ∪ sub(F ) ∪ sub(G)
For instance,

sub(¬((¬x4 ∨ x1 ) ∧ x3 ))
= {x1 , x3 , x4 , ¬x4 , (¬x4 ∨ x1 ), ((¬x4 ∨ x1 ) ∧ x3 ), ¬((¬x4 ∨ x1 ) ∧ x3 )}.

3 Semantics of propositional logic

So far, we have only seen how to write syntactically correct formulas of proposi-
tional logic. The syntax describes just a formal language, and does not give any
meaning to formulas. The meaning, the semantics, of formulas will be the topic of
this section, which is given in terms of truth values {0, 1}, where 0 indicates false
and 1 indicates true, and is defined by structural induction.
Definition 3. An assignment is a function A : X → {0, 1} that induces an assign-
ment  : F(X) → {0, 1} by structural induction as follows:
1. Â(false) = 0, Â(true) = 1
2. For every ( x ∈ X, Â(x) := A(x)
1 if Â(F ) = 0
3. Â(¬F ) :=
0 otherwise
(
1 if Â(F ) = 1 and Â(G) = 1
4. Â((F ∧ G)) :=
0 otherwise

3
 (
1 if Â(F ) = 1 or Â(G) = 1
5. Â((F ∨ G)) :=
0 otherwise

Whenever Â(F ) = 1, we say that the formula F evaluates to true under the
assignment A. Otherwise, we say that F evaluates to false under A.
Example 4. Let F = (x ∧ ¬y) ∨ z and A be an assignment such that A(x) = 1 and
A(y) = A(z) = 0. Then F evaluates to true under A, since
(
1 if Â((x ∧ ¬y)) = 1 or Â(z) = 1
Â(F ) =
0 otherwise
(
1 if Â((x ∧ ¬y)) = 1 (since A(z) = 0)
=
0 otherwise
(
1 if Â(x) = 1 and Â(¬y) = 1 (by definition of ∧)
=
0 otherwise
(
1 if Â(y) = 0 (since A(x) = 1)
=
0 otherwise
= 1 (since A(y) = 0).

In the following, for convenience we will omit writing the hat when dealing with
the induced assignment  of an assignment A.
Since any logical connective only connects a finite number of formulas, we can
alternatively give the semantics by explicitly listing the resulting truth value for all
possible truth values of the subformulas. This gives rise to so-called truth tables.
Example 5. The semantics of logical connectives via truth tables:

A(F ) A(G) A(F ∧ G) A(F ) A(G) A(F ∨ G)

0 0 0 0 0 0
1 0 0 1 0 1
0 1 0 0 1 1
1 1 1 1 1 1

A(F ) A(G) A(F → G) A(F ) A(G) A(F ⊕ G)

0 0 1 0 0 0
1 0 0 1 0 1
0 1 1 0 1 1
1 1 1 1 1 0

People new to logic get sometimes confused by the semantics of disjunction and
implication. Observe that x ∨ y evaluates to true also if both x and y evaluate to
true, whereas humans often use disjunction with the semantics of the exclusive or.
Moreover, observe that an implication x → y evaluates to true in particular when-
ever x evaluates to false: from an incorrect premise we can draw any conclusion.
In this case, we say that the implication holds vacuously.

4 Models, satisfiability and validity

We introduce a couple of further definitions of concepts that are central to propo-
sitional logic.
Definition 6. Let F ∈ F(X) and A : X → {0, 1} be an assignment.
1. If A(F ) = 1 then we write A |= F (“F holds under A”, or “A is a model of F ”. )
2. If F has at least one model then F is satisfiable, otherwise F is unsatisfiable.

4
 3. If F holds under any assignment A : X → {0, 1} then F is called valid or a
tautology, written |= F .

In particular, the satisfiability problem plays an important role, not only in

logic, but in the whole of computer science.
Definition 7. Given F ∈ F(X), the Boolean satisfiability problem (SAT) is to
decide whether F is satisfiable.

In order to illustrate the concept of a tautology, the following example states four
well-known tautologies. You can convince yourself of the fact that they actually are
tautologies by constructing the corresponding truth tables.
Example 8. The subsequent first two tautologies are known as the distributive
laws, the last two as De Morgan’s laws:

|= (F ∨ (G ∧ H)) ↔ ((F ∨ G) ∧ (F ∨ H))

|= (F ∧ (G ∨ H)) ↔ ((F ∧ G) ∨ (F ∧ H))
|= ¬(F ∧ G) ↔ ¬F ∨ ¬G
|= ¬(F ∨ G) ↔ ¬F ∧ ¬G.

We close this section with the definitions of logical consequence and equiva-
lence.
Definition 9 (Entailment). A formula G is a consequence of (or is entailed by) a
set of formulas S if every assignment that satisfies each formula in S also satisfies
G. In this case we write S |= G.
Entailment allows us to draw logical conclusions from existing facts. Using
truth tables, you can convince yourself that

{¬c, a ∨ b, b → c} |= a.

This is the example we saw in the previous section, and now we can even formally
conclude that Alice is an architect.
Warning! In logic the symbol |= is overloaded. Above we define S |= F
for a set of formulas S and formula F . Previously we have written A |= F
to say that an assignment A is a model of F .
The final concept we want to introduce is logical equivalence.

Definition 10 (Equivalence). Two formulas F and G are said to be logically equiv-

alent if A(F ) = A(G) for every assignment A. We write F ≡ G to denote that F and
G are equivalent.

5 Encoding constraint problems into satisfiability problems

In order to illustrate the concepts that we have seen so far, we are now going to
discuss how some well-known constraint problems can be encoded in propositional
logic, and how we can reason about them using our machinery.
The first problem that we encode into propositional logic is the well-known
Sudoku puzzle:

5
 2 5 1 9
8 2 3 6
3 6 7
1 6
5 4 1 9
2 7
9 3 8
2 8 4 7
1 9 7 6

For each i, j, k ∈ {1, . . . , 9} we have a proposition xi,j,k expressing that grid po-
sition i, j contains number k. Now build a formula F as the conjunction of the
following constraints:
• Each number appears in each row and in each column:
9 ^
^ 9 _
9 9 ^
^ 9 _
9
F1 := xi,j,k F2 := xi,j,k
i=1 k=1 j=1 j=1 k=1 i=1

• Each number appears in each 3 × 3 block:

9 ^
^ 2 ^
2 _
3 _
3
F3 := x3u+i,3v+j,k
k=1 u=0 v=0 i=1 j=1

• No square contains two numbers:

9 ^
^ 9 ^
F4 := ¬(xi,j,k ∧ xi,j,k0 ) .
i=1 j=1 1≤k<k0 ≤9

• Certain numbers appear in certain positions: we assert

F5 := x2,1,2 ∧ x1,2,8 ∧ x2,3,3 ∧ . . . ∧ x8,9,6 .

The formula F thus obtained is satisfiable if and only if the given Sudoku in-
stance has a solution. Some facts about Sudokus have not explicitly been included
in F . For instance, the property that no number appears twice in the same row,
i.e.,
9 ^
^ 9 ^
F6 := ¬(xi,j,k ∧ xi,j 0 ,k )
i=1 k=1 1≤j<j 0 <9

has not explicitly been stated. However, it can be verified that |= F → F6 . Though
redundant, explicitly adding F6 to F may help a satisfiability solver when search-
ing for a satisfying assignment. Note that the number of variables xi,j,k is 93 = 729.
Thus a truth table for the corresponding formula would have 2729 > 10200 lines!
Nevertheless a modern SAT-solver can find a satisfying assignment in millisec-
onds.
The second example we consider is that of finding a Hamiltonian path in an
undirected graph. Given a undirected graph G = (V, E) with vertices V and edges
E ⊆ V × V such that E is symmetric, the Hamiltonian path problem asks whether
there exists path in G that visits every vertex exactly once. Figure 2 illustrates
a Hamiltonian path in a graph. We now show how the Hamiltonian path problem
can be encoded into propositional logic. Given an undirected graph G = (V, E) such
that E ⊆ V × V is symmetric, for each vertex i, j ∈ {1, . . . , n} we have a proposition
xi,j expressing that vertex i is the jth vertex in the Hamiltonian path. Now build the
formula F as the conjunction of the following constraints:

6
 Figure 2: Example of a Hamiltonian path in an undirected graph.

• Each vertex is visited precisely once, and no two vertices are visited at the
same time:
n _
^ n n
^ ^
F1 := xi,j F2 := ¬(xi,j ∧ xi,k ) ∧ ¬(xj,i ∧ xk,i )
i=1 j=1 i=1 1≤j6=k≤n

• The path goes along edges:

n ^
^ n n−1
^
F3 := xi,j ∧ xk,j+1 → ei,k
i=1 k=1 j=1
^ ^
F4 := ei,j ∧ ¬ei,j
(i,j)∈E (i,j)6∈E

Here, the ei,j are additional propositional variables encoding the structure of G.
The graph has a Hamiltonian path precisely when F := F1 ∧ F2 is satisfiable.

6 The SAT Problem

A decision problem is a computational problem for which the output is either “yes”
or “no”. Such a problem consists of a family of instances, together with a question
that can be applied to each instance. A decision problem of prime importance
is the SAT problem for propositional logic. Here the instances are propositional
formulas and the question is whether a given formula is satisfiable.

6.1 The Complexity of SAT

The truth-table method for solving the SAT problem requires at least 2n steps in
the worst case for a formula with n variables, that is, it runs in no better than
exponential time. The proof system underlying modern SAT solvers can be seen as
a subsystem of the resolution proof procedure, which will be introduced later on.
These SAT solvers work well in practice, routinely determining (un)satisfiability
of formulas with hundreds of thousands of variables and clauses. However it is
known that resolution is also exponential in the worst case.
It is an open question whether there is an algorithm for deciding SAT whose
worst-case running time is polynomial in the formula size. In fact this question
?
is a formulation of the famous P = NP problem. It is even open whether there is
a sub-exponential algorithm for the SAT problem. By a sub-exponential algorithm

7
 √
we mean that the running time f (n) is 2o(n) , e.g., f (n) could be n600 , nlog(n) , n n , or
2n/ log(n) . In other words, it is not known whether or not we can do even a tiny bit
better than exhaustive search in the worst case!

6.2 Reductions to SAT

Many “hard” combinatorial decision problems can be reduced to SAT. A reduction
of a decision problem to SAT is an algorithm that inputs an instance I of the
decision problem and outputs a propositional formula ϕI such that ϕI is satisfiable
if and only if I is a “yes” instance.
Example 11. We consider the 3-colourability problem for graphs. Recall that an
undirected graph is a tuple G = (V, E) consisting of a set of vertices V and an
irreflexive symmetric edge relation E ⊆ V × V . If (u, v) ∈ E we say that vertices
u and v are adjacent. A 3-colouring of G is an assignment of a colour in the set
C = {r, b, g} to each vertex so that no two adjacent vertices have the same colour.
An instance of the 3-colouring problem is a graph G, and the question is whether
G has a 3-colouring.
We express the requirements of a 3-colouring in a propositional formula ϕG
that is derived from G. To define ϕG we first introduce a set of atomic propositions
{xv,c : v ∈ V, c ∈ C}. Intuitively xv,c represents the proposition vertex v has colour c.
We then encode the notion of a 3-colouring by the following formulas.
• Each vertex has at least one colour:
^ _
F1 := xv,c .
v∈V c∈C

• Each vertex has at most one colour:

^ ^
F2 := ¬(xv,c ∧ xv,c0 ) .
v∈V c,c0 ∈C
c6=c0

• Adjacent vertices have different colours:

^ ^
F3 := ¬(xu,c ∧ xv,c ) .
(u,v)∈E c∈C

Finally, we define ϕG := F1 ∧ F2 ∧ F3 . Note that it is straightforward to write a small

program that takes a graph as G input and outputs the formula ϕG . It is clear
that ϕG is satisfiable if and only if G has a 3-colouring and moreover a satisfying
assignment of ϕG determines a 3-colouring of G.
The idea of solving a combinatorial problem by reduction to SAT is that the SAT-
solver should do all the hard work. The reduction itself should be computationally
straightforward: at the very least it should be implementable by a polynomial-time
algorithm. For example, in the case of 3-colourability, given a graph G one can
produce ϕG by performing a single traversal of G.