World's most popular travel blog for travel bloggers.

# Complexity of calculating a single model versus all models of a propositional formula with a SAT solver

, ,
Problem Detail:

I have little background with SAT sovers and theoretical computer science.

How can I describe the complexity of calculating all models of a propositional formula versus just the usual SAT problem of finding just one model?

I am writing a paper, in an area where finding a single of a model of a type of propositional formula is considered "easy", but for my reasearch I need to calculated all models. (I am using Picosat that can calculate all models of a logic formula.) Is there a way to describe how "hard" or "complex" finding all models is compared to finding a single model?

The worst-case complexity of finding all models of a SAT formula over $n$ variables is roughly $\Theta(2^n)$. (For instance, consider a formula where all assignments satisfy the assignment; then there are $2^n$ satisfying assignments, so just listing all satisfying assignments takes $\Omega(2^n)$ time.)

Nonetheless, this number probably isn't very useful in practice. In practice, the running time to find all models depends heavily on the formula and on the number of models. Standard methods for worst-case complexity don't offer a good way to summarize the time to do this, as the running time practice varies heavily.

So, for your paper, I wouldn't place much stock on this complexity figure. I just don't think it is very illuminating.