Pagini recente » Cod sursa (job #3295573) | Cod sursa (job #2635219) | Cod sursa (job #3191578) | Cod sursa (job #2958360) | Cod sursa (job #3296954)
#include<bits/stdc++.h>
using namespace std;
//#pragma GCC optimize("O3,unroll-loops")
//#pragma GCC target("avx2,bmi,bmi2,lzcnt,popcnt")
string numeFisier="2sat";
ifstream fin(numeFisier+".in"); ofstream fout(numeFisier+".out");
#define cin fin
#define cout fout
#define INIT ios_base :: sync_with_stdio(false); cin.tie(NULL); cout.tie(NULL);mt19937 rng(chrono::steady_clock::now().time_since_epoch().count());
#define mp make_pair
#define pb push_back
#define ft first
#define sc second
#define ll long long
#define pii pair<int, int>
#define count_bits __builtin_popcount
#define int ll
// An instance of this struct must be instantiated manually
struct StronglyConnectedComponents{
int n,m;
vector< vector<int> > g;
int indexArray0=0;
vector<int> indexArray;
vector<int> lowlink;
vector<bool> onStack;
stack<int> st;
vector< vector<int> > componentOfRepresentative;
vector<int> representative;
//Strongly connected components in reverse topological order
vector< vector<int> > stronglyConnectedComponents;
//CondensationGraph
vector< vector<int> > condensationGraph;
void getNM(int N, int M){
n =N;
m = M;
g.assign(n+10, {});
indexArray.assign(n+10, 0);
lowlink.assign(n+10, 0);
onStack.assign(n+10, 0);
}
void strongConnected(int u){
indexArray0++;
indexArray[u] =indexArray0;
lowlink[u] = indexArray0;
st.push(u);
onStack[u]=true;
for(int v:g[u]){
if(!indexArray[v]){
strongConnected(v);
lowlink[u]=min(lowlink[u], lowlink[v]);
}
else{
if( onStack[v] ){
lowlink[u] = min(lowlink[u], lowlink[v]);
}
}
}
if( lowlink[u]==indexArray[u] ){
stronglyConnectedComponents.pb({});
while(st.top()!=u ){
onStack[st.top()]=false;
stronglyConnectedComponents.back().pb(st.top());
st.pop();
}
stronglyConnectedComponents.back().pb(u);
st.pop();
onStack[u]=false;
}
}
void buildStronglyConnectedComponents(){
if(!stronglyConnectedComponents.empty()){
return;
}
for(int i=1; i<=n; i++){
if(indexArray[i]==0){
strongConnected(i);
}
}
}
void buildCondensationGraph(){
buildStronglyConnectedComponents();
if( !condensationGraph.empty() ){
return;
}
representative.assign(n+10, 0);
componentOfRepresentative.assign(n+10, {});
for(auto component: stronglyConnectedComponents){
int repr = component[0];
for(auto u : component){
representative[u]=repr;
}
componentOfRepresentative[repr]=component;
}
};
};
struct SAT2{
int numberOfVariables, numberOfClauses;
vector<vector<int>> clauses;
//the actual solution
//if is not satisfiable, will be {-1}
vector<int> assignment;
int getNodeFromVariable(int u){
u+=numberOfVariables;
if(u<numberOfVariables){
u++;
}
return u;
}
int getVariableFromNode(int u){
if(u<=numberOfVariables){
return u-numberOfVariables-1;
}
else{
return u-numberOfVariables;
}
}
void assign(int u, bool truth){
if( u<0 ){
truth = !truth;
u = -u;
}
assignment[u] = ((int)truth);
}
void satisfy(){
StronglyConnectedComponents implications;
implications.getNM(numberOfVariables*2, numberOfClauses*2);
for(auto clause : clauses){
int u = clause[0];
int v = clause[1];
int notU = getNodeFromVariable(-u);
int notV = getNodeFromVariable(-v);
u = getNodeFromVariable(u);
v = getNodeFromVariable(v);
implications.g[ notU ].pb( v );
implications.g[notV].pb(u);
}
implications.buildCondensationGraph();
assignment.assign(numberOfVariables+10, -1);
for( auto component : implications.stronglyConnectedComponents ){
int repr = implications.representative[component[0]];
int notRepr = implications.representative[getNodeFromVariable( -getVariableFromNode(repr) )];
if(repr == notRepr){
assignment={-1};
return;
}
for (auto u : component){
int varU = getVariableFromNode(u);
int varNotU = -varU;
if( assignment[ abs( varU ) ]!=-1 ){
continue;
}
assign( varU, true );
assign(varNotU, false);
}
}
}
} sat2;
void input(){
cin>>sat2.numberOfVariables>>sat2.numberOfClauses;
for(int i=1, u, v; i<=sat2.numberOfClauses; i++){
cin>>u>>v;
sat2.clauses.pb({u,v});
}
}
void solve(){
sat2.satisfy();
}
void output(){
if(((int)sat2.assignment.size())==1){
cout<<"-1";
return;
}
for(int i = 1; i<=sat2.numberOfVariables; i++){
cout<<sat2.assignment[i]<<" ";
}
}
int32_t main(){
INIT
input();
solve();
output();
return 0;
}