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
