algorithm2-satisfiability

Generation solutions to 2-SAT from an existing one


The polynomial time algorithm of 2-SAT involving SCC tells us whether a solution exists or not and also helps us in generating a solution to the problem . But there can be more than one solution . I wanted to know is it possible to generate other solutions efficiently using the existing one ?


Solution

  • I guess it depends on your definition of "other solutions", for example the optimization problem of 2SAT (solution with minimal number of variables as 1s), is NP-Complete.

    If you want any solution, and by "efficient" you mean polynomial time - you can flip variables in your assignment from true->false and vise versa (one simple way to do it is adding (x OR x) or for false (^x OR ^x) as a clause). Then, rerunning your 2SAT solver will give you a different solution, if such exist. You need to rerun your 2SAT solver at most n times, where n is the number of variables, and since your 2SAT solver is also polynomial time, this solution runs in polynomial time.