[HN Gopher] Solving SAT via Positive Supercompilation
___________________________________________________________________
Solving SAT via Positive Supercompilation
Author : Hirrolot
Score : 99 points
Date : 2024-02-01 17:01 UTC (5 hours ago)
(HTM) web link (hirrolot.github.io)
(TXT) w3m dump (hirrolot.github.io)
| inasio wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| Nope. For example, binary search is in NP (because it is in P),
| but is much easier than SAT.
| JohnKemeny wrote:
| 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.
| nyrikki wrote:
| 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.
| theGnuMe wrote:
| 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 wrote:
| 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.
| Hirrolot wrote:
| 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.
| zellyn wrote:
| 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 wrote:
| 3-SAT is NP-Complete, so either (a) is correct or else P=NP.
| zellyn wrote:
| Touche! 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!
| Hirrolot wrote:
| 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.
| zellyn wrote:
| 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 wrote:
| sad that SAT competition still hasn't moved from 00s and still
| is on http
|
| SAT conferences aren't on youtube either :(
___________________________________________________________________
(page generated 2024-02-01 23:00 UTC)