Pagini recente » Cod sursa (job #1186507) | Cod sursa (job #3282941) | Cod sursa (job #56792) | Cod sursa (job #450857) | Cod sursa (job #1542858)
#include<iostream>
#include<fstream>
#include<vector>
using namespace std;
#define INPUT "2sat.in"
#define OUTPUT "2sat.out"
#define MAX_LIT 100000
#define MAX_DISJUNCTIONS 200000
int literals;
int conjunctions;
bool viz[2 * MAX_LIT];
int connexComponent[2 * MAX_LIT];
vector<int> adjacencyLists[2 * MAX_LIT];
vector<int> revertedAdjacencyLists[2 * MAX_LIT];
int noOfStronglyConnectedComp;
vector<int> component[2 * MAX_LIT + 1];
vector<int> orderList;
bool truth[MAX_LIT + 1];
void clearArray(int* arr, int n) {
for (int i = 0; i < n; ++i) {
arr[i] = 0;
}
}
void clearBoolArray(bool* arr, int n) {
for (int i = 0; i < n; ++i) {
arr[i] = false;
}
}
int getIndex(int i) {
if (i < 0) {
return i + literals;
}
return i + literals - 1;
}
void constructEdge(int left, int right) {
adjacencyLists[getIndex(-left)].insert(adjacencyLists[getIndex(-left)].end(), getIndex(right));
adjacencyLists[getIndex(-right)].insert(adjacencyLists[getIndex(-right)].end(), getIndex(left));
}
void readInput() {
ifstream in(INPUT);
in >> literals;
in >> conjunctions;
int left, right;
for (int i = 0; i < conjunctions; ++i) {
in >> left;
in >> right;
constructEdge(left, right);
}
in.close();
}
void firstDFS(int node) {
viz[node] = true;
for (int i = 0; i < adjacencyLists[node].size(); ++i) {
if (!viz[adjacencyLists[node].at(i)]) {
firstDFS(adjacencyLists[node].at(i));
}
}
orderList.insert(orderList.begin(), node);
}
void constructOrderList() {
orderList.clear();
clearBoolArray(viz, 2 * literals);
for (int i = 0; i < 2 * literals; ++i) {
if (!viz[i]) {
firstDFS(i);
}
}
}
void constructRevertedAdjacencyLists() {
for (int i = 0; i < 2 * literals; ++i) {
for (int j = 0; j < adjacencyLists[i].size(); ++j) {
revertedAdjacencyLists[adjacencyLists[i].at(j)].insert(revertedAdjacencyLists[adjacencyLists[i].at(j)].end(), i);
}
}
}
void secondDFS(int i, int t) {
connexComponent[i] = t;
component[t].insert(component[t].end(), i);
for (int j = 0; j < revertedAdjacencyLists[i].size(); ++j) {
if (!connexComponent[revertedAdjacencyLists[i].at(j)]) {
secondDFS(revertedAdjacencyLists[i].at(j), t);
}
}
}
void constructComponents() {
noOfStronglyConnectedComp = 1;
clearArray(connexComponent, 2 * literals);
for (int i = 0; i < 2 * literals; ++i) {
if (!connexComponent[orderList.at(i)]) {
secondDFS(orderList.at(i), noOfStronglyConnectedComp);
++noOfStronglyConnectedComp;
}
}
}
void constructStronglyConnectedComponents() {
constructOrderList();
constructRevertedAdjacencyLists();
constructComponents();
}
bool areOpposite(int i, int j) {
return (i + j == 2 * literals - 1);
}
bool isFormulaeSatisfiable() {
for (int i = 0; i < literals; ++i) {
if (connexComponent[i] == connexComponent[2 * literals - 1 - i]) {
return false;
}
}
return true;
}
void giveValues() {
clearBoolArray(viz, literals + 1);
for (int i = 1; i <= noOfStronglyConnectedComp; ++i) {
for (int j = 0; j < component[i].size(); ++j) {
int node = component[i].at(j);
if (node < literals) {
if (!viz[literals - node]) {
truth[literals - node] = true;
viz[literals - node] = true;
}
}
else {
if (!viz[node - literals + 1]) {
truth[node - literals + 1] = false;
viz[node - literals + 1] = true;
}
}
}
}
}
void printResult() {
ofstream out(OUTPUT, fstream::trunc | fstream::out);
if (!isFormulaeSatisfiable()) {
out << -1;
}
else {
giveValues();
if (truth[1] == false) {
out << "0";
}
else {
out << "1";
}
for (int i = 2; i <= literals; ++i) {
if (truth[i] == false) {
out << " 0";
}
else {
out << " 1";
}
}
}
out.close();
}
int main() {
readInput();
constructStronglyConnectedComponents();
printResult();
}