Live data from Hacker News

I solved SAT (boolean satisfiability), what now?

news.ycombinator.com

1–5 of 5 posts

I solved SAT (boolean satisfiability), what now?

#1
Hi all, I discovered a solution to the SAT problem (boolean satisfiability) that runs in time complexity O(n*log(m)), and space O(2^n), where m is the number of inputs and n is the number of boolean operations. I have spent a few months solving various SAT problems with a program I wrote. I'm a senior in high school. What should I do? Advice would be appreciated. Thank you in advance.

Re: I solved SAT (boolean satisfiability), what now?

#3
How can your program use O(2^n) space in less than O(2^n) time? Do you just allocate a huge chunk of memory but don't use most of it? If so, you can replace it by a hash table using O(n² * log(m)) space at an amortized constant cost per memory operation.

Once you have reduced memory consumption in this manner, you can try solving some previously-out-of-reach large SAT instances from past competitions https://satcompetition.github.io/

I expect you to fail, but I think attempting this and figuring out where you made a mistake will likely be educational.

Re: I solved SAT (boolean satisfiability), what now?

#5
post #3

How can your program use O(2^n) space in less than O(2^n) time? Do you just allocate a huge chunk of memory but don't use most of it? If so, you can replace it by a hash table using O(n² * log(m)) space at an amortized constant cost per memory operation. Once you have reduced memory consumption in this manner, you can try solving some previously-out-of-reach large SAT instances from past competitions https://satcompe…

@OP: Just as a reminder, to compute the time you must assume a single processor. You can't run 2^n operations in parallel.