15116번 - Unsatisfying 다국어

Usually a computer scientist tries to satisfy some constraints. This time you will try to make some logical statements unsatisfiable.

You will be given a list of logical statements of the following form:

p₁ ∨ p₂,
¬p₂ ∨ p₃,
p₃ ∨ ¬p₄.

Each of the p_i is a proposition that can be either true or false. The disjunction operator ∨ can be interpreted as logical OR. The ¬ symbol is negation, which negates the value of the subsequent proposition from true to false, and vice versa.

To satisfy a list of logical statements, you must assign either true or false to each of the propositions such that every disjunction in the list evaluates to true.

Your task is to add disjunctions to the list to make the list of statements unsatisfiable. But the additional disjunctions you add cannot use the negation symbol!

All disjunctions (both those given and ones you add) must have exactly 2 terms.

The first line of input contains two space-separated integers n and m (1 ≤ n, m ≤ 2,000), with n representing the number of propositions and m representing the number of disjunctions.

Each of the next m lines contains two space-separated integers a_i and b_i (1 ≤ |a_i|, |b_i| ≤ n), which describes the two propositions of the ith disjunction in the given list. A positive value a_i, for example, represents the proposition p_ai. On the other hand, if a_i is negative, it represents the negated proposition, namely ¬p_|ai|.

The second sample input corresponds to the following list of logical statements:

p₁ ∨ p₂,
¬p₁ ∨ ¬p₃,
¬p₂ ∨ p₃,
p₃ ∨ ¬p₄,
¬p₂ ∨ ¬p₃.

Output, on a single line, a single integer representing the minimum number of additional disjunctions necessary to make the list unsatisfiable. If it is not possible to make the list unsatisfiable, print -1 instead. Each disjunction you add must have two (not necessarily distinct) propositions, and you may not use negated propositions.

In the second sample case, adding a disjunction p₂ ∨ p₂ makes the list unsatisfiable.