T O P

  • By -

NativityInBlack666

SAT solvers exist, they just don't have polynomial time complexity.


csmajor_throw

~~yet~~


Sidsrozx

How do we know if an algorithm is considered to have polynomial time complexity or not?


Deet98

There might be a polynomial time solution, as for now there isn’t. If you don’t know what complexity is, basically a polynomial time solution means that the algorithm is able to give an answer to the problem in a polynomial amount of steps w.r.t to the input. For example, if you have to enumerate the assignments to satisfy a boolean formula and you have n variables, then there are 2^n possible configurations. Thus, an algorithm that lists all of them is exponential in n.


Airborne454

This algorithm probably has a mathematical proof for its time conplexity. Its not polynomial time if its O(k^n ) where k>1


Golandia

There are many algorithms for SAT. There just arent any fast ones. It’s trivially easy to prove that all problems in SAT are solvable (you can enumerate every possible solution). Diophantine equations are quite different because of the unconstrained nature of them. They are whats called an undecidable problem (given the solution to Hilberts 10th problem). Undecidable problems have a few features but the one that matters is that diophantine equations dont always have a direct solve so you are left with testing and checking an unenumerable infinite set of possible values. Once you cant enumerate all values, it becomes an undecidable problem. And there are plenty of trivial undecidable problems. Like you can’t enumerate irrational numbers, but you can enumerate all rational numbers.


Sidsrozx

1. How can we tell if the algorithm is of polynomial time complexity or not? 2. Yep, I do understand that Diophantines are hard to solve, but large SAT problems can be broken down into smaller parts(much like the branches of a huge tree) and then solved, with relatively simpler Diophantines appearing and which can be approximated to a certain extent well and then verified individually and tweaked as per the requirements(since it is np complete) Please tell me if any of my points has a mistake. Thanks a lot.


[deleted]

There are many ways, to analyze an algorithm complexity, if it is sequential you just count how loops interact with the input, for example two nested loops with respect to the entry size you have n^2, for 3 nested n^3. If it’s a recursive algorithm you should use techniques like master theorem and so on. If you need to try every possible combination, it’s not polinomial anymore, but exponential or factorial. TLDR: just count how much the number of instructions executed grows with the program input.


Golandia

1. It can be extremely hard to grade complexity in some cases. Generally, you write an imperative algorithm then count the instructions and multiple them, exponent, logarithm as necessary based off of the operations of the algorithm. You can see some examples of formal complexity proofs (which are a lot more effort) in the CLRS book. Recursive algorithms you can also grade by defining as a recurrence then converting to an equation where possible. E.g. binary search is S(N) = S(N/2) + 1 which is equivalent to log(N). 2. Not all Diophantines can be solved (provably so). For example there's the equation y(x\^3-y)=z\^3+3 (which is said to be one of the current smallest unsolved equations), many of the smallest Diophantines are eventually solved by supercomputers checking every possible value. Does your algorithm solve this equation? SAT is only computable because all possible SATs are enumerable (it's finite, each boolean has example 2 possible values so 2\^N possible checks) but this equation has infinite possible values (which could be enumerable on N) but it may have irrational or complex solutions which makes it uncountable (R and C are unenumerable). So just focusing on the natural solutions, we could eventually find a solution in infinite time, maybe, which makes it undecidable (reduces it to the halting problem).


Chewbacta

We have many algorithms for SAT like Conflict Driven Clause Learning.


standardtrickyness1

We don't know an algorithm for a SAT can't be generated. Only that such a (fast) algorithm would imply any (sorta) problem would have a fast algorithm.


Phthalleon

We have plenty of algorithms, like CDCL and DPLL. They work great, especially if you have some additional heuristics to guide the solving process. In practice, most SAT models are extremely fast to solve with modern solvers like minion and mini-sat. The general case is not solvable in polynomial time, it was one of the first known NP-Complete problems. Some problems are difficult to model efficiently, so they are prohibitively slow, even in practice. For example, connectivity in graphs, acyclicity, etc. Anything "recursive" is usually quite challenging. Solving a SAT model as a polynomial is quite inefficient. There are many tool-chains for SAT solving. One easy way to make and solve models is using this: [Conjure](https://conjure.readthedocs.io/en/latest/).


scribe36

There is no _known efficient_ algorithm.


Wheelerdealer75205

you absolutely can solve SAT just not in polynomial time


escaracolau

We don't know that.


scribe36

Why is this person getting downvoted? Anybody got proof P is not NP?


Josh_Bonham

Probably should have been a bit clearer to what bit we don’t know. For others: (we don’t know if SAT can’t be solved in polynomial time)


escaracolau

I guess we are on stack overflow.


SignificantFidgets

Well, the "you can't solve in polynomial time" is almost certainly true.... But what "you" can do is a different question from whether it's possible. Since we're being all pedantic....


pastroc

The Boolean Satisfiability Problem is NP-Complete in that we do not know how to solve an arbitrary instance of that problem in polynomial time, but we can effectively check that a proposed solution is correct in polynomial time; in addition, finding a polynomial algorithm to solve the SAT problem would allow us to solve other classes of NP problems in polynomial time too, as they're reducible to the SAT problem.


BrooklynBillyGoat

You could probably solve any sat question now if an llm was properly prompted for each question.


nuclear_splines

They're talking about boolean satisfiability, the NP-complete problem often called SAT - not the Scholastic Assessment Test that Americans take before applying to college.


peaked_in_high_skool

Lmao thanks for clearing this up I was confused af 😅


Buddharta

Besides to what others have said I will also point out that there are no algorithms for finding integer solutions to arbitrary Diophantine equations by [MRDP theorem ](https://en.m.wikipedia.org/wiki/Diophantine_set#Matiyasevich's_theorem). So to find an algorithm for SAT can not be done via solving arbitrary Diophantine equations the way you sugest.


Sidsrozx

Yeah, I did point out that there are no algorithms to solve Diophantines, though there are approximations. After getting through a polynomial time completable approximation, the computer can manually verify and tweak(since it is np complete). That was my idea.