In a way that's the best we can hope for. Satisfiability in propositional logic is NP

hard. So if we believe P to be unequal to NP we have to see something exponential there.

And most people believe NP not equal to NP. And so what we're seeing, we briefly talked about

that, is these phase transitions. We see those for many NP complete problems where if you find a good

parameter, and in this case clause to variable ratio is one of those. Then you'll see empirically,

right, somebody ran a SAT solver on a huge mass of randomly generated propositional formulae here.

It's an easy, easy, if you have a SAT solver that's an easy experiment to set up and just plotted the

yes no answers from your decision procedures against, or the number of yes no answers here

against this parameter and then you kind of get this cliff picture. We've looked into a bit why

this is so, because having lots of clauses makes things unsatisfiable. Having lots of variables

gives you a lot of choice in which you can make things satisfiable. So you would kind of, after the

fact, it came as a surprise when people first did this, after the fact you kind of can see why this

has to be like this. What really came as a surprise is that at the exact point of this ratio, almost

the exact point, which is at 4.3 something here, you also see the difficult, the DPLL difficult

problems. And we tend to see that the better the SAT solver is, the more closely these two places

actually coincide. Kind of this SAT solver has a probably unnecessary problem on the high variable

cases. Okay, so you want to probably, you want to do something about your variables next. And we

typically have an extreme runtime peak at the phase transition, which is something that you're

also seeing for other NP-complete problems. If only because solvers for those just translate

into DPLL and then hit it with a big stick. Okay, so not clear how much that tells us. Okay, and

there is this phase transition conjecture that says if you have an NP-complete problem, then you

can always find an order parameter where you get this kind of a phase transition. Now we're kind

of out of AI in theoretical computer science. And we have lots of data points for this, where people

have actually found such an order parameter, but it seems almost impossible to prove this conjecture.

But who knows, one of you might.