Difference between C-SAT and SAT?

Question

What exactly is the difference between these two NP-complete problems? It seems to me that they are both asking if a boolean formula can be satisfied (i.e. output 1) but one is in the context of a circuit and the other just a formula. However couldnt one write a boolean formula from a boolean circuit?

Answer 1

You are right, they are very close to each other. Any C-SAT problem could be represented as SAT, any SAT problem could be represented as C-SAT. There is a question how to translate C-SAT <-> SAT in the most efficient way. Some tasks are better to represent as SAT, some of them 'looks' better as C-SAT.

In addition, there are SAT solvers that use circuit representation internally, instead of more popular clausal form.

Further, you can read this great survey: M. Bjork, 2009, Successful SAT encoding techniques

Answer 2

Both problems are concerned with the satisfiability of boolean functions. The difference lies in the way the functions are represented - either as circuits or as formulas.

In a circuit the output of a single gate can be used multiple times. When translating a circuit to a formula, the obvious way to deal with this is to duplicate parts of the circuit, which can lead to an exponential increase in size.