3
$\begingroup$

If i have a propositional logic formula, every time i add a variable the number of interpretation grow up by 2.

So if i have a propositional formula with 3 variables i have 8 interpretations.

So, is the time complexity of the SAT problem of propositional logic a $O(2^{x})$ ?

Improve this question
$\endgroup$
12
  • $\begingroup$ You are mixing time complexity of problems and runtime of algorithms here. It is true, that if you have an algorithm for SAT checking every single interpretation until you find one satisfying the formula, your algorithm runs in $\mathcal{O}(2^n)$ time. However, since it is a possible that $\mathsf{P} = \mathsf{NP}$, SAT might be solvable in polynomial time. $\endgroup$ – ttnick Mar 1 '18 at 10:00
  • $\begingroup$ The method i exposed is it not a possible way to solve a SAT propositional problem ? If it's a possible way, to me it seems the most onerous method, because it's practically a brute-force. Is it correct ? $\endgroup$ – Qwerto Mar 1 '18 at 10:03
  • 2
    $\begingroup$ Yes, by doing the most naive thing, try every single interpretation, you end up in $\mathcal{O}(2^n)$. But to come back to the initial question: This is not the "time complexity of SAT"! $\endgroup$ – ttnick Mar 1 '18 at 10:22
  • 1
    $\begingroup$ If you men efficient algorithms those which run in polynomial time, then no. But there are algorithm which are pretty good in practice (e.g. DPLL) but not in worst case polynomial time. $\endgroup$ – ttnick Mar 1 '18 at 10:58
  • 1
    $\begingroup$ Number of interpretations for 2SAT also grows exponentially. Though, linear time algorithms exist. $\endgroup$ – rus9384 Mar 1 '18 at 18:13
5
$\begingroup$

Your question hints at multiple misconceptions which I'm going to address.

If i have a propositional logic formula, every time i add a variable the number of interpretation grow up by 2.

First, let's be clear about terminology.

  • variable vs literal -- the formula $a \lor b \land a$ has three literals but two variables.
  • model vs interpretation -- every logical formula has exactly one of two possible interpretations, true and false.

It would be correct to say: the number of models grows exponentially (with base 2) in the number of variables.

So, is the time complexity of the SAT problem of propositional logic a $O(2^x)$?

No, that does not follow.

  • What is $x$? In complexity theory, we usually express complexity in the input length. So if $x$ is the number of literals, that thought makes sense; if it's the number of variables, it does not. However, in the worst cases (if we consider search space alone), the number of variables and literals is the same.
  • The number of possible models (e.g. valuations of the variables) alone is not trivially an upper bound on the complexity. The brute-force algorithm also has to evaluate the formula for every candidate, so you have to add a linear factor at least (depends on the computational model and cost model you use).

  • When somebody says, "the complexity is X" that implies a lower bound in addition to an upper bound. Your observation does not provide a lower bound, even after correction.

    That is because the size of the search space does not correlate with solving complexity. Take sorting, for instance: finding the correct permutation has a search space of size $n!$ and yet we can solve the problem in linearithmic time. SSSPP is another common example.

Improve this answer
$\endgroup$
4
$\begingroup$

The complexity of determining the satisfiability of a given propositional formula is unknown. It is conjecture not to be polynomial – this is the celebrated $\mathsf{P} \neq \mathsf{NP}$ conjecture. A more refined conjecture is the exponential time hypothesis and its variants, which have recently seen applications in (conditionally) analyzing the complexity of problems in $\mathsf{P}$, a pursuit known as fine-grained complexity.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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