Logic programming and solvers

Functional programming has become quite popular in the last decade. Most people’s attention is now on machine learning. What if I told you there was one last El Dorado, one last unexploited programming paradigm?

In this article, I will try to show the potential uses of logic programming and solvers:

Prolog on the case
How natural-language constraints can be translated into logic programming
Prolog’s algorithm
How the basic logic programming algorithm works
Solvers
How solvers can solve difficult problems
Unsatisfiable cores
How they can capture the intent of the user
Other uses
Further leads

Prolog on the case

We will imagine a situation, and see when you will find the answer. No publicly available AI, at the time of the publication, has been able to find the solution. Indeed, they excel in creative endeavours, but have trouble being logic and consistent. And that is where logic programming shines. Since large language models (LLM) can translate natural-language statements into logic code, they work synergetically.

For those who do not know Prolog, it looks like this:

It means: the fact parameterised by Parameter1, Parameter2 is true if condition1(...) and condition2(...) are true. I will translate the story facts into Prolog. Variables are capitalised. Now that this is done, let us investigate.

You are enjoying a stay in a manor with some guests. Only him and you have the key to the study room.

You decide to join him. The door being locked, you use your key and lock it again, once inside the dark room. Only the centre, where your friend is sitting, is lit and visible. However, when you go towards him, you realise that something is off: his key is lying at his feet, and your friend is holding a knife… stabbed in his chest. What has happened?

Running this code will download 11MB for Prolog.

There was only him in the room. A suicide? However, on closer inspection, you notice that the back wound is larger than the chest wound. However, the tip of the knife is thinner. The fatal wound was in the back…?

We are now sure there is a third party who killed your friend. What can we learn about him?

The killer is with you, in the room, and has certainly seen you.

This is the deduction no LLM could do. Let us see how Prolog could do it.

Prolog’s algorithm

This section supposes you know the basic Boolean algebra. You can skip it if you are more interested in the technological possibilities.

Here are the rules:

Prolog adds facts (clauses in our equations) with a conjunction ( $\land$ ).
It adds the negation of our query, and checks whether the total is false. Indeed, when you have a list of facts you know to be true, just adding the query is not helpful. Whereas, if you add its negation, and observe a contradiction, it means the original query is true.
Clauses are unified with the rule: $\left(A \lor B\right) \land \left(\lnot A \lor C\right) \rightarrow B \lor C$ . Indeed, $A$ is either $true$ or $false$ . When it is $true$ , $C$ is $true$ , since $\left(\lnot A \lor C\right)$ is $true$ . When it is $false$ , $B$ is $true$ , since $\left(A \lor B\right)$ is true. Therefore, $B \lor C$ is true.

Here is an example:

The translation into clauses (joined by $\land$ s) is:

$man\left( Socrates \right)$
$\forall x, man\left( x \right) \rightarrow mortal\left( x \right)$ (or in basic operators, $\forall x, \lnot man( x ) \lor mortal\left( x \right)$ )
$\lnot mortal\left( Mortal \right)$ ( $\lnot$ is the negation or the query, the source of the contradiction)

Then, Prolog proceeds by pattern matching, starting with our query. Since we also have the same pattern( $mortal$ ) in (2), and it starts with $\forall$ , we instanciate (2) with $x = Mortal$ :

$\lnot man( Mortal ) \lor mortal\left( Mortal \right)$

By combining (3) and (4), we obtain:

$\lnot man( Mortal )$

Finally, the last step to obtain the empty clause is to unify (5) with (1), with $Mortal = Socrates$ . That is how Prolog works.

There are many extensions to Prolog’s paradigm, such as a probabilistic version.

While natural language can easily be translated by a LLM to Prolog, the limitation of Prolog’s algorithm is that it must be able to instantiate a solution. What about harder problems? We will need sharper tools.

Solvers

Let us suppose we are building a wall (using just brick, without binder). The foreman shows you a brick and tells you:

As the bricks’ sides and the wall length are integers, I thought they would fit perfectly. I have tried to lay the bricks on all their sides, but every time, the last brick was 1 (cm/inch/arbitrary unit) too long! It would not have happened if the wall was shorter. Anyway, send the invoice for the wall’s length.

And then, he left. Suddenly, you realise: he did not tell you the length of the wall! It seems to be one of those impossible mathematical problems: “from the radius of the ring, deduce the date of the engagement”. The mathematician wizards among our readers may suggest the Chinese remainder theorem, but for those among us who are mere mortals, we might turn to a solver; here, Z3.

Z3 uses a strange syntax: the operator is always first, surrounded by parentheses. For example, instead of writing $a \lt b + c$ , you would write ( < a ( + ( b c ) ) ). Apart from this Lisp-y eccentricity, the language is closer to our day-to-day programming than Prolog.

Let us now study the brick he showed you. It has three different edges, and therefore, lengths:

In our example, the lengths are 3, 5, and 7. Therefore, the remainder of the division (mod) of the wall length by the brick’s sides (3, 5, and 7) is 2, 4, and 6. Let us write down all of this.

Running this will download 33MB of compressed dependencies. sat means that there is a solution.

Success: the length is 104! You can verify it by yourself. Z3 does not (always) need to instantiate a model, and uses much more powerful heuristics than Prolog’s algorithm. The downside is that it can lose itself easily, and needs guidance. More generally, keep in mind that you cannot:

Prove recursive facts.
Generate what might be function, in general. For example, generating an infinite array is analogous to a function, since it is a map from indices to values.

Unsatisfiable cores

Solvers are almost never used outside industrial contexts, but they can be useful even for mundane logic. Let us consider the current platform, Comment.

A deeper study of its principles can be found 🗺️here.

Let us consider the following tasks:

❶

To do

❷

To do

Imagine that the user has two lists open: one with the tasks to do (containing them), and another with the tasks done (currently empty). In functional UI frameworks like React, they are both a simple filter on the list of tasks.

Then, he drags both tasks to the list of tasks done. What should happen in the database?

Intuitively, it would change their status from ToDo to Done.
However, since the flow of data is unidirectional, we must leave the declarative functional paradigm and write an imperative handler: “when new tasks are dropped, find the conflicting tags (here, the status), and replace them by the tags of their new context (status = Done).”

Most apps are full of this duplicated logic: once in the view, and once in the handlers. Can we avoid it? Here is the example with Z3:

The result is consistent with what we want to be displayed. However, since the user dropped those tasks in the tasks done, let us add these contradictory assertions:

Z3 obviously finds that there is a contradiction: unsat. However, thanks to the option :produce-unsat-cores true, it also shows the assertions causing it: t1Status and t2Status. t1Name and t2Name can be kept.

Therefore, we can take the same code, remove t1Status and t2Status, and ask Z3 to infer the right values:

Aha: now, the status of these tasks is Done! We can update them in our database/store. So, the steps were:

Define the logic for separating the tasks among our lists
Assert that the lists are actually what the user has done
Update the conflicting records following Z3’s analysis

Therefore, we can avoid writing the handler by hand: Z3 will infer the intent of the user!

Other uses

Additionally, I believe logic programming and solver can be used for collaboration:

Masterpieces are the fruit of unique minds because they need a coherent design. However, by specifying their vision through constraints, creators can co-author a work.
In programming, it unlocks a new kind of collaborative architecture, made of modules:

Each module specifies a list of intents, and the solver ensures they will be met. Therefore, the collaborator does not have to read the whole codebase. The solver can find the contradictions (when a feature is updated, for example), and the updater must acknowledge it replacement. Adding a module will be safer, since the solver will list the overruled behaviours. To find the relevant modules to update, LLMs and vector databases will be useful.

Why are they not used more today, then? Unfortunately, performance is prohibitive for many real-time uses.

Exploration of the intersection between logic and day-to-day programming ranges from simple applications of a solver on top of an existing language to trying to combine them in a single language that handles recursion.