David R. MacIver's Blog

A new method for SAT model counting (that doesn't work)

There’s an idea that has been bouncing around in my head for about a year that I keep revisiting and trying and failing to make work every couple of months. I’ve finally understood the in retrospect very obvious reason why it hasn’t been working, and indeed why any approach like it cannot possibly work, so it’s time to write it up to get it out of my head, and in the hope that some of the pieces will be interesting or useful to others.

Prelude

SAT model counting is this: You have a SAT problem (that is, some boolean formula over \(n\) variables, typically expressed in conjunctive normal form), and you want to know how many distinct variable assignments satisfy the formula. This is much harder than SAT, where you only want to know whether there is at least one.

To see an easy example of why it’s much harder: Imagine taking any SAT problem \(f\) you like, and adding one variable to the formula, \(v\), and defining a new formula \(f'(x, v) = v \vee f(x)\). i.e. the new problem is satisfied if the old problem is, or if \(v\) is.

The satisfiability version of this is now trivial: Yes, this is satisfiable, just set \(v\) to true. The counting problem version of this however is exactly as hard as the counting problem for your original \(f\) was.

This is particularly bad because it applies recursively: It’s a key feature of all SAT solvers that when they detect a “pure literal” (that is, a variable like \(v\) above that if you set it to true or false can only ever make the problem easier), they set it in the most convenient way. In model counting, you have to try it both ways, so there are many cases where we know how to solve a SAT problem efficiently but don’t know how to count it in less than exponential time because you have to branch on each variable.

The idea that I’ve been entertaining for about a year, building on ideas I was working on back then, is that you can construct an unbiased Monte Carlo estimator for the model counting problem even when you can’t count it exactly. That is, you can define some random process where if you run it a bunch of times, on average it converges to the true answer.

The fact that you can do this is easy. Here, I’ll construct one for you right now: Randomly assign all \(n\) variables. If the result satisfies the formula, return \(2^n\). Otherwise return \(0\).

This works because if there are \(k\) solutions then the probability \(p\) of a random assignment satisfying the formula is exactly \(\frac{k}{2^n}\), so what we do here is we simulate a Bernoulli random variable with parameter \(p\) by doing that random assignment, then take the expected value of that variable and scale it appropriately.

There’s just one problem with this estimator. It is, to use a technical term, shit.

More specifically: It is extremely high variance. The problem with this estimator is that (for most interesting choices of SAT problem) most of the time it returns \(0\), and a tiny fraction of the time (which probably rounds to “never”) it returns a huge overestimate.

Anyway, the idea I’ve been entertaining is this: If you take some subset of variables \(U\), and you can get a Monte Carlo estimator \(Q\) of the probability \(q\) that a random assignment of \(U\) can be extended to a satisfying solution of \(f\) together with a random variable \(X\) that uniformly samples such an assignment, you can recursively build a Monte Carlo estimator for \(p\) as \(p = q E(P(SAT|X))\), so you can use \(Q g(X)\) as your estimator, where \(g\) is some recursive estimator that takes a partial assignment and estimates the probability that a random assignment of the remainder is satisfiable.¹

Anyway, the point of this post is:

1. You can, for quite large \(U\), get such a pair of estimators, in many cases very efficiently.
2. The resulting estimator is still shit.

Why this doesn’t work

Let me construct for you an example that shows that this fails exactly as badly as the coin flip model.

First, take some SAT problem \(f\) over \(m\) variables that has exactly one solution.

Now, augment it with \(k\) variables, \(u_1, \ldots, u_k\), and consider the SAT problem \(f'(u, v) = f(v) \vee (u_1 \wedge \ldots u_k)\).

The correct number of solutions to this is \(2^{k} - 1 + 2^m\) - all but one of the possible assignments of \(u\) have exactly one extension, but if all of the \(u_i\) are set to true, the remaining \(m\) variables can be assigned freely, so you have \(2^m\) solutions associated with that particular assignment of \(u\) only.

Now, pick \(m\) to be very large, and \(k\) to be… largeish. Say 32, so that \(2^k\) is about a billion. Take the uniform sampler over satisfiable assignments to \(U\) that you get from just randomly assigning all the variables (every possible assignment is satisfiable), and as your recursive step return \(2^{-m}\) if you didn’t set all of the \(u_i\) true or \(1\) if you did.

We’ve now got the same problem as before: The vast majority of the time, our estimator estimates the number of solutions as \(2^k\), but one time in a billion it estimates it as \(2^{k + m}\). The former is a huge under-estimate, but it’s dominated by the huge overestimate we make extremely rarely.

There are, possibly, some ways to rescue this, but only if you can detect that it’s happening. In this case it’s very obvious that it is, but in more natural examples where the discrepancy is better hidden, I don’t know how to do it.

The method

Let me now tell you about the very neat method I have to get these estimators that I’ve just demonstrated to you aren’t actually useful.

The idea is to use the table methods I’ve outlined before. You start with a set \(U\) that is small enough that you can enumerate all \(2^{|U|}\) possible assignments (you can, under many circumstances, enlarge it quite a lot later). You build a table of all of those assignments.

Now, you uniformly sample a row from that table, and feed it to an incremental SAT solver. This gives you a core - a subset of that assignment that cannot be satisfied. You now delete all rows matching that core. This usually fairly rapidly converges on a table that, with high probability contains satisfying assignments, and iterating this until you get a satisfying result will correctly uniformly sample from the set of satisfiable assignments of your variables.²

Suppose you’ve got to the point where this table now samples satisfying assignments with high probability. We still need to estimate the probability that a random assignment of \(U\) is satisfiable. How do we do that?

Well, if we’ve got \(k\) rows in our table, then the probability that a random assignment of \(U\) is satisfiable is \(\frac{k}{2^{|U|}}\) times the probability that a random row in the table is satisfiable. We can use Adaptive Weighted Rejection Sampling for that.

Or, more simply, if we’ve got the probability of success down, we can skip the adaptive part. Sample uniformly from the table until you’ve got two satisfiable solutions, and let \(r\) be the number of unsatisfiable ones you saw along the way. Return \(\frac{1}{r + 1}\). This is a standard Negative Binomial Estimator for a probability (which has the nice feature that it’s always non-zero).

Putting these two together, you get the building blocks you need for the estimator.

There’s a lot more detail that I’ve figured out at various points about how to build tables with lots of variables, and how to combine several of these, and so on and so forth. It’s possible that some of it is useful and generalises, but all of my notes and experiments are in a bit of a state of a mess, and I don’t currently have much faith in them.

Where to from here?

Probably nowhere. I expect I’ll continue tilting at this windmill on and off, and I have some ideas for how to rescue this, but I think the existence of these rare events that lead to unusually large subproblems is something of a death sentence for this entire approach. If you can identify them and compensate for them, maybe it’s not a problem. This approach certainly seems to work pretty adequately for, say, random 3-SAT, but it does run into this problem with real problems on the model-counting competition instances (indeed I reverse engineered the problem I describe here from thinking about those).

It does, of course, work for model counting pretty well when you can make the table cover the whole set of variables. There might be some SAT problems where this is actually a viable and useful method, but I think they’re probably almost exclusively SAT problems where other methods work just fine.

Mostly I just felt like there’s a neat observation here and it was sortof silly sitting on it given that I do not realistically expect to ever make progress on this problem in general, or this approach in particular, so I thought I’d put it out there in the hopes that at least two other people in the world might find this interesting.