Hacker News Reader

Comment by wiz21c | Hacker News Reader

SAT solvers are really powerful machines. You can fit many problems in a Boolean formula and then ask the solver to work it out. Now, the solver is not always optimized for your task but sometimes it helps. Also, the exercise of turning a problem into a (usually huge) Boolean formula is interesting. For example, I solved the "find a longest path in a graph" with a SAT solver (TBH, I quickly replaced that with a specialized solver, but, well, that was fun !)

View on HN

SAT is the prototypical NP-complete problem.

And indeed I think the reduction of NP problems to SAT is pretty intuitively understandable, at least at a hand-wavy level. If a decision problem is in NP, then given some candidate solution to the problem we can verify it in polynomial time. If you imagine a computer implementing this decision algorithm, and you squint your eyes, you can imagine it as a huge boolean satisfiability problem. The program takes some input (as bits aka boolean variables) and the program is run in the circuitry of the computer which at the bottom is effectively doing boolean algebra with logic gates and such. And so if you can solve SAT in polynomial time, then you can run it on this instance of SAT (the instantiation of the verifier for this NP problem) and find out if there's any input to that NP problem that satisfies it. Obviously there's a lot more work to make it formal.

While it is true, if you follow current research, most people in the field seem to be on a great hunt for hard SAT instances where no known heuristic really helps. As of yet this hunt has not been successful.

A hard SAT problem:

Let nonce be 32 boolean inputs, representing numbers from 0..2^32-1.

Let other_bits and difficulty be a collection of constant boolean inputs, in the following expression.

Let f(other_bits, nonce, diff) be the boolean logic circuit used in Bitcoin mining, for a recent candidate block.

Roughly speaking, f combines nonce with other_bits to make a bit string, performs SHA-256 on the bit string, then SHA-256 on that, and then checks if the leading diff number of bits are zero.

Folding in the constants, f reduces to a boolean logic circuit with 32 inputs and 1 output, g(nonce) = result.

The SAT problem: Does there exist a value of nonce for which g(nonce) = 1?

If you can solve this quickly, you just sped up Bitcoin mining by a factor 2^32 iterations, which is a lot. You can take this further as well.

I don't know of any SAT solver heuristic which really helps with this.

This SAT instance is huge, which makes it hard. But you haven't shown that it is a harder SAT instance than a random one of its size.

It's all about the difficulty vs the size of the instance.

To the best of my knowledge, the example has no known heuristics for finding a solution that are significantly faster than brute force.

That puts it in the hardest class of instances for its size (subject to available knowledge), because all instances can be solved by brute force.

A SAT solver might very well have optimizations that make it end up running in 2^200 on average instead of what brute force would give.

The problem is, since the instance is so large, we don't know what happens. No one has ever ran one to completion.

So no, it's not in the hardest class of instances for its size. Its difficulty is unknown.

You can encode as moderately large (low hundreds of clauses/variables) SAT instances questions of Ramsey-theory and other unsolved combinatorics and those instances will not be solved by any heuristic.

> As of yet this hunt has not been successful.

How current is your information ?

I think I've seen random instances in some of the more recent SAT competitions with only a few thousand variables that have not been solved. That said in theory there should be 100 variable instances that are too hard to solve but I haven't seen any really hard instances that small.

I was in Lissabon Last year at the SAT conference and that was my main takeway, though my field of research is only adjacent.

One paper was about creating random sat instances where the probability of unsat ist 50/50 and as it turned out: none of those instances was hard.

You can always craft hard instances to defeat a specific heuristic. But crafting one that is hard for all of them is the problem.

Reply on news.ycombinator.com