that a formula is unsatisfiable. Should we simply trust that as a fact? Well, no, I don't think that's a good idea. There's lots of possible ways a SAT solver could have errors in it, either algorithmic or programming, and having it simply say a formula is not satisfiable really isn't enough, especially when used in an area

such as formal verification. What we'd rather have it do is generate a proof of unsatisfiability, meaning something that could be checked automatically with a very simple checking program. So this proof should consist of a series of very small steps, each of which can be evaluated

according to some rules in a logical framework. This program should be simple enough that we can understand it and perhaps even formally verify it. Our work relies heavily on work that was published in 2006 by Karsten Zintz, Armin Bierhe, and Tony Usula,

where they showed that it was a very natural thing to incorporate proof generation in an extended resolution framework into a B2D-based SAT solver. Our contribution then 15 years later is to increase the use of existential quantification,

which as we'll see is a big impact on the performance and capability of a SAT solver. We represent formulas as in conjunctive form as a set of causes, each of which is a disjunction of variables or their compliments, also known as literals.

And we'll use the bottom symbol to represent the empty cause, meaning logical faults. Our rules are based on the resolution principle, which is a simple mechanical way of generating a new cause that's implied by two existing causes. So causal proof consists of a sequence of causes,

starting with the input causes and then followed by derived causes, each of which follows by resolution from a previous input cause as well as possibly derived causes. If we can reach the point where we have an empty cause then, what we've proved

is that the original set of input causes has a conflict, it's unsatisfiable. Extended resolution lets us introduce extension variables that become shorthand for formulas over the other variables in the formula. In particular, we introduce a set of defining causes

which encode a constraint of the form E if and only if F where E is our extension variable and must be a variable that has not occurred previously in the proof. We can now use E as a shorthand for F and through repeated application,

this can actually reduce the size of the proof exponentially. So imagine we wanted to prove these four constraints are unsatisfiable with the strategy of introducing extension variable to encode the formula U and V with these defining causes.

Then our extended resolution proof would look like before that we have a sequence of causes but they can include defining causes and the derived causes can be based on input causes, defining causes, as well as earlier derived causes. Again, we reached the empty cause

and that indicates that the original set of input causes is unsatisfiable. We make use of binary decision diagrams which are a way of representing a Boolean function as a graph and have a lot of nice properties. The main algorithms that we'll use on it are the apply algorithm, which given two BDDs in a coding functions F and G

and some Boolean operation say and or, generate the BDD representation of the conjunction or disjunction of these two functions. We'll also make use of existential quantification where given a function, again, represented by a BDD

and a set of variables X, we quantify out those variables, project them out so that the resulting function does not rely on any of these variables. Let's follow a little bit of detail about the apply algorithm since we'll use this as part of our proof generation. So the apply algorithm operates recursively

and imagine at some point in its operation, we reach a point where we have two root nodes, U and V and we want to form their conjunction. Then what we'll do is we'll recursively call this algorithm on the two pairs of children according to variable X being one or zero.

And each of those will return a result node, in this case, W one and W zero. And then we add a new node to the BDD that has those two nodes as children and the variable X as its defining variable. To generate extended resolution proofs,

what we'll do is we'll introduce a new extension variable for every node in the BDD. And as notation, we'll use the same symbol for the node name as for its extension variable. So for example, if nodes U has children, U one and U zero, our defining clauses are over the associated extension variables,

defining what constraints on the value of U as a variable as a function of its child nodes, U one and U zero, as well as on the variable X. We'll modify the apply algorithm so that when we compute a conjunction,

we not only return a node, but we also generate a proof that the extension variables associated with the arguments, U and V imply the extension variable associated with the result W. And this proof will follow the recursive structure

of the apply algorithm. So imagine we've done this before that we recall these recursively on the two sets of children nodes. And then each of those will return proofs, again, in terms of extension variables that U one and U V one implies W one and U zero and V zero imply W zero.

And now we can take the defining clauses for nodes U, V and W and combine those with the recursively computed proofs to generate a proof of the final result that U and V, again, their extension variables imply W.

Quantification is a critical operation for getting good performance out of the BDD-based SAT solver. And it's a little bit tricky to actually step through the detailed logic of this algorithm and generate a proof, but we don't actually need to.

All we need to do is show that it preserves implication. That is, if we quantify some node U in terms of variables X and produce a node W, that their associated extension variables will obey U implies W. And there's a simple algorithm for this that traverses the two graphs for nodes U and W

are similar to the apply algorithm. So let's combine this into our overall SAT solver and proof generation. We're given input variables and a set of causes of those variables, and we want to prove that those causes are unsatisfiable. Well, the standard technique using BDDs

is we'll introduce a variable, a BDD variable for each input variable, and we'll encode each cause as a BDD by disjuncting their literals. And then at the top level, we will do successive conjunction

and quantification operations. And if the input causes are unsatisfiable, we'll all eventually reach a case where we generate the leaf value zero, indicating that the formula is not satisfiable. Along the way, we'll generate a proof. What we'll do is for each BDD we generate

with some root node U, we'll prove that the set of input causes logically entail that that extension variable for U holds. And this starts with each of the input causes C will generate a proof that it entails

its corresponding root node U via a very simple proof based on the structure of that BDD. And then for the conjunction and quantification operations, we'll make use of these recursively computed results to assemble this into a series of proofs as I've described.

And once we reach the case of constant zero, that has associated with it, the empty cause. And so we've generated a proof that the input causes logically imply the empty cause. We've implemented this with a program all written in Python and available on GitHub.

We've used a number of benchmarks and each one we generate the formulas in terms of CNF files, but also at a specific ordering of the variables for the BDDs and a file that determines what order we should apply the conjunction and quantification operations.

Let me demonstrate this for the mutilated chessboard problem, a well-known problem in propositional reasoning. The idea is to take an end-to-end chessboard and remove two diagonally opposite corners. And then we're given a set of dominoes, each of which can cover two squares and ask, is there a tiling of this board?

And the answer is no, of course, because there's more white squares than black squares on this chessboard. So it's simple for us to say, but to actually represent that as a proof purely in resolution requires a proof of exponential size. This is a very easy problem to encode in SAT.

We introduce a Boolean variable for the boundary between each pair of adjacent squares. And we say that for the four boundaries for a given square, only exactly one of them must be true. If we run this with a standard CDCL SAT solver,

for example, KiSAT, which is as good as it gets, it won the 2020 SAT competition, we'll see this as indeed a very challenging problem. What we show here is as a function of n, how many causes get generated in the proof of unsatisfiability for that particular instance. And this is actually a very good measure

of the proof size, the time required, and also the amount of backtracking that the SAT solver had to do. And you'll see for KiSAT, even getting it up to n equals 22 was a big challenge. It required over 12 hours of runtime, and it generated a proof of over 100 million causes.

If we use a sort of naive version of our BDD-based SAT solver, you'll see we don't even do as well as KiSAT. It takes longer and we can handle even only smaller benchmarks. So these are the methods that were proposed in the two papers back in 2006.

We can do much better than this though by adopting techniques that for me were inspired by symbolic model checking. Imagine we're scanning the board from the left to the right determining what set of tilings are possible as we add each column. So you can see for a given tiling, all we really need to know is

which of the horizontal tiles from the previous column are jutting into this new column. And so as you can see, there's two configurations here that differ, but in terms of their effect on column four, they're exactly the same. And so we should be able to abstract away

the details of the early tiling and only keep track of what they imply for each successive tile. And we can do this using quantification. We just keep track of the set of vertical constraints, which I call X sub J, that define the boundaries between columns J and J plus one,

and existentially quantify away the vertical and horizontal constraints from earlier columns. So you see that this particular pair of tilings would yield the same abstracted state. And now we can compose the characteristic function that defines what set of configurations are possible

at column J minus one with a transition relation, namely the exactly one constraints for column J and generate from that, the set of possible configurations for after column J

using this equation below, which will look familiar to you if you've looked at symbolic model checking. It's important to realize that this equation is not a reformulation of the problem. It's just a way of taking the existing set of input clauses and ordering how we perform conjunction and quantification operations on them.

This works because even though the number of possible configuration grows exponentially with N, the BDD representation of that function grows only quadratically. So even for N equals 64, we have a BDD with around 1100 nodes.

As you can see with this straight line here, lot labeled column scan, we can get polynomial performance by this strategy. And it allows us to go up to N equals 124 with an overall scaling of N to the 2.7. It's really pretty good considering that the problem itself scales as N squared

since it's an N by N chessboard. So I give credit to these earlier authors for that insight that there's a very natural way of encoding the underlying logic of BDD operations using extended resolution.

Our contribution then was mainly to show that we could do arbitrary existential quantification. And this was essential for problems such as the mutilated chessboard. We showed that it worked not just on the chessboard, but the paper also describes the application of this to the pigeonhole principle problem,

which is another one for which all resolution proofs are of exponential size. And you saw that with idea of column scanning can be adapted to it, getting a proof of size order N cubed. We still have a lot of work to do. Our implementation is just a Python, really a prototype,

and we have to make a more serious implementation. We also, if this were to be used as a real SAT solver, we'd have to provide a lot more automation. In particular, some automated way of selecting a variable ordering based on just the CNF file and some way to order the conjunction

and quantification operations without guidance from the user. We're also interested in seeing other places for which BDDs have been successful at Boolean problems and seeing if we could take the same idea of generating extended resolution proofs of them.

This includes quantitative Boolean formulas, a model checking and model counting. So we look forward to a lot more work we can do in this area. Thank you.