NOT a SAT problem
시간 제한2초메모리 제한1024 MB
주어진 CNF를 거짓으로 만들 수 있는지 판별하고, 가능하면 그렇게 만드는 변수 배정을 하나 출력한다.
문제
SAT 문제는 아래와 같이 정의된다.
- CNF가 주어졌을 때, 이 CNF가 참이 되도록 논리 변수들에 참과 거짓을 적절히 배정할 수 있는지 판별하는 문제를 SAT 문제라고 한다.
이때, CNF는 아래와 같이 정의된다.
- 하나 이상의 절이 (Logical AND)로 연결된 논리식을 CNF라고 한다.
이때, 절은 아래와 같이 정의된다.
- 하나 이상의, 논리 변수 또는 논리 변수의 (Logical NOT)이 (Logical OR)로 연결된 논리식을 절이라고 한다.
예를 들면, 와 은 절이다.
그리고, 위 두 절을 이은 는 CNF이다.
마지막으로, 이 CNF에 사용된 논리 변수 에 참과 거짓을 적절히 배정해서 CNF의 결과를 참으로 만드는 문제는 SAT 문제가 된다.
하지만 이 문제는 SAT 문제가 아니다. 그러니, 이 문제에서는 CNF의 결과를 참으로 만드는 대신, CNF의 결과를 거짓으로 만들어야 한다!
입력
첫째 줄에는 사용되는 논리 변수의 개수 과 CNF에 있는 절의 개수 이 주어진다.
둘째 줄부터 개의 줄에 걸쳐서, 절의 정보가 다음과 같이 공백으로 구분되어 주어진다.
각 줄의 첫 번째 정수는 절에 있는 논리 변수의 개수 를 의미하며, 이후 개의 정수가 공백으로 구분되어 주어진다. 여기서 주어지는 정수 는 양수일 경우 가 절에 들어있음을, 음수일 경우 가 절에 들어있음을 의미한다.
입력으로 주어지는 의 합은 이하이다.
출력
첫째 줄에 CNF의 결과를 거짓으로 만들 수 있다면 YES를, 아니면 NO를 출력한다.
만약 CNF의 결과를 거짓으로 만들 수 있다면, 둘째 줄에 CNF의 값을 거짓으로 만드는 의 값을 공백으로 구분하여 출력한다. 가 참이라면 을, 가 거짓이라면 을 출력한다.
만약 CNF의 결과를 거짓으로 만들 수 있는 경우가 여러 가지인 경우, 그중 아무거나 하나를 출력한다.