Lesson 3

Programming problem. Implement the algorithm for the 2-satisfiability problem. Please do not use SAT packages, but feel free to use the \(\texttt{networkx}\) library for finding strongly connected components and their topological ordering.

The first line contains the number of variables, \(1 \leq n \leq 100\), and the number of clauses, \(0 \leq m \leq 1000\). Each of the following \(m\) lines contains two integers from the set \(\{ -n, \dotsc, -1, 1, \dotsc, n \}\), separated by a space. If the formula is unsatisfiable, output the single word “UNSAT”. Otherwise, output a satisfying assignment \(a_{1}, \dotsc, a_{n}\), where \(a_{i} \in \{ -i, i \}\) on one line, with values separated by a space.

4 8
3 -2
-1 -4
1 2
-1 2
-2 3
-1 4
-3 1
2 4

UNSAT