Okay

welcome to the last AI lecture in 2025.

As announced

we will try for our remaining two quizzes in the last minutes of the lecture.

So we're going to start the quiz at 9.36 if all goes well.

So please make sure that I've stopped the lecture before that.

I know some of you who are here actually are very good at doing this or so.

So helps that we actually get everything organized.

So we're talking about SAT solvers.

SAT solvers being computer programs that,

given a formula of propositional logic

tells you this formula is satisfiable.

And by the way

the satisfying variable assignment is the following.

Or it tells you it's unsatisfiable.

The first one is relatively unproblematic because given the satisfying assignment

we can just apply it to the formula

grind the mill

and then if anything but true comes out in the end

we can play.

Now

the other outcome

namely unsatisfiable

is much more unsatisfactory in a way.

Because we have to trust the program to say

I've tried everything I did

I didn't find anything so far so good.

But does that also mean that there isn't one?

And so that's very difficult to verify.

We speak of certain decisions having certificates.

Having a certificate means the program returns something that we can then use to verify the claimed result.

But unsatisfiable just doesn't give us a certificate

which means we have to trust maybe a huge mountain of code.

And we know that people make mistakes.

And so we would like to have something more there.

And that's one of the things we're going to talk about today.

So we've looked at the quintessential SAT solver

the dominating approach nowadays

and it's a very simple algorithm.

And rather than looking at the code again

I would like to go through two examples that actually show you pretty well what we're doing.

We have two kinds of subprocedure.

One is unit propagation.

Think that is the kind of what we're doing with inference.

We're propagating knowledge we already know.

The idea there is that we pick a unit that allows us to fix a value in the assignment

and then we use that to simplify.

The procedure we looked at there is clause simplification.

That means many of the clauses can be dropped outright.

And the other kinds of clauses that contain the opposite of the literal we are concentrating on right now can be dropped from the clause.