Logical Encoding

Logical encoding is the process of transforming a problem (algorithmic problem or otherwise) into a series/system of logical statements (either in propositional logic or predicate logic). Solving the encoding is equivalent to solving the actual problem. Similarly, if the encoding is unsatisfiable, then there is no solution for the problem.

A benefit of logical encoding is that it allows much faster solving, such as by using logic solvers.

Examples §

Example: Map Colouring Problem

The map colouring problem can technically be brute-forced by a system of logical statements in propositional logic Take a very small area consisting of very few regions. For example, take an area consisting of only 3 regions (or a map of 3 states)
%%🖋 Edit in Excalidraw, and the dark exported image%% We know that we would need at most 3 colours to colour this area (since it has only 3 regions). Let’s pick Red, Green and Blue as our colours. Then, since region A must be coloured, we know that:

$$(\text{A is Red})\text{ OR }(\text{A is Green})\text{ OR }(\text{A is Blue}{)}^{\ast }.$$

#tosee does it need to be xor or is the constraints enough to satisfy that we don’t get a region coloured with 2 colours at once? Similarly, we can apply this constrain to all our regions, by making sure our condition above applies to A and B and C

$$\begin{array}{rl}& [(\text{A is Red})\text{ OR }(\text{A is Green})\text{ OR }(\text{A is Blue})]\\ \text{ AND }& [(\text{B is Red})\text{ OR }(\text{B is Green})\text{ OR }(\text{B is Blue})]\\ \text{ AND }& [(\text{C is Red})\text{ OR }(\text{C is Green})\text{ OR }(\text{C is Blue})]\end{array}$$

Then, we can start adding more constraints. We know that because $A$ and $B$ are connected, they must have different colours (by definition of the map colouring problem). Hence, we must NOT have A being red and B being red. Again, we can extend this logic to all the colours:

$$\begin{array}{rl}& \text{NOT (A is Red AND B is Red)}\\ \text{AND }(& \text{NOT (A is Green AND B is Green)})\\ \text{AND }(& \text{NOT (A is Blue AND B is Blue)})\end{array}$$

And to our other region-pair, B-C

$$\begin{array}{rl}& \dots \\ \text{AND }(& \text{NOT (B is Red AND C is Red)})\\ & \dots \\ \text{AND }(& \text{NOT (A is Red AND C is Red)})\end{array}$$

Finally, combining all our logical statements, and converting them into their respective logical connectives, we get our encoding:

Final Encoding

\begin{align} &[(\text{$A$ is $Red$}) \lor (\text{$A$ is $Green$}) \lor (\text{$A$ is $Blue$})] \\ \land \ &[(\text{$B$ is $Red$}) \lor (\text{$B$ is $Green$}) \lor (\text{$B$ is $Blue$})] \\ \land \ &[(\text{$C$ is $Red$}) \lor (\text{$C$ is $Green$}) \lor (\text{$C$ is $Blue$})] \\ \land \ &[(\text{$C$ is $Red$}) \lor (\text{$C$ is $Green$}) \lor (\text{$C$ is $Blue$})] \\

\land &[(\lnot\text{($A$ is $Red\wedge B$ is $Red$)}) \land \lnot\text{($A$ is $Green\wedge B$ is $Green$)}) \land \lnot\text{($A$ is $Blue\wedge B$ is $Blue$)})]\ \land &[(\lnot\text{($B$ is $Red\wedge C$ is $Red$)}) \land \lnot\text{($B$ is $Green\wedge C$ is $Green$)}) \land \lnot\text{($B$ is $Blue\wedge C$ is $Blue$)})]\

\end{align}

If we can satisfy this super long statement, we know our problem has a solution. In other words, if the logical encoding is satisfiable, then we know there exists a solution to the original problem. Some solutions:

• A is red, B is blue, C is green
• A is red , B is blue, C is red
• …

#todo Sudoku encoding