Satisfiability P93741
Write a program to find all the solutions to a set of m three–literal clauses c1, …, cm in conjunctive normal form.
For instance, {a = true, b = false, c = true, d = true} is a possible solution for the three clauses
| a or b or c, not a or b or c, b or not c or d. |
As another example, {a = true, b = false} is a possible solution for the clause
| b or not a or a. |
Stricktly speaking, this clause does not have three literals (in fact it is equal to true, which has no literals at all), but in this exercise it is allowed to have repeated literals in the same clause.
Input
Input consists of a natural number 1 ≤ n ≤ 20, followed by a natural number m > 0, followed by c1, …, cm. The names of the variables are the first n lowercase letters, and all of them appear in the input at least once. A negative literal is indicated by a minus symbol in front of the variable.
Output
Print all the possible solutions of the set of clauses. The literals of each solution must appear in alphabetical order. If there is no solution, print a hyphen.
Information about the checker
You can print the solutions to this exercise in any order.
Input
4 7 a b c -a -d c a c c -c b -b a -b -c -b -c -d -d -d -d
Output
a b c -d a b -c -d a -b c -d a -b -c -d -a -b c -d
Input
3 5 c c a a b -c -a b b -b -b -b -c -c -b
Output
-
- Author
- Salvador Roura
- Language
- English
- Translator
- Carlos Molina
- Original language
- Catalan
- Other languages
- Catalan
- Official solutions
- C++
- User solutions
- C++