4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ A quick comment not really relating to your question: one can also solve 2-SAT instances using an off the shelf SAT solver. $\endgroup$ – Juho Dec 30 '15 at 19:49
  • 1
    $\begingroup$ I know, but im interested specifically in implementing Krom's algorithm $\endgroup$ – RabidOrange Dec 30 '15 at 19:50
4
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ Oh, so you add a special clause and then you try to apply again the inference rule? And so on? $\endgroup$ – RabidOrange Dec 30 '15 at 20:20
  • $\begingroup$ Yes, that's the idea. There could also be other options, but that definitely works. To know for sure what Krom intended, you'd have to read his paper. $\endgroup$ – Yuval Filmus Dec 30 '15 at 20:21
  • 1
    $\begingroup$ (The first step in implementing an algorithm is understanding why it works. When pen&paper didn't convince me I understood how an algorithm presented including pseudo code works and why, I remember coding it just to be able to watch it go through its steps. Can't readily remember a use case from decades ago, just now it's LCP merge (Ng&Kakehi).) $\endgroup$ – greybeard Dec 31 '15 at 4:17
  • $\begingroup$ @YuvalFilmus Just one more thing. When you use my example (a or b) to illustrate the algorithm, you add the clause ¬a or ¬a and then apply resolution to produce the clause b or ¬a; but right after that, you apply resolution between (a or b) and (b or ¬a), which produces the clause b or b. Why do you do that? I understand that I must apply resolution after adding one "special clause", but why do I have to apply resolution between the produced clause and the "original clause"? (If that's what means that second resolution) Thanks in advance. $\endgroup$ – RabidOrange Jan 5 '16 at 1:51
  • $\begingroup$ @RabidOrange You can apply resolution in any order you wish, but you have to do it in all possible ways until you deduce all possible clauses. $\endgroup$ – Yuval Filmus Jan 5 '16 at 7:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.