Boolean Satisfiability Problem

A satisfiability problem in conjunctive normal form consists of a the conjunction of a number of clauses, where is clause is a disjunction of a number of variables or their negations. If we let xi represent variables that can assume only the values $true$ or $false$, then a sample formula in conjunctive normal form would be $$(v_1\lor v_2\lor v_3)\land (\neg v_2 \lor v_4 \lor v_3)\land (\neg v_2\lor \neg v_4\lor v_3)\land (v_1\lor \neg v_3 \lor v_5)$$ where $\lor$ represents the or boolean connective, $\land$ represents and and $\neg v_i$ is the negation of $v_i$.

Given a set of clauses $C_1, C_2,\dots , C_m$ on the variables $v_1, v_2, \dots , v_n$, the satisfiability problem is to determine if the formula $$C_1\land C_2\land \dots \land C_m$$ is satisfiable. That is, is there an assignment of values to the variables so that the above formula evaluates to $true$. Clearly, this requires that each $C_j$ evaluate to $true$.

Please write a program to solve the satisfiability problem.

Input

To represent an instance of such problems, we will create an input file that contains all of the information needed to define a satisfiability problem. This file will be an ASCII file consisting of a two major sections: the preamble and the clauses.

The Preamble. The preamble contains information about the instance. This information is contained in lines. Each line begins with a single character (followed by a space) that determines the type of line. These types are as follows:

Comments. Comment lines give human-readable information about the file and are ignored by programs. Comment lines appear at the beginning of the preamble. Each comment line begins with a lowercase character c.
c This is an example of a comment line.
Problem line. There is one problem line per input file. The problem line must appear before any node or arc descriptor lines. For cnf instances, the problem line has the following format.
p FORMAT VARIABLES CLAUSES
The lower-case character p signifies that this is the problem line. The FORMAT field allows programs to determine the format that will be expected, and should contain the word “cnf”. The VARIABLES field contains an integer value specifying $n$, the number of variables in the instance. The CLAUSES field contains an integer value specifying $m$, the number of clauses in the instance. This line must occur as the last line of the preamble.

The Clauses. The clauses appear immediately after the problem line. The variables are assumed to be numbered from $1$ up to $n$. It is not necessary that every variable appear in an instance. Each clause will be represented by a sequence of numbers, each separated by either a space, a tab, or a newline character. The non–negated version of a variable $v_i$ is represented by i; the negated version is represented by -i.

Each clauses is terminated by the value 0. Unlike many formats that represent the end of a clause by a new–line character, this format allows clauses to be on multiple lines.

Please read input from standard input.

The input meets the following conditions:

$0<n<30000$
$0<m<60000$

Output

Output sat if input is satisfiable, otherwise output unsat.

Sample Input

c Do You Like What You See?
c Van Darkholme
c That turns me on
c Oh that's good
c Deep dark fantasy
p cnf 5 4
 1 2 3 0
 -2 4 3 0
-2 -4 3 0
1 -3
 5 0

Sample Output

sat

Sample Description

$(v_1\lor v_2\lor v_3)\land (\neg v_2 \lor v_4 \lor v_3)\land (\neg v_2\lor \neg v_4\lor v_3)\land (v_1\lor \neg v_3 \lor v_5)$

Sample Code(wrong answer)

#include<bits/stdc++.h>
using namespace std;
int main(){
    string jinkela;
    while(cin>>jinkela);
    cout<<"sat"<<endl;
    return 0;
}

Judge Setting

run-time limit: 1800000 ms
memory limit: 62914560 byte
測資數量: 7