Part 3 - DPLL, CDCL and DPLL(T)

We looked at the terminology and a few rules in the last chapter, only to find it too hard to follow.

In logic, reasoning by rule is usually more interesting. However, there is time when we have to test every combination of truth values to see if a statement is satisfiable.

Before we find out how such an exhaustive search can be done, let’s first introduce the CNF of logic statements.

“CNF” stands for “conjuctive normal form”, in which

• a statement consists of various “clauses” connected by “and”
• inside the clauses, literals are connected by “or”
• a literal is either a variable or its negation

What does that remind you of?

It is possible for you to look at how a SAT problem is presented, as well as its difficulty, at The SAT Game.

As we see before, “and”, “or” and “not” can represent all kinds of relations. Here we take a step further and think every statement in propositional logic can be represented in such three levels. There are some ways to convert any kind of propositional logic statements, even more general problem statements, into a CNF, and …

Good point. There are general ways to convert things to those forms, but generally a hard problem in daily life comes with constraints that should all be met, and CNF is more close to such a problem.

In nature however, this derives from the hard core of computational complexity.

Computation… Computers! Do you see some connections between electronic computers and our satisfiability problem?

Good. Computers have not only switches but also gates, which can calculate all kinds of operations like “and”. It is sometimes amazing, though, that satisfiability solvers help computer chip design. Metaphorically, I see this as the species of computer breeding offsprings.

As to computer aided reasoning, or “automated reasoning”, they are not so mature as to solve hard puzzles for us, but they are evolving.

Computers usually view problems naively. For example, $3 \times 4 \times 5$ is two multiplications, while $3 \times 20$ is one, and complex functions are also built on top of additions and multiplications, which takes a fixed amount of time per operation. As a result, we only calculate the operations they need to perform as a rough estimate of the run time.

So, if modern satisfiability solvers, as computer programs, does not rely much on syntactic reasoning, how do they solve a general problem?

The core idea in this is called “search”, which is also a major topic in any kind of computer programming books.

Let’s stick to the example in chapter 1, exploring only the truth values of 3 kid’s statements.

In our puzzle, there is only one truth value combination that can satisfy the requirements. To find the combination, we need to enumerate every possibility.

So far that’s right. However, the number of combinations grows as we add more variables. For 2 variables, the computer enumerates 4 possibilities; for 3 variables, it enumerates 8. And the possible combinations become too many to enumerate, even for powerful computers.

But modern solvers is capable of dealing with hundreds of variables and thousands of clauses, even in the worst case. How can it be?

Well, what we previously do (enumerating everything and evaluating them) is called brutal force search. Imagine troopers breaking into your house and turn it upside down!

However, it’s not the case that we humans will search every place for a pair of lost keys, right? We always have some intuition about where to find things. And some folk managed to teach computers to do that! It’s called heuristic search.

That makes sense. But we have another choice! Instead of a piece of information per every possibility, we give the computer some way to decide the information itself.

…PICS…

As I have said, we have many clauses to satisfy. Once all clauses becomes true, we are done. We imagine that the number of true clauses is some indicator, just like the progress bar in your downloader!

We instruct the machine to stay in one combination, look at its neighbors, and pick up the best one to live in! Ideally, the satisfied clauses adds up, and finally everything is fine.

That sort of search, we often call “local search”, only checks a “local” property. That is, some combinations that live together. It knows very little about the general information, and yet it is powerful enough for many problem sets.

Of course, there are harder problems. Imagine searching for a purloined letter, while the dumb policemen only knew to waylay the minister! We have to rely again on reasoning, though in a structured manner.