I was making a program for solving 2 SAT problems, using Krom's algorithm. I did not found a lot of information searching in Google, so I used Wikipedia's description of Krom's algorithm to implement it but I'm stuck in the last step.
If I understand it well, the algorithm could be resumed in this:
1) You have to reduce your original 2 CNF boolean formula using Krom's inference rule as much as you can:
(a or b) and (¬a or c) => (b or c)
2) While preserving consistency, for each variable in the original formula, you must add only one of these special clauses: (x or x) and (¬x or ¬x).
(For Krom, a formula is consistent if there aren't both of these special clauses at the same time in the formula)
3) You assign to each variable TRUE or FALSE depending on which of these special clauses has been added to the formula. If the variable x has the special clause (x or x) then we assign TRUE to x; and if the variable y has the special clause (¬y or ¬y) then we assign FALSE to y.
4) This is the step where I am stuck.
My problem is that I don't know what to do once I have made the assignments to the variables. And the last paragraph of the Wikipedia describing the algorithm doesn't explain it clearly. Do I have to check satisfiability on this formula or also in the original formula as well?
Furthermore, for example:
I have this formula:
(a or b)
Then I add for each variable its special clause (as the algorithm doesn't specify which of them you should pick) like this
(a or b) and (¬a or ¬a) and (¬b or ¬b)
So I assign to the variables a and b the value FALSE, but then the first clause (the clause on the original formula) becomes false. What do I do in that case? Could somebody explain me the last step of Krom's Algorithm for solving 2SAT problems?