Solving SAT via Positive Supercompilation

https://hirrolot.github.io/posts/sat-supercompilation.html

by Hirrolot • 2 years ago

153 38 2 years ago

hirrolot.github.io

inasio• 2 years ago

There are many very simple heuristics for solving 3-SAT, some even with analytical convergence estimates. A simple random walk (Algorithm P in Knuth's Satisfiability fascicle), which iterates through the clauses and flips a variable at random if it encounters a violated clause, will do the trick too

arcastroe• 2 years ago

Ah, should've double checked before posting. Thank you everyone who corrected me. Leaving it up for others.

SAT is an NP-complete problem, meaning that it is at least as hard as any other problem in NP

I think this statement is backwards. Instead, any other problem in NP is at least as hard as SAT

amluto• 2 years ago

NP-complete means that a problem is both NP-hard (it's as hard as anything else in NP) and is in NP (with all that membership in NP implies: there is a polynomial time witness and verifier for a "yes" answer, it's at most polynomially harder than any NP hard problem, etc.).

tsimionescu• 2 years ago

Nope. For example, binary search is in NP (because it is in P), but is much easier than SAT.

JohnKemeny• 2 years ago

To be slightly nitpicky, it is problems that belong to complexity classes and not algorithms. Binary search is an algorithm that solves searching in a sorted list.

Funnily, although we usually think of it as having complexity O(log n), that does not hold true for the Turing machine model, with which the complexity classes P and NP are defined.

refulgentis2• 2 years ago

Wait:

` binary search is in NP (because it is in P),`

P = NP!? Casually proved in a HN comment?

nyrikki• 2 years ago

Thinking of this way helps me.

NP-complete is the intersection of sets NP and NP-hard , but not the part of NP that contains P.

Lots of NP-hard problems are not in NP is important.

gbacon3• 2 years ago

See this helpful diagram:

https://en.wikipedia.org/wiki/NP-hardness#/media/File:P_np_n...

theGnuMe• 2 years ago

Is this just compiler optimized memoization? I mean this is great for parallelization as well but I thought this was standard in the functional programming paradigm. Maybe I am wrong.

whitten• 2 years ago

As I recall, memorization usually involves associating the results of calling a pure function with the particular input values so the computation of the function is reduced to a lookup operation.

The calculation of the pure function is still used for any other combination of input values.

Supercompilation looks at the unevaluated symbolic recursive code and replaces the code in some cases with simpler, specialized code tuned to the actual input values, so does a memoizing not only of the result, but the code used to calculate the function to begin with.

Hirrolot4• 2 years ago

There are currently no production-grade compilers that make use of supercompilation in the functional world. Memoization is about caching results of pure functions; supercompilation is about deep program transformation.

tgv• 2 years ago

Any idea why there aren't? Not even to a small degree? To me, it looks like fairly straight-forward rewriting. Perhaps it's hard to tell how much is useful?

deep program transformation

It doesn't have to be deep, does it? You can't transform the entire program, so there's an arbitrary cut-off anyway.

rurban• 2 years ago

I thought the SPARC part of Ada did that

zellyn3• 2 years ago

I'm almost completely clueless with both 3-SAT and supercompilation, but I'm willing to bet that if you found a neat trick that solves 3-SAT problems easily, then either or both (a) there are classes and/or sizes of 3-SAT problems for which your solution breaks down badly (goes exponential), or (b) what you're doing reduces to a 3-SAT strategy that the people who enter 3-SAT contests[1] already knew about a long time ago.

[1] http://www.satcompetition.org/

CobrastanJorji• 2 years ago

3-SAT is NP-Complete, so either (a) is correct or else P=NP.

zellyn3• 2 years ago

Touché! I guess I was thinking that there are often sub-classes of NP-complete problems that are amenable to much more efficient algorithms, and it might be easy to accidentally not try any hard ones. Turns out the author fully acknowledged exponential explosion, which I would have known had I read Final Words section instead of skimming everything after the intro!

Hirrolot4• 2 years ago

The solution has exponential time and space complexity, which I noted in the blog post. It is only interesting for its simplicity and as a stress test for supercompilers.

zellyn3• 2 years ago

Ah, I missed that. Makes perfect sense! By the way, if you're interested in the "this problem can blow up badly because it can be converted to 3-SAT", you might like https://research.swtch.com/version-sat

NooneAtAll3• 2 years ago

sad that SAT competition still hasn't moved from 00s and still is on http

SAT conferences aren't on youtube either :(

pixelpoet• 2 years ago

I love that the favicon for the 2023 results is a Doge, lol: https://satcompetition.github.io/2023/results.html

Hirrolot4• 2 years ago

Haha, awesome!

kazinator• 2 years ago

Conversion of an NFA graph to DFA (in regex processing) seems to be a kind of supercompilation. The NFA is treated as a process, and is simulated for all possible input symbols at every step. The supercompiler makes note of what states it goes into and turns sets of them into DFA states.

gbacon3• 2 years ago

Without backreferences, it has a worst-case exponential blow up due to the DFA possibly needing to simulate that many simultaneous NFA states.

Regex matching with backreferences is NP-hard.

- https://perl.plover.com/NPC/NPC-3SAT.html

- https://perl.plover.com/NPC/NPC-3COL.html

Solving SAT via Positive Supercompilation

Related Stories