# Can you solve 2-sat problem when truth assignments of some variables are determined

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?

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