5
$\begingroup$

I am trying to find a assignment to satisfy a 2-sat statement. Problem is some of the clauses are 0 or x or 1 or x. I think the 1 or x clauses have no effect on the solution, but the 0 or x clauses determine the value for x. As I have clauses like ~x or y the determined value for x results in determining the value for y and so on. Can I solve this problem with Krom's procedure?

$\endgroup$
9
$\begingroup$

First set all literals $x$ to $1$ if they appear in a clause $0 \vee x$, and set $\bar x$ to $0$. If that requires you to set some $x$ to both $0$ and $1$, it's unsatisfiable. Iterate this until you don't have to set any more literals to $0$. If you get this far without finding out that the formula is unsatisfiable, remove all clauses that contain a $1$. Now you either have no clauses left - then it's satisfiable - or some 2-CNF formula to which you can apply Krom's algorithm.

Alternatively, remove all clauses $1 \vee x$ and replace all clauses $0 \vee x$ by $(y \vee x) \wedge (\bar y \vee x)$ for a newly introduced variable $y$. You can directly apply Krom's algorithm to the formula you get this way.

$\endgroup$
7
$\begingroup$

Also a similar solution is to define Zero and One variables and add two extra clauses $ \bar{zero} \vee \bar{zero} $ for value 0 and $ one \vee one $ for value 1. After that we can follow the Krom's algorithm.

$\endgroup$

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.