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?
$\begingroup$
$\endgroup$
0
Add a comment
|
$\begingroup$
$\endgroup$
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 (or more likely, a linear-time algorithm like that of Aspvall, Plass, Tarjan) to the formula you get this way.
$\begingroup$
$\endgroup$
0
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.
