Take the 2-minute tour ×

Is there a standard way to determine a complexity of the specified SAT problem? I'm researching algebraic cryptanalysis and came to solving multivariate quadratic equation systems using CryptoMiniSat. However it would nice to evaluate a complexity of the full cipher equation system. Does it only depend on the number of polynomials and variables? And is there a way to estimate the time needed for solving the equation system and what parameters do I need to know to find that out?

share|improve this question
AFAIK the short answer is no in general. Hard crypto problems are notable to generate hard SAT instances, even though random problems with similar metrics (number of clauses, equations..) would be easy. –  fgrieu May 14 '12 at 6:58
That's what I've expected. Thank you for the answer! –  Zoresvit May 19 '12 at 7:15

1 Answer 1

up vote 1 down vote accepted

No, there is not.

Your question is not well-posed. You have not specified whether you want worst-case complexity or average-case complexity, and over what class of SAT instances. The answer will depend heavily upon those details.

If you want to know what is the world record for an algorithm for 3SAT, measured by its worst-case complexity over all possible 3SAT instances, that's a question to ask on http://cs.stackexchange.com/ or http://cstheory.stackexchange.com/ . See, e.g., Best Upper Bounds on SAT and Measuring the difficulty of SAT instances. But don't expect these theoretical results to necessarily have any relationship to the performance of SAT solvers in practice.

share|improve this answer
Thank you very much for the explanation, now I have better understanding of how it works. This will already be a good help for my research. –  Zoresvit Oct 23 '12 at 6:12

Your Answer


