[Solved]: Can you solve 2-sat problem when truth assignments of some variables are determined

Problem Detail: 

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?

Asked By : sudomakeinstall2

Answered By : G. Bach

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.

Best Answer from StackOverflow

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