Finding the number of solutions of 2 SAT

Question

I want an algorithm to know whether there exists more than one solution for 2-satisfiability problem say for 1000 literals assuming it is satisfiable. Please explain.

Answer 1

According to Wikipedia:

Feder (1994) describes an algorithm for efficiently listing all solutions to a given 2-satisfiability instance, and for solving several related problems.[14] Algorithms are also known for counting the number of solutions, more quickly than it would be possible to list all solutions,[15] and for finding pairs of solutions that differ as greatly as possible.[16]

Especially

Dahllöf, Vilhelm; Jonsson, Peter; Wahlström, Magnus (2005), "Counting models for 2SAT and 3SAT formulae", Theoretical Computer Science 332 (1–3): 265–291, doi:10.1016/j.tcs.2004.10.037 ; Fürer, Martin; Kasiviswanathan, Shiva Prasad (2007), "Algorithms for counting 2-SAT solutions and colorings with applications", Algorithmic Aspects in Information and Management, Lecture Notes in Computer Science, 4508, Springer-Verlag, pp. 47–57, doi:10.1007/978-3-540-72870-2.

seems to be what you want.

---

Here's a diploma theses on this subject. It's quite lengthy, so it should be easier to follow: http://people.inf.ethz.ch/arazen/publications/2sat.pdf

And another one including Pseudo-Code: http://www.engineeringletters.com/issues_v15/issue_2/EL_15_2_12.pdf.

But since this problem is a non-trivial mathematical problem, you have to live with math in this case.

Answer 2

I'm a bit confused by the statement of the problem and the title of your question.

If "to know whether there exists more than one solution" is really the only thing you need, listing all solutions is surely an overkill! Find the first solution, say "A AND NOT B" and add a 'blocking clause', that is a guard, that turns a SAT-solver away from that solution.

In the mentioned example, such a constraint is "NOT (A AND NOT B)". Bring it to CNF and be happy :-)