2-SAT(Boolean Satisfiability)

F = (a||b) && (c||d) && (e||f)....   (||대신 xor등으로 변형가능함)

다음과 같이 F가 주어질 때, 

  1. F가 참이나 거짓이 되도록 할 수 있는지 여부

  2. F가 참/거짓일 떄 a,b,c,d,e,f,..의 값은 무엇인지

를 묻는 문제들이 대표적이다.

 

배경지식:

 0. p->q 

       == notp or q

  . p가 false라면 p->q는 항상 참이다.

 

 1. p || q

       ==  notp -> q && notq->p

       (두 항이 대우관계로 같은 말이다. 방향이 반대인 그래프를 하나 더 그려주기 위함인 것으로 이해함.)

 2. p xor q

       == (notp -> q && notq->p) && (p->notq && q->notp)

       (묶인 것 끼리 대우관계이다. 위와 같은 이유라고 이해함.)

 

 3. p->q를 그래프로 생각했을 떄,

    p->notp 경로가 존재하고 notp->p 경로가 존재하면 모순이 되서 맨 위에 서술한 F가 참/거짓으로 결정되지 않는 모순인 명제가 된다..!

    p정점과 notp정점이 같은 scc에 있는지 파악해 주면 된다.

   

    p번째 서술에 대해서

    p는 양수, notp는 음수라고 생각하고, 음수는 짝수번호를, 양수는 홀수번호를 할당해서 정점 번호를 매겨준다.

   

    p = p<0 ? -(p+1)*2 : p*2-1;        //p번째 서술에 대해서 양/음수에 맞는 정점번호 할당.

    int NOT(int p) { return p%2 ? p-1 : p+1; };   //not 연산을 간단하고 빠르게 처리할 수 있다.

 

 

typedef pair<int, int> P;

int id, dfsn[MAX * 2], SN, sn[MAX*2];
bool finished[MAX * 2];
vector<int> adj[MAX * 2];
stack<int> s;

inline int NOT(int p) { return p % 2 ? p - 1 : p + 1; }

int makeSCC(int curr) {};

int main() {
	int n, m; cin >> n >> m;
	for (int i = 0, u, v; i < m; i++) {
		cin >> u >> v;
		u = u < 0 ? -(u + 1) * 2 : u * 2 - 1;
		v = v < 0 ? -(v + 1) * 2 : v * 2 - 1;
		adj[NOT(u)].push_back(v);
		adj[NOT(v)].push_back(u);
	}
	for (int i = 0; i < 2 * n; i++)
		if (dfsn[i] == 0) makeSCC(i);

    //i와 not(i)가 같은 scc에 속하는지 여부 판단.
	bool flag = true;
	for (int i = 0; i < n; i++)
		if (sn[2 * i] == sn[2 * i + 1])
			flag = false;
            
    //F를 true로 만들기 위한 pi값들을 찾자.        
	int result[MAX];
	fill(result, result + MAX, -1);
	P p[MAX*2];
	for (int i = 0; i < 2 * n; i++) 
		p[i] = { sn[i],i };
	sort(p, p + 2 * n);
    
    //scc의 번호가 큰 것(DAG상 앞에 있는 것) 부터
	for (int i = 2 * n - 1; i >= 0; i--) {
		int val=p[i].second;
        //(val/2)번째 명제가 아직 안정해져있을 때,
        // 그 명제가 false가 되도록 설정 (p->q 에서 p가 false면 전체명제 항상 참)
		if (result[val / 2] == -1) result[val / 2] = !(val % 2);
	}

	for (int i = 0; i < n; i++) cout << result[i] << " ";
}

    

   기본문제:

https://www.acmicpc.net/problem/11280

https://www.acmicpc.net/problem/11281

11281번: 2-SAT - 4