# Determine complexity of a SAT problem

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 be 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?

• 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, 2012 at 6:58
• That's what I've expected. Thank you for the answer! May 19, 2012 at 7:15

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 https://cs.stackexchange.com/ or https://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.

• 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. Oct 23, 2012 at 6:12

We do not know how to bound the complexity of a SAT problem. There are several special form SATs known to be solveable efficiently, but there is no finite list of such special problems.

You can use a generic solver for a limited budget and see if it succeeds. But it failing is no gurantee the problem is hard.

When we wish to generate a hard instance of SAT we encode another problem believed to be hard as SAT. We can encode any NP problem as a SAT problem. For instance we can encode an integer factorization problem as SAT and we believe such a SAT problem is hard as solving it would solve the related factorization problem.