<p>I think there is at least one model of computation where 2-SAT is easy and Clique is provably hard: resolution refutation complexity (i.e. how hard is to deduce contradiction from the initial clauses using resolution inference rule). If you think about decision problem instead of refutation, you may ask &quot;how hard is for a Resolution based SAT-solver to solve 2-SAT, and what about Clique?&quot;.</p>
<p>Of course in this case you have to take in account a specific encoding of Clique as a CNF formula.</p>
<p>This is a very specific model of computation, but covers algorithms that are quit common in practice (well, more common than bounded-depth circuit I would say).</p>

CC BY-SA 4.0
2022-01-19T11:17:48.860Z
2022-01-19T11:17:48.860Z
MassimoLauria
<p>2-SAT is NL-complete so separating 2-SAT from Clique would separate NP from NL, also a major open problem.</p>

CC BY-SA 4.0
2022-01-20T00:43:24.317Z
Many thanks, Lance!!
ShyPerson
CC BY-SA 4.0
2022-01-18T22:36:24.160Z
2022-01-18T22:36:24.160Z
Lance Fortnow
<p>Since the P vs. NP problem is still an open problem, 2-SAT and Clique might both be in P if P = NP. Is there any known complexity measure whatsoever that is already mathematically proven to distinguish 2-SAT from Clique?</p>

<cc.complexity-theory><clique><2sat>
Separating 2-SAT from Clique
ShyPerson
# Separating 2-SAT from Clique

(Asked by: username_0 on 2022-01-18)

Since the P vs. NP problem is still an open problem, 2-SAT and Clique might both be in P if P = NP. Is there any known complexity measure whatsoever that is already mathematically proven to distinguish 2-SAT from Clique?

**Tags:** cc.complexity-theory, clique, 2sat


---

## 2 answers

### Answer by username_2 on 2022-01-18. Score: 9 | Accepted answer

2-SAT is NL-complete so separating 2-SAT from Clique would separate NP from NL, also a major open problem.

> **Comments:**
> **username_0**: Many thanks, Lance!!  

---

### Answer by username_1 on 2022-01-19. Score: 5

I think there is at least one model of computation where 2-SAT is easy and Clique is provably hard: resolution refutation complexity (i.e. how hard is to deduce contradiction from the initial clauses using resolution inference rule). If you think about decision problem instead of refutation, you may ask "how hard is for a Resolution based SAT-solver to solve 2-SAT, and what about Clique?".

Of course in this case you have to take in account a specific encoding of Clique as a CNF formula.

This is a very specific model of computation, but covers algorithms that are quit common in practice (well, more common than bounded-depth circuit I would say).


---

