Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

Given an instance of SAT, I would like to be able to estimate how difficult it will be to solve the instance.

One way is to run existing solvers, but that kind of defeats the purpose of estimating difficulty. A second way might be looking a the ratio of clauses to variables, as is done for phase transitions in random-SAT, but I am sure better methods exist.

Given an instance of SAT, are there some fast heuristics to measure the difficulty? The only condition is that these heuristics be faster than actually running existing SAT solvers on the instance.

Related question

Which SAT problems are easy? on cstheory.SE. This questions asks about tractable sets of instances. This is a similar question, but not exactly the same. I am really interested in a heuristic that given a single instance, makes some sort of semi-intelligent guess of if the instance will be a hard one to solve.

share|improve this question
Can you elaborate why the phase transition w.r.t. "density" is not what you need? –  Raphael Mar 15 '12 at 7:18
@Raphael that is a pretty good method, and I mention it in my question. But I got the impression that even better heuristics exist. The phase transition one bothers me because it is seems so easy to trick (just append easily satisfiable clauses or instance to the the one you are trying to disguise) –  Artem Kaznatcheev Mar 15 '12 at 7:26
Sorry, missed that part of your question. Right, as the commenters note, phase transition seems to be sensitive to non-random formulae. –  Raphael Mar 15 '12 at 7:33
You can represent a SAT (in CNF) formula as a bipartite graph, with vertices for every formula and clause and edges representing occurrences. If this graph is easy to partition, then the problem can be decomposed into the partitioned subgraphs. Maybe this can serve as a useful measure? I have no idea (which is why this is a comment and not an answer). –  Alex ten Brink Mar 15 '12 at 12:43
You might find this useful: ece.uwaterloo.ca/~vganesh/QPaper/paper.pdf –  user 2 days ago

1 Answer 1

up vote 18 down vote accepted

In general, this is a very relevant and interesting research question. "One way is to run existing solvers..." and what would this even tell us exactly? We could see empirically that an instance seems hard for a specific solver or a specific algorithm/heuristic, but what does it really tell about the hardness of the instance?

One way that has been pursued is the identification of various structural properties of instances that lead to efficient algorithms. These properties are indeed prefered to be "easily" identifiable. An example is the topology of the underlying constraint graph, measured using various graph width parameters. For example it is known that an instance is solvable in polynomial time if the treewidth of the underlying constraint graph is bounded by a constant.

Another approach has focused on the role of hidden structure of instances. One example is the backdoor set, meaning the set of variables such that when they are instantiated, the remaining problem simplifies to a tractable class. For example, Williams et al., 2003 [1] show that even when taking into account the cost of searching for backdoor variables, one can still obtain an overall computational advantage by focusing on a backdoor set, provided the set is sufficiently small. Furthermore, Dilkina et al., 2007 [2] note that a solver called Satz-Rand is remarkably good at finding small strong backdoors on a range of experimental domains.

More recently, Ansotegui et al., 2008 [3] propose the use of the tree-like space complexity as a measure for DPLL-based solvers. They prove that also constant-bounded space implies the existence of a polynomial time decision algorithm with space being the degree of the polynomial (Theorem 6 in the paper). Moreover, they show the space is smaller than the size of cycle-cutsets. In fact, under certain assumptions, the space is also smaller than the size of backdoors.

They also formalize what I think you are after, that is:

Find a measure $\psi$, and an algorithm that given a formula $\Gamma$ decides satisfiability in time $O(n^{\psi ( \Gamma )})$. The smaller the measure is, the better it characterizes the hardness of a formula.

[1] Williams, Ryan, Carla P. Gomes, and Bart Selman. "Backdoors to typical case complexity." International Joint Conference on Artificial Intelligence. Vol. 18, 2003.

[2] Dilkina, Bistra, Carla Gomes, and Ashish Sabharwal. "Tradeoffs in the Complexity of Backdoor Detection." Principles and Practice of Constraint Programming (CP 2007), pp. 256-270, 2007.

[3] Ansótegui, Carlos, Maria Luisa Bonet, Jordi Levy, and Felip Manya. "Measuring the Hardness of SAT Instances." In Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI’08), pp. 222-228, 2008.

share|improve this answer
I like the formalization you quote. It would also be nice to have it refined to explicitly state that $\psi(\Gamma)$ is efficiently computable. Thanks for the answer! Do you know any less formal measures people might use 'in practice'? –  Artem Kaznatcheev Apr 1 '12 at 22:45
@ArtemKaznatcheev I think the backdoor set is probably the only one really used. When running a solver, we don't really care about the hardness of the formula; the instance has to be solved nevertheless. The measurement must give us a computational advantage, or maybe we can use it to choose a suitable heuristic. Other than that, I guess hardness measures are still pretty experimental. –  Juho Apr 2 '12 at 8:57

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.