0 Judge
Code: 0
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.
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:
c
.
c This is an example of a comment line.
p FORMAT VARIABLES CLAUSES
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:
Output sat
if input is satisfiable, otherwise output unsat
.
$(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)$
#include<bits/stdc++.h>
using namespace std;
int main(){
string jinkela;
while(cin>>jinkela);
cout<<"sat"<<endl;
return 0;
}