3108：Horn Clauses

Consider some set of boolean variables and a boolean formula. A set of values for the variables is called satisfying if the formula evaluates to true after replacing the variables by the corresponding values. A formula is called unsatisfiable if there exist no such set.

In general, there is no known algorithm finding the satisfying set of values in polynomial time, although it is not yet proved that such algorithm does not exist. The same holds for determining whether the given formula is unsatisfiable. Despite this there are some particular classes of boolean formulae for which the problem of satisfiability and unsatisfiability can be solved in polynomial time. Now we will define one of such classes, and your task will be to create polynomial time algorithm for it.

A Horn clause is a boolean formula, constructed according to the rules below. Let x be a variable from the set. Then a literal is a boolean expression which consists only of the variable by itself or of the variable negation: either x (positive literal) or ¬x (negative literal). A clause is a disjunction of one or more literals. A Horn clause is a clause with at most one positive literal.

Consider some Horn clause ¬n₁∨¬n₂∨…∨¬n_k ∨p. It would be more convenient to replace disjunctions with implication: (n₁∧n₂∧…∧n_k)⇒p.

For consistency, when succedent (the right part of the implication) is empty we will imagine that there is a constant false specified instead; similarly empty antecedent (the left part of the implication) is supposed to be true.

Consider a formula which is a conjunction of one or more Horn clauses. In this particular case, satisfiability and unsatisfiability problems can be solved by polynomial time algorithms. Write a program that would do it.

The file consists of formulae, written according to the following BNF. Here [‹expression›] means that expression may be omitted, {‹expression›} means that expression may occur zero or more times. Characters in quotes denote themselves.

Each formula is specified in a separate line. The total length of the input file does not exceed 20 000 characters.

Your output must contain either the set of variables with their values that satisfy the corresponding formulae, or word “unsatisfiable”. The variables may be specified in arbitrary order; the value for each variable must be specified exactly once. If there is more than one satisfying set, output any one.