Counting Clauses

Time limit1sMemory limit512 MB

Summary
Given a 3-SAT instance with m clauses and n variables, print satisfactory if it has at least eight clauses and unsatisfactory otherwise.
Level

Easy1 of 10

Topics
Implementation
Solved
No attempts yet

Problem

It is time for the annual 3-SAT competition, where contestants race to solve as many 3-SAT instances as possible within the time limit. 3-SAT is a classic NP-complete problem. You are given a boolean formula in conjunctive normal form, made up of a set of clauses, each containing exactly three literals. Each literal refers to a variable either positively or negatively, and a variable can be assigned the value True or False. The question is whether there is an assignment to the variables such that every clause evaluates to True. No clause contains duplicates of a literal. It is possible, however, for a clause to contain both ¬xi and xi. An example of a 3-SAT instance is shown below (taken from sample input 1):

(¬x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3) ∧ (x1 ∨ ¬x2 ∨ x3) ∧ (x1 ∨ ¬x2 ∨ ¬x3) ∧ (x1 ∨ x2 ∨ ¬x3)

Øyvind is a judge in the competition, responsible for verifying the quality of problem instances crafted by the other judges before the contest starts. Øyvind hates 3-SAT instances with fewer than eight clauses, because they are always satisfiable and give the contestants no real challenge. He therefore deems such problem instances unsatisfactory. Whenever Øyvind encounters an instance with eight or more clauses, he knows that figuring out whether it is satisfiable is a real challenge, so he judges these problem instances satisfactory. Given an instance of 3-SAT, can you help find Øyvind's judgement?

Input

The input is a single instance of the 3-SAT problem. The first line contains two space-separated integers: m (1 ≤ m ≤ 20), the number of clauses, and n (3 ≤ n ≤ 20), the number of variables. Then m clauses follow, one clause per line. Each clause consists of 3 distinct space-separated integers in the range [−n, n] \ {0}. In each clause, the three values correspond to the three literals in the clause. If the literal is negative, the clause is satisfied when the corresponding variable is set to False. If it is positive, the clause is satisfied when the variable is set to True.

Output

Print “satisfactory” on a single line if Øyvind finds the 3-SAT instance satisfactory, and “unsatisfactory” otherwise.

Examples2

  1. Example 1

    Input
    5 3
-1 2 3
-1 -2 3
1 -2 3
1 -2 -3
1 2 -3
    Expected output
    unsatisfactory

  2. Example 2

    Input
    8 3
1 2 3
1 2 -3
1 -2 3
1 -2 -3
-1 2 3
-1 2 -3
-1 -2 3
-1 -2 -3
    Expected output
    satisfactory