Lesson 6

Programming problem. Implement an algorithm for the Horn-SAT problem. Please do not use SAT packages. 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 begins with an integer \(1 \le k \le n\), followed by \(k\) integers from the set \(\{ -n, …, -1, 1, …, n \}\), separated by a space. It is guaranteed that each clause contains at most one positive literal.

If the formula is unsatisfiable, output the single word “UNSAT”. Otherwise, output a satisfying assignment \(a_{1}, …, a_{n}\), where \(a_{i} \in \{ -i, i \}\), with values separated by a space. If multiple satisfying assignments exist, output any assignment that contains the minimum number of positive values.

4 6
2 3 -2
2 -1 -4
2 -1 2
2 -2 3
2 -1 4
2 -3 1

-1 -2 -3 -4