Unsatisfying
Time limit2sMemory limit512 MB
Given 2-SAT clauses, find the minimum number of clauses of the form (p_a OR p_b) to add so the whole formula becomes unsatisfiable, or -1.
- Level
Medium7 of 10
- Topics
- Graph, DFS, Greedy, Implementation
- Solved
- No attempts yet
Problem
A computer scientist usually tries to satisfy a set of constraints. This time you do the opposite and make a list of logical statements unsatisfiable.
You are given a list of logical statements of the following form:
Each is a proposition that is either true or false. The disjunction operator is read as logical OR. The symbol is negation, which flips the value of the proposition that follows it from true to false and from false to true.
To satisfy a list of logical statements, you must assign true or false to each proposition so that every disjunction in the list evaluates to true.
Your task is to add disjunctions to the list so that the whole list becomes unsatisfiable. The disjunctions you add cannot use the negation symbol.
Every disjunction, both the given ones and the ones you add, has exactly two terms.
Input
The first line contains two integers and separated by a space (). Here is the number of propositions and is the number of disjunctions.
Each of the next lines contains two integers and separated by a space (), describing the two propositions of the -th disjunction. A positive means the proposition , and a negative means the negated proposition . Read the same way.
The second sample input corresponds to the following list of logical statements:
Output
Print on a single line one integer, the minimum number of disjunctions you must add to make the list unsatisfiable. If the list cannot be made unsatisfiable, print instead. Each disjunction you add consists of two propositions, the two propositions do not have to be distinct, and neither of them may be negated.
Hint
In the second sample, adding the disjunction makes the list unsatisfiable.