Problem 7: 2-SAT Problem

Problem Statement: Given a 2-SAT problem with n variables and m clauses, determine if there exists an assignment that satisfies all clauses.

Input

First line contains n and m. Each of the next m lines contain two integers a and b representing a clause (a OR b), where a and b can be negative indicating negation.

Output

Print "YES" if a satisfying assignment exists, otherwise print "NO".

Examples


Input:
2 3
1 2
-1 2
-1 -2

Output:
YES

Solution Explanation

Method 1: Construct the implication graph and use Kosaraju's algorithm to find strongly connected components, then check if any variable and its negation fall in the same component. Method 2: Use the Tarjan's algorithm to identify SCCs inline during DFS traversal, which also allows you to check satisfiability.

Solution in C++


#include 
#include 
#include 
#include 
#include 
using namespace std;

int var(int x, int n){
    return (x > 0) ? x - 1 : n - x - 1;
}

void addEdge(int u, int v, vector> &g){
    g[u].push_back(v);
}

int main(){
    int n, m;
    cin >> n >> m;
    vector> g(2*n), gr(2*n);
    auto add_clause = [&](int a, int b){
        int u = var(-a, n), v = var(b, n);
        int u2 = var(-b, n), v2 = var(a, n);
        addEdge(u, v, g); addEdge(v, u, gr);
        addEdge(u2, v2, g); addEdge(v2, u2, gr);
    };
    int a, b;
    for(int i=0;i> a >> b;
        add_clause(a, b);
    }
    // Kosaraju
    vector used(2*n, false);
    vector order, comp(2*n);
    function dfs1 = [&](int v){
        used[v] = true;
        for(auto u : g[v]) if(!used[u]) dfs1(u);
        order.push_back(v);
    };
    for(int i=0;i<2*n;i++) if(!used[i]) dfs1(i);
    function dfs2 = [&](int v, int cl){
        comp[v] = cl;
        for(auto u : gr[v]) if(comp[u]==-1) dfs2(u, cl);
    };
    fill(comp.begin(), comp.end(), -1);
    int idx = 0;
    for(int i = 2*n-1; i>=0; i--){
        int v = order[i];
        if(comp[v] == -1) dfs2(v, idx++);
    }
    for(int i=0;i