0

I know that applying Strongly connected components in a Digraph we can check 2-SAT boolean satisfiability if the problem is solvable in polynomial time.

Let's assume the problem is satisfiable.

The question: is there a general algorithm to calculate that solution relying on 2-SAT?

Ivan Voroshilin
  • 5,233
  • 3
  • 32
  • 61

1 Answers1

1

Assuming I understand your question correctly, yes, there is a general algorithm to find a solution (i.e. a satisfying assignment) by using the algorithm for the satisfiability problem.

Suppose I assign a variable xi the value "true" (so that the literal xi is true and ~xi is false) to make a new 2-CNF from the original. If I were to run satisfiability on it (i.e. use the thing with SCCs to find if the new CNF is satisfiable):

  1. What does it tell you about the satisfying assignments in the original CNF if the resulting CNF is now not satisfiable?
  2. What does it tell you about the satisfying assignments in the original CNF if the resulting CNF is still satisfiable?

The idea behind the algorithm is to make the variable "false" if you hit case 1, and "true" if you hit case 2, and loop through every variable (keeping the assignments that you made to variables you've already looked at). Once you can answer the questions I've posed, you'll understand the concept behind it.

Dennis Meng
  • 5,109
  • 14
  • 33
  • 36
  • Thanks Dennis for the answer. Basically, I've been trying to map this problem from Google Jam to 2-SAT but have some difficulties: http://code.google.com/codejam/contest/32016/dashboard#s=p1&a=1 There are some constraints as well and this is my first experience in problems like this one. – Ivan Voroshilin Nov 03 '13 at 17:11
  • 1
    Yeah, the problem you linked isn't 2-SAT; you'd have to have each person liking at most two flavors for it to be 2-SAT. My tip on that problem is that because of the constraints on how big N is, there can't be more than 1024 combinations of making everything malted or unmalted. There aren't that many customers, you could probably just loop through all of the combinations and find one that works. – Dennis Meng Nov 03 '13 at 17:25
  • Absolutely! These constraints got me confused. – Ivan Voroshilin Nov 03 '13 at 17:44