Propositional logic is an altogether easier logic than first-order logic. In propositional logic, we only have to deal with propositional variables, which are either true or false, and Boolean combinations of those propositional variables. There are no quantifiers to introduce horrible complexity or undecidability to propositional logic, and everything has a finite sort of character. Propositional logic is a neat little logic.
Despite that, there’s a surprising amount we can say and do in propositional logic, and a surprising number of reductions that can be done to propositional logic. Given that SAT (the problem of deciding whether a given propositional formula is satisfiable or not, i.e. whether a given propositional formula has a solution or not) is an NP-complete problem, it follows that a surprising number of problems are solvable in NP by a simple reduction to propositional logic. Since NP-complete problems are easy (well, easy relative to the problems found about first-order logic!), we have a good method to show that a given problem is easy (or easy enough).
Here I’ll have a look at some problems that we can formulate in propositional logic, and so solve by throwing a SAT-solver at the given problem. There’s nothing particularly groundbreaking here, but it’s fun to solve puzzles. So let’s solve some puzzles.
Graph problems
Given a graph, and an interesting property of graphs, does that interesting property hold of our graph? Since whether or not there’s an edge between any two vertices $u$ and $v$ can be expressed as a proposition formula $e_{u,v}$, we can formulate properties of given graphs in propositional logic, and use our SAT-solvers to show whether they’re true or not.
We have to be careful here; since we’re working with propositional logic, we can’t say anything about the properties of infinite graphs (or, at the very least, we can’t say anything about anything more than a finite subgraph of an infinite graph), and we can’t make general claims about all graphs from within propositional logic. Since each propositional variable can only make claims about given vertices and given edges, we have to have a graph given to us in the first place, and so our propositional formulae can only hold over given graphs.
Still, we can write nice general forms of these formulae using indexed conjunctions and disjunctions, and so let’s see some of the properties of graphs that we can formalise in this way.
Paths
Given a (directed) graph $G$ and two vertices $u$ and $v$, is there a path from $u$ to $v$ in $G$? So long as we’re given a graph that’s only finite, we can formalise this problem in propositional logic.
To solve it, for every graph $G$ and vertices $u$ and $v$, we construct a propositional formula $\path{u}{v}$, which is true iff there exists a path from $u$ to $v$ in $G$. Note that we can’t write down a single formula that, when given a graph $G$ and vertices $u$ and $v$, expresses that there’s a path from $u$ to $v$; even if we move to first-order logic, we can show that there’s no such single formula using Ehrenfeuct-Fraïssé games.
In any case, let’s take our graph $G$ and write down our formula $\path{u}{v}$. For this, we define for each vertex $w$ a propositional variable $p_w$ that we want to be made true iff $w$ is part of a path from $u$ to $v$. We’ll want any satisfying valuation of our formula to encode a path from $u$ to $v$, and so any satisfying valuation will encode a path from $u$ to $v$. We’ll use the power of shorthand to write the formula down.
We define inductively on the length of the path we want to find. When that length is zero; we know that $u$ and $v$ must be the same vertex; there’s no path of length zero between any two distinct vertices. So we write:
\[ \path{u}{v}^0 \defeq \biggl\{\begin{align*}\top & \text{ if $u = v$}\\ \bot & \text{ otherwise}\end{align*} \]
where $\top$ is your favourite propositional tautology (e.g. $p \or \neg p$) and $\bot$ is your favourite propositional contradiction (e.g. $p \and \neg p$). The above means that $\path{u}{v}^0$ comes out true iff $u$ is equal to $v$.
We then, inductively, define paths of length $k+1$ between $u$ and $v$ by appeal to there being a path of length $1$ between $u$ and some vertex $u’$, and a path of length $k$ from $u’$ to $v$:
\[ \path{u}{v}^{k+1} \defeq p_u \and \bigvee_{\tuple{u,u’} \in E} (p_{u’} \and \path{u’}{v}^k) \]
where $E$ is the set of edges of the graph $G$.
Now, because any propositional formula must be of only finite length, we can’t just appeal to there being some $k$ for which $\path{u}{v}^k$ holds and call that our general $\path{u}{v}$ formula; there are infinitely many $k$ to quantify over and we only have finitely much space to write down our formula in. But we do know that, in a graph of size $G$, there’s a path between two vertices $u$ and $v$ only if there’s a path of size at most $\size{G}$ between two vertices $u$ and $v$, where $\size{G}$ is the number of vertices that appear in $G$. So we only have to quantify over $\size{G}$ many of our path formulae to get our general path formula.
So we set
\[ \path{u}{v} \defeq \bigvee_{g \leq \size{G}} \path{u}{v}^g \]
and we have the formula we wanted from the start. $\path{u}{v}$ comes out true iff there’s a path of length $g$ from $u$ to $v$, where $g$ is less than the size of $G$, and that comes out true iff there’s a path from $u$ to $v$ at all. So we’re done.
Cliques
Given a (directed) graph $G$ and some number $k$, does the graph $G$ contain a clique of size $k$? We can solve this problem by formalising it propositional logic. Here, a clique of a graph $G$ is a set $C$ of vertices of $G$ where, for any two vertices $u$ and $v$ in $C$, there exists a path from $u$ to $v$ in $G$, and there exists a path from $v$ to $U$ in $G$. Basically, in a clique we can always travel between any two vertices.
To reduce the problem of whether or not a formula has a clique to a propositional formula, we introduce a propositional variable $p_v$ for each vertex $v$ of the given graph $G$. We intend to read a clique of size $k$ off of any satisfying valuation of our formula, and so each propositional variable $p_v$ will come out true in a valuation iff that valuation defines a clique of size $k$.
For this, we define the propositional formula $C$:
\[\begin{align*} C \defeq &\bigwedge_{u \in V} \bigwedge_{v \in V} ((p_u \and p_v) \implies \path{u}{v})\\&\and \bigvee \set{\bigvee_{u \in U} p_u | \size{U} = k} \end{align*}\]
where $\path{u}{v}$ holds iff there’s a path from $u$ to $v$. Since we’ve been given the graph $G$, we know we can formalise $\path{u}{v}$ here as we did above, by using additional propositional variables.
What the above formula expresses in the first conjunct is that for any two vertices $u$ and $v$, if $u$ and $v$ are both in the same clique, then there exists a path between them. In the second conjunct, the above formula expresses that any such clique is of size precisely $k$. So any valuation that satisfies the formula $C$ sets precisely $k$ propositional variables $p_v$ to be true, where there’s a path between any two vertices in that set. So the formula $C$ is satisfiable iff it has some clique of size $k$, as we wanted.
Sudoku
Given an $n \times n$ sudoku board with some squares filled out, is there a solution that can be reached starting from that board? Well, let’s find a good propositional representation of the problem, and in doing so lead the way to using a SAT-solver to solve the problem.
Let’s say that the objects we’re working over in this problem are positions on the sudoku board, and that for each position we have a propositional variable $p^m_{x,y}$ that holds iff there’s a number $m$ written in the position $\tuple{x,y}$. Of course, this is only meaningful if precisely one number can be placed in any given square, and so we enforce these by writing some propositional formulae. First we specify, using the formula $S_1$, that every square has some number written in it:
\[ S_1 \defeq \ \bigwedge_{1 \leq i \leq n} \bigwedge_{1 \leq j \leq n} \bigvee_{1 \leq m \leq n} p^m_{i,j} \]
and then we specify, using the formula $S_2$, that every square has at most one number written in in:
\[ S_2 \defeq \bigwedge_{1 \leq i \leq n} \bigwedge_{1 \leq j \leq n} (\bigwedge_{1 \leq m \leq n} \bigwedge_{\substack{1 \leq m’ \leq n \\ m’ \neq m}} \neg(p^m_{x,y} \and p^{m’}_{x,y})). \]
With these, we know that any valuation of the propositional variables $p^m_{x,y}$ that satisfies $S_1$ and $S_2$ will assign to each square precisely one number. We now want to write propositional formulae that enforce the rules of sudoku, namely that in each row, column and three-by-three square there is precisely one of each of the digits $1–n$.
Let’s first write a formula that enforces there being only one of each digit per row:
\[ S_3 \defeq \bigwedge_{1 \leq i \leq n} \bigwedge_{1 \leq j \leq n} \bigwedge_{1 \leq m \leq n} (p^m_{i,j} \implies \bigwedge_{\substack{1 \leq i’ \leq n \\ i’ \neq i}} \neg p^m_{i’,j}) \]
and, similarly, a formula that enforces there being only one of each digit per column:
\[ S_4 \defeq \bigwedge_{1 \leq i \leq n} \bigwedge_{1 \leq j \leq n} \bigwedge_{1 \leq m \leq n} (p^m_{i,j} \implies \bigwedge_{\substack{1 \leq j’ \leq n \\ j’ \neq j}} \neg p^m_{i,j’}). \]
Finally, we write a formula that enforces there being only one of each digit per three-by-three box:
\[ S_5 \defeq \bigwedge_{1 \leq i \leq n} \bigwedge_{1 \leq j \leq n} \bigwedge_{1 \leq m \leq n} (p^m_{i,j} \implies \bigwedge_{i’, j’ \in f(i,j)} \neg p^m_{i’,j’}) \]
where $f$ is a convenient function that, when given a position on the board $\tuple{i,j}$, returns the set of all other positions in the same three-by-three box as the position $\tuple{i,j}$. Using a bit of modular arithmetic it shouldn’t be too hard to define $f$.
Taking the conjunction of all of $S_1$ through $S_5$, we get a formula where any satisfying valuation of that formula encodes a filled-out legal sudoku board. Finally, if we already have some squares that are filled in and want to know whether there exists a legal sudoku board with those positions filled in, we just add to our final formula propositions $p^m_{x,y}$ for each of the filled-out squares $\tuple{x,y}$ with the digit $m$ in them.
We’ve now found a way to solve sudoku puzzles by encoding them as propositional formulae and checking whether they’re satisfiable. This is good.
Chess problems
Given a chessboard, is the white player in checkmate or not? That’s another problem that can be reduced to a propositional formula, and so it’s a problem that admits a nice logical formulation. Let’s write down that formulation here.
Here we’ll define a proposition $\piece{x}{y}$, for each chess piece, which holds iff one of those pieces is in square $\tuple{x, y}$ of the board. We’ll use the unqualified proposition $\piece{x}{y}$ to just mean that there’s any piece at all in the square $\tuple{x,y}$; we can treat it as an implicit disjunction over all other piece types. Let’s assume we’re working on a standard eight-by-eight board.
Let’s first formalise the proposition that the white king is in check. For this I’ll assume that there’s one and only one white king on the board, but otherwise I won’t make requirements on the number of other pieces that appear on the board, or the possibility of reaching such a position from the starting position. I take it that the white king is in check even if that’s because it’s surrounded by eight black kings.
We first formalise that every square has at most one piece on it by writing:
\[ \mathrm{sensible} \defeq \bigwedge_{1 \leq x \leq 8} \bigwedge_{1 \leq y \leq 8} \bigwedge_{p \in \mathrm{Pieces}} p_{x,y} \implies \bigwedge_{p’ \neq p} \neg p_{x,y}. \]
That enforces that, if one type of piece is on a square, then no other type of piece is on that square. We don’t want to enforce that every square has a piece on it—that would be a very cramped game of chess!—and so we skip that formula here, unlike we did in the sudoku case.
We then go over the pieces of the board and see whether any pieces of that kind are putting the white king in check:
\[\begin{align*} \mathrm{check}_{x,y} \defeq &\phantom{\vee} (\pawn{x-1}{y-1} \or \pawn{x+1}{y-1})\\&\or(\rook{x-1}{y} \or (\rook{x-2}{y} \and \neg \piece{x-1}{y}) \or \dots )\\ &\or(\bishop{x-1}{y-1} \or (\bishop{x-2}{y-2} \and \neg \piece{x-1}{y}) \or \dots)\\ &\or(\knight{x-1}{y-2} \or \knight{x-2}{y-1} \or \dots)\\ &\or(\queen{x-1}{y-1} \or (\queen{x-2}{y-2} \and \neg \piece{x-1}{y-1}) \or \dots)\\ &\or(\king{x-1}{y} \or \king{x-1}{y-1} \or \dots).\end{align*}\]
We’ll assume that if a square is off the board, then there’s no piece on it; this helps us avoid tricky edge cases depending on the position of the white king.
We’ve formulated whether or not the white king is in check. Now we need to formulate whether or not the white king is in checkmate. To do this, we iterate over each of the moves that the white king could make, and check whether that move is even possible and whether the white king would still be in check even if that move was made.
\[ \checkmate{u}{v} \defeq \mathrm{sensible} \and \check{u}{v} \and \bigwedge_{\substack{\tuple{x,y} \in X\\ \neg \textrm{white-piece}_{x,y}}} \check{u}{v}[\bot/\pawn{u}{v}, \bot/\rook{u}{v}, \dots, \bot/\king{u}{v}]. \]
The qualification under the indexed conjunction makes sure we’re only looking at pieces that the white king can move to; as in, those positions where there isn’t a white piece. The body of the indexed conjunction makes sure that the white king would be in check in each of these positions as well. The bit in square brackets is a substitution of $\bot$ for any piece that’s in that square; we do it to delete any black pieces on the square the white king moves to (since the white king takes the piece in that case).
Our formula $\checkmate{u}{v}$ is therefore satisfied just when, for each position $\tuple{u,v}$ the white king is either in or can move to, the formula $\check{u}{v}$ is satisfied. The formula $\check{u}{v}$ is satisfied just when, in the next turn, a black piece can take the white king in position $\tuple{u,v}$. So the formula $\checkmate{u}{v}$ comes out true on a board just when the white king in position $\tuple{u,v}$ is in checkmate.
Of course, this formula makes most sense when we’ve already provided a set of propositional variables denoting the positions of various pieces on the board; without that, the formula $\checkmate{u}{v}$ comes out satisfiable just when there’s any way to checkmate a white king on the square $\tuple{u,v}$. Given that we can always surround the king with queens and get this effect, it’s not interesting to know whether there’s a position that can checkmate the white king at all. So we do need a bit of extra information on which propositional variables are true to find out whether or not the white king is in checkmate.
Tricks and technical devices
Throughout we’ve used a few tricks and technical devices to solve similar problems. These tricks are nice in that they have a logical flavour to them. Let’s look at a few of them here.
Emulating properties
We can’t say that given objects have given properties in propositional logic; we don’t have any way of talking about objects or properties in the language of propositional logic, only propositions. But first-order propositions either hold of objects or they don’t. So whether or not a proposition holds can be defined as a Boolean variable, and Boolean variables are just what propositional logic is good at talking about.
Because of this, given a collection of objects $x_1, x_2, \dots$ and some property $P$, we can define propositional variables $P_1, P_2, \dots$ where $P_1$ is true iff $P$ holds of $x$.
Similar notation lets us talk about relations holding over objects as well. We can write $R_{x,y}$ to be a propositional variable that holds iff $R(x,y)$ holds i.e. iff $x$ relates to $y$ by relation $R$.
Further, if we have only finitely many objects and only finitely many properties that hold over those objects, then we have only finitely many different ways for those properties to hold over those objects. That is to say, given a collection of objects $x_1, \dots, x_n$ and some property $P$, there are precisely $2^{n}$ different ways for $P$ to hold over the collection of objects $x_1, \dots, x_n$.
Since we have only finitely many ways for a property to hold over a finite number of objects, we can apply our next trick to emulate quantifiers over that domain.
Emulating quantifiers
We can’t introduce the arbitrary quantifiers $\exists$ and $\forall$, since we’re not working within first-order logic. But, given a finite collection of objects we’d like to quantify over (say, vertices of a graph or positions of a board), we can still emulate quantification over that collection in propositional logic, using the indexed conjunction $\bigwedge$ and indexed disjunction $\bigvee$ operators.
Note that the indexed conjunction and indexed disjunction operators aren’t part of the syntax of propositional logic, but are really just shorthands to avoid us having to write the normal conjunction $\wedge$ and disjunction $\vee$ symbols over and over again. So long as we have finite bounds for our indexed conjunction and indexed disjunction operators, it’s legitimate to use them when writing down propositional logic formulae.
Using the emulation of properties above, we can quantify over finite domains and talk about the properties that hold over finite domains. For instance, if we have a collection of objects $x_1, \dots, x_n$, and we want to enforce that property $P$ holds on each of those objects, then instead of writing $\forall x\ P(x)$ we write $\bigwedge_{1 \leq i \leq n} P_{x_i}$. Similarly, if we want to enforce that property $P$ holds on some of those objects, then instead of writing $\exists x\ P(x)$ we write $\bigvee_{1 \leq i \leq n} P_{x_i}$.
We can build up from this and write about arbitrary Boolean combinations of atomic formulae about quantified variables holding, using our emulated quantifiers and emulated properties. For instance, if we’d like to translate the first-order sentence over the finite domain $D$
\[ \forall x\ (\exists y\ R(x,y) \implies P(x)) \]
into propositional logic, then we’d just write
\[ \bigwedge_{x \in D} ((\bigvee_{y \in D} R_{x,y}) \implies P_x). \]
The surface logical form has been preserved by our emulated properties and emulated quantifiers, and so we have a neat translation from first-order formulae over finite domains to propositional formulae.
Solving easy problems
We know that the satisfiability problem for formulae in DNF (disjunctive normal form, where formulae are disjunctions of conjunctions of atomic formulae) is solvable in polynomial time; given such a DNF formula, we just iterate over each clause, and check whether each clause is satisfiable or not. If some clause is, then the whole formula is. Since a conjunction is satisfiable precisely when each of its conjuncts is, we just need to check that no propositional variable appears both positively and negatively in the same conjunction to check if that conjunctions is satisfiable or not.
Using our emulated quantifiers, we can therefore see when some problems are solvable in polynomial time. Any formulae of the form $\bigwedge_{i \in I} p_i$, $\bigvee_{i \in I} p_i$ or $\bigvee_{i \in I} \bigwedge_{j \in j} p_{i,j}$, for propositional variables $p_i$ and $p_{i,j}$, are formulae in DNF. Indeed any formulae of the form $\bigvee^* \bigwedge^* p$, where the star $*$ is understood as repeated iteration and $p$ are some propositional variables, comes out as a DNF formula. Hence satisfiability problems that can be reduced to formulae of this form in polynomial time are themselves polynomial time solvable. So we have a way of reading off the complexity of a problem from the logical form (or at least, our shorthand for that logical form) of the formula that represents it.
Conclusion
We’ve gone through some problems and puzzles that can be formulated in propositional logic, and in doing so have reduced solving those problems to SAT, the propositional satisfiability problem. There are more problems that can be reduced in this way, but for these we can use the techniques we’ve looked at so far to solve them. Propositional logic thus turns out to be quite handy.