題目大意：給你 m 個式子， 問你最少再新增多少式子能使沒有任何一種賦值方式使全部的式子為真。 並且在你給的式子中不能有非。

思路：根據題目給的m個式子可以建出2-Sat的圖， 現在問你最少加多少個邊使得2-Sat不成立， 我們可以發現我們給出的式子肯定是 a | a

的形式， 在題目中沒有 ~p | ~q這種形式必定無解， 否則最多增加2式子就能完成， 我們列舉a， 取check如果所有都不行就輸出2。

#include<bits/stdc++.h>
#define LL long long
#define fi first
#define se second
#define
 
 mk make_pair
#define PLL pair<LL, LL>
#define PLI pair<LL, int>
#define PII pair<int, int>
#define SZ(x) ((int)x.size())
#define ull unsigned long long

using namespace std;

const int N = 4000 + 7;
const int inf = 0x3f3f3f3f;
const LL INF = 0x3f3f3f3f3f3f3f3f;
const int mod = 1e9 + 7
 
;
const double eps = 1e-8;
const double PI = acos(-1);

int n, m;
bool flag;
int scc[N], stk[N], dfn[N], low[N], tot, cnt, idx;
bool in[N];
vector<int> G[N];

void tarjan(int u) {
    dfn[u] = low[u] = ++idx;
    stk[++tot] = u, in[u] = true;
    for(int v : G[u]) {
        if(!dfn[v]) tarjan(v), low[u] = min(low[u], low[v]);
        
 
else if(in[v]) low[u] = min(low[u], dfn[v]);
    }
    if(dfn[u] == low[u]) {
        cnt++;
        while(1) {
            int now = stk[tot--];
            scc[now] = cnt;
            in[now] = false;
            if(now == u) break;
        }
    }
}

int main() {
    scanf("%d%d", &n, &m);
    for(int i = 1; i <= m; i++) {
        int u, v; scanf("%d%d", &u, &v);
        if(u < 0 && v < 0) flag = true;
        if(u < 0) u = n - u;
        if(v < 0) v = n - v;
        if(u <= n) G[u+n].push_back(v);
        else G[u-n].push_back(v);
        if(v <= n) G[v+n].push_back(u);
        else G[v-n].push_back(u);
    }
    for(int i = 1; i <= n<<1; i++)
        if(!dfn[i]) tarjan(i);
    for(int i = 1; i <= n; i++)
        if(scc[i] == scc[i+n])
            return puts("0"), 0;
    if(!flag) return puts("-1"), 0;
    for(int i = 1; i <= n; i++, cnt = 0, idx = 0) {
        G[i+n].push_back(i);
        for(int j = 1; j <= n<<1; j++) dfn[j] = 0;
        for(int j = 1; j <= n<<1; j++) if(!dfn[j]) tarjan(j);
        for(int j = 1; j <= n; j++)
            if(scc[j] == scc[j+n])
                return puts("1"), 0;
        G[i+n].pop_back();
    }
    puts("2");
    return 0;
}

/*
*/