[Solved]: How to do last step of Krom's algorithm for solving 2SAT problems

Problem Detail: 

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?

Asked By : RabidOrange

Answered By : Yuval Filmus

The first step in implementing an algorithm is understanding why it works.

In your case, Krom's algorithm is based on repeated application of the resolution rule $$ \begin{array}{c} a \lor b \qquad \bar{a} \lor c \\\hline b \lor c \end{array} $$ Here $a,b,c$ are literals. This rule is valid, and applied to two 2-clauses produces a 2-clause. Hence there is no harm in running it until reaching a point at which it can be applied no more. If in this way we reach a clause $a \lor a$, then the literal $a$ must be true. So if we reach both $a \lor a$ and $\bar{a} \lor \bar{a}$, there is no solution.

More interestingly, if all solutions have $a$ set to true, then the completeness of resolution implies that $a \lor a$ will be generated.

This suggests the following algorithm:

1. Generate all 2-clauses reachable by resolution.
2. If you have generated both $a \lor a$ and $\bar{a} \lor \bar{a}$ for some variable $a$, then there is no solution.
3. Otherwise, if for some variable $a$ we have generated neither $a \lor a$ nor $\bar{a} \lor \bar{a}$, add one of them as you please and go back to step 1.
4. Output the truth assignment satisfying all literals $a$ for which we have generated $a \lor a$.

This is just one implementation; others are possible. (For example, we could immediately substitute any known values before step 3.)

Back to your example: $a \lor b$. Step 1 produces no new clauses. The variable $a$ is "free", so in step 3 we add (say) $\bar{a} \lor \bar{a}$. Step 1 is now more interesting: $$ \begin{array}{c} a \lor b \qquad \bar{a} \lor \bar{a} \\\hline b \lor \bar{a} \end{array} \\ \begin{array}{c} a \lor b \qquad b \lor \bar{a} \\\hline b \lor b \end{array} $$ We can now read off the truth assignment $a=F,b=T$.

Had we added $a \lor a$ instead, step 1 would still not do anything, and so we would add either $b \lor b$ or $\bar{b} \lor \bar{b}$ in step 3, and then read off one of the truth assignment $a=T,b=T$, $a=T,b=F$.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/51302

3.2K people like this

 Download Related Notes/Documents