Satisfiability P93741


Statement
 

pdf   zip

html

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.

Public test cases

  • 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

    -
    • Information
    Author
    Salvador Roura
    Language
    English
    Translator
    Carlos Molina
    Original language
    Catalan
    Other languages
    Catalan
    Official solutions
    C++
    User solutions
    C++