The kind of space of programs that do propositional inference we call SAT solvers.

SAT solvers are extremely useful. They can do more than just wumpus.

Satisfiability checking is the first problem where we found out that the problem is NP-hard,

which means, which essentially means everything takes exponentially long. Proofs are exponentially

long typically. But on the average you can actually do very, very well. So there's a

whole community who builds programs that decide the satisfiability of propositional formulae.

And there are other communities who build translators into propositional formulae like

wumpus. So wumpus is a good example. You have a problem. You don't really know how to solve

it via inference. But you have a clever idea how to turn this into a propositional formula.

And then you hit it with the big stick, which is you hit it with a SAT solver. And the SAT

solver tells you unsatisfiable or satisfiable. So if we had one of those, we could actually

do not just wumpus 4 times 4, but say wumpus 400 times 400. That's a big formula. And if

you have a good SAT solver, that will still very quickly tell you satisfiable or unsatisfiable.

And that's all the agent needs. And that's something that is done routinely. For instance,

when the US invaded Iraq, when was that, 10 years ago? They had a big planning problem.

For every tank, for every rifle, for every soldier, you had to plan where do we want

this guy or piece of equipment at what time, and how does it get there, given that we only

have finitely many helicopters and planes and ships and all of those kind of things.

So a logistical nightmare. And what they did was they used an industrial strength planning

system. And that planning system actually wrote down all the constraints that it could

find that the generals had probably given, plus all the knowledge about the terrain that

if you want to go from Virginia to Iraq, you have to cross the seas, so you need a ship

or an airplane. You can't just drive there, those kind of things. And this planner then

internally translates it into a big propositional formula. And then a SAT solver comes and says

yes or no. And that's how they did it. And that's one of the standard ways of doing it.

And that's kind of the standard way you attack any problem if you don't know how to solve

it. And you have the hunch it's probably something with inference. What you do is you try to

translate it into propositional logic, hit it with a big stick. So there's a community

that builds these SAT solvers. They meet once a year and meet around big problems, a million

propositional variables. And then they see who can solve the most problems the fastest.

And if you are doing a PhD in that area, you probably want to win that competition. And

of course if you have a good system, then the US military says, well, we would like

to talk to you. And you never hear about these people again.

And I want to kind of go briefly into SAT. And one of the things you should notice is

that SAT is actually the same as constraint satisfaction. You can actually think of a

propositional formula as a long list of values that you have to do. Every single little literal

formula is actually an assignment. Those are binary constraints. And every long formula

is just a multiple constraint between many variables. So SAT is actually a very special

kind of CSP. And now you could say, oh, that's easy, wonderful. We know how to do a CSP solver,

so we can do SAT solving by translating into a CSP. It's been done, but CSPs as SAT solvers

haven't been successful in that competition for 30 years now. When I started my PhD, you

could do these kind of things. Now they've gotten just much too good. But sometimes it's

interesting to know these. And the other way is also true. You can translate any CSP into

a SAT problem and solve it that way. And sometimes that's the best we can do, but not in that

case. Other things, hardware verification is something that goes wonderfully with SAT.

You have a propositional, you remember a circuit. You can have in any kind of a node there, you

can have voltage or no voltage. Very clearly a propositional variable. And then you have

rules that tell you what these kind of gates do. They could be flip-flops, they could be

AND gates or gates and so on. And you can actually, if you have only AND or NOR, the

gates for sequential logic circuits, you can just directly unroll this thing into a propositional