|시간 제한||메모리 제한||제출||정답||맞은 사람||정답 비율|
|2 초||512 MB||24||8||5||62.500%|
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:
p1 ∨ p2,
¬p2 ∨ p3,
p3 ∨ ¬p4.
Each of the pi is a proposition that can be either
false. The disjunction operator ∨ can be interpreted as logical OR. The ¬ symbol is negation, which negates the value of the subsequent proposition from
false, and vice versa.
To satisfy a list of logical statements, you must assign either
false to each of the propositions such that every disjunction in the list evaluates to
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 ai and bi (1 ≤ |ai|, |bi| ≤ n), which describes the two propositions of the ith disjunction in the given list. A positive value ai, for example, represents the proposition pai. On the other hand, if ai is negative, it represents the negated proposition, namely ¬p|ai|.
The second sample input corresponds to the following list of logical statements:
p1 ∨ p2,
¬p1 ∨ ¬p3,
¬p2 ∨ p3,
p3 ∨ ¬p4,
¬p2 ∨ ¬p3.
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.
2 1 1 2
4 5 1 2 -1 -3 -2 3 3 -4 -2 -3
In the second sample case, adding a disjunction p2 ∨ p2 makes the list unsatisfiable.