백준 2-SAT - 4 C++
https://www.acmicpc.net/problem/112812-SAT 문제를 공부해보았습니다. 2-SAT문제는 아래와 같습니다.(x or y) : clause 를 대상으로 CNF 형태 (모두 and로 묶여 있는 형태) 에 대해 해가 존재하는 지를 판단 (만족하는 해가 있는가?) 하는 satisfiability 문제입니다. x or y == ~x -> yx or y == y or x == ~y -> x 이므로 CNF로 주어진 식을 아래와 같이 그래프로 표현할 수 있습니다. ex) (~x1 or x2) and (~x2 or x3) and (x1 or x3) and (x3 or x2) x1 -> x2, ~x2 -> ~x1x2 -> x3, ~x3 -> ~x2~x1 -> x3, ~x3 -> x1~x3 ..
알고리즘/백준
2025. 2. 23. 01:14