CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot

That's why I phrased it in terms of a bound based on some characteristic of the problem.

But I was just asking for information. I know it's a well-known problem. To be honest the fact that we're even seriously discussing this as something that may be doable is a huge step forward. AIUI, previous state of the art on real languages would have this as hopelessly pie-in-the-sky.

I think in many cases memory bound is uninteresting; one could examine a vector implementation and be satisfied that it won't explode unnecessarily. After all, we do exactly that on non-proved implementations without too much fear all the time. SAT just came to mind as a problem where that could be an interesting thing to be able to prove.

What burns me just as often is when "the problem is modeling the problem" garners a response of refusing to model anything, lest ye be wrong. This is the realm of architectural astronauts that have not yet accepted that title. I'll just put some mechanism in here where the user can make this code do whatever they want and all will be good.

This is sabotage masquerading as reason. As a somewhat senior person, refusing to decide is leaving that decision to your 'inferiors', who then bear the shame of having guessed wrong. Their track record looks worse, and yours looks better. See, you can't trust they new guys with anything. They always fuck it up. That's why you should listen to me instead.

I'm getting real tired of working with Grima Wormtongue.

What I expect from senior devs is that they have a plan, and one or more backup plans. When Plan A doesn't work, I expect them to acknowledge it and flip to Plan B. I get disappointed a lot, and I can see it in others as well. I can't tell you how many times I've surprised someone into stunned silence by practicing what I preach. Wait you're not going to fight me about how your plan didn't work? What is happening?

---

Now the long version...

There's a very precise answer here, actually, since SAT is what's called an NP-complete problem (a very important and large class of problems). The easiest way to explain what you can use with SAT is to first define NP, then define NP-completeness.

Let X be some finite "alphabet" of symbols in your system, e.g. 0 and 1 for binary inputs (but as it turns out, for our purposes it could be any finite alphabet and it doesn't really change the definition).

We define a decision problem on finite strings of symbols in X, as a predicate on strings of symbols in X, P: X* -> Prop (strings in X are just a finite number of concatenated symbols of X, e.g. "", "0", "00", "10", etc.); another way of thinking about this is just saying that P is a subset of the set of all strings of symbols in X. It can be pretty complicated to actually check whether a string is actually in P (you can define P as "the set of all programs that don't halt!"), so that is not that useful computationally.

Intuitively, since we're doing computer science, we want to characterize the properties we can actually check. Let's narrow down decision problems just a bit. First, we'll define "computable" functions f : A -> B for any types A and B, as functions / algorithms that take inputs of type A, return inputs of type B, and halt on all inputs (you can define halting formally but it's a pain so we'll skip that). These are a much better fit for computers to run than arbitrary predicates, because they have an answer and a defined algorithm.

Now, we'll narrow down the set of decision problems to the class of what are called "semidecidable problems," which is basically the largest class of functions we can say something useful about computationally. For a decision problem P : X* -> Prop, we say P has a semidecision procedure if there exists an alphabet Y and a computable function f : (X, Y) -> bool, such that for any string x : X, P x holds if and only if there exists some string y: Y such that f(x, y) returns true.

Clearly, not every predicate has a semidecision procedure: the stupid counterexample we talked about before (the set of all prgorams that don't halt) doesn't have one. But, to show how broad this class is, the halting problem actually is semidecidable! That's because if a program halts, by definition, it must halt in a finite number of steps; so you can make Y* just be a natural number represented in binary (or whatever your favorite base is), pass the max number of steps to compute to f (a function that simulates a computer for y steps), and then the function returns true if f halts within y steps and false otherwise. Pretty incredible, right? This is one of many reasons why people are usually mistaken when they say something is impossible because of the halting problem; in practical cases, you can almost always work around it with a semidecision procedure and an appropriate certificate.

One really neat aspect of semidecision procedures is that any semidecidable problem P has an algorithm that, given x: X, will always* terminate and return true if P x holds (but may run forever if it doesn't, so this is called a ). How? Because Y is finite, every string Y* can be represented as a natural number in base Y. So we can just run through every natural number, in order, convert each one into its equivalent string in Y, and then run f (the semidecision procedure for P) on (x,y). If it returns true, we're done, and we know x is in the set (and if x is in the set, we know it will eventually return true for some y, so this always terminates if x is in the set). If it doesn't return true, we're not done, but that's okay because we're only a semidecision procedure :)

There's a bunch of other interesting stuff about semidecision procedures, but we're now going to narrow it down even further... because the problem with the definition I just gave is that there's no restriction on how big y can be. It could be very large, arbitrarily larger than X. So I could just give you a ridiculous number as the upper bound on how long it takes to halt, for instance, and tell you to keep trying for that number of steps, and you couldn't realistically prove me wrong, but also obviously couldn't run that many steps. Additionally, the semiprocedure f just needs to be computable, but nobody said it needs to be fast... as long as you can prove that it halts, it can be basically arbitrarily slow! And of course, the algorithm I mentioned for finding the certificate is incredibly impractical even for relatively small certificates.

So a useful class of problems are those for which there exists an "efficient" semidecision procedure, where the total time required to run f on x and y is bounded in some way by the length of the original input, x. "Efficient" can mean a lot of things, but most people agree that stuff that's exponential in the length of x is probably not efficient, so a popular definition is that a decision procedure is "efficient" if it can run in time polynomial in the length of the input (note that this is the length of the input string, so for example if x is a number represented in binary, it needs to be polynomial in the logarithm of the number, not the number itself). Note that this obviously also places a bound on how much bigger the useful part of y can be than x: it has to be at most polynomially bigger, otherwise the algorithm definitely can't run in time polynomial in the length of x since it has to spend longer than that just reading the parts of the certificate it needs!

Using polynomial time (also called P) is nice because it erases away a bunch of stuff, like log factors (i.e. the form in which the input is represented), conversion procedures, etc. Polynomial time is also closed under most operations: if two procedures can run in polynomial time, then basically any composition you can think of that uses them also runs in polynomial time. It can also hide huge hidden terms though, so "polynomial time reducible" or "polynomial doesn't necessarily actually mean "efficient", it's just a convenient category that restricts things so they don't blow up in insane ways. In practice, most stuff people actually care about has a pretty small polynomial.

The class of problems I just defined (problems with semidecision procedures that run in time polynomial in the input?). That's NP! And that's the set of problems you can encode as SAT instances :) Why? The answer is pretty interesting... first, remember how we defined an algorithm that always terminates with "yes" if x is in the set, for any semidecision procedure at all? Well, with the restriction that our semidecision procedure runs in polynomial time and that the certificate is at most polynomially larger than X, we can ∂efine a new procedure, called a decision procedure, for the problems, as follows:

Given x, run through every y up to a polynomial greater than the maximum certificate blowup (we know this polynomial exists, and what it is, by the definition of problems in NP, as I mentioned earlier, so we know that if a certificate exists, we'll find it). For each y, run our decision procedure f(x, y) on it; this runs in polynomial time, also by definition. If f(x, y) returns true, then we return true. If it didn't return true for any y up to our upper bound, we return false. This new algorithm is said to decide P: it halts on all inputs, not just the ones that return yes, and returns true if x is in P and false otherwise. Problems with this property are called decidable, so we can see that all problems in NP are decidable.

How does this relate to SAT? Well, first, let's observe we can convert the problem from base |X| and |Y| to base 2 (and back) in polynomial time, with at most polynomial input blowup (proof omitted, it's not that interesting). Once we've done that, the algorithm we gave above looks a lot like a naive algorithm for solving SAT: if we think of every bit in the certificate as a boolean variable, then we're just running through all possible assignments to the boolean variables, and then checking f(x,y) on each assignment to see if any are true. So if we can somehow abstract f(x, _) into a boolean circuit (that uses at most polynomially more space than the original input), we're all set!

As it turns out, we can do that! The actual way we do it is kind of subtle, especially if we want to be efficient, and depends heavily on the program representation you've chosen, but the Wikipedia article on the Cook Levin theorem (https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem) gives one approach. So, any problem in NP can be converted to SAT in polynomial time :). Since SAT is also in NP (the certificate is the string of satisfying assignments, and checking it just requires running the boolean expression on the certificate), we call SAT (and other problems like it) "NP-complete." Any problem in NP that you can convert SAT into in polynomial time is also NP-complete, so this is a very natural class of problems, and it contains a whole bunch of important stuff (basically, anything where you need to search the input space for an answer, but can verify it easily).