[JS] 2-SAT

충족 가능성 문제란 여러 개의 boolean 변수들로 이루어진 표현식에서, 각 변수의 값을 true, false 중 하나로 설정하여 전체 식의 결과를 true로 만들 수 있는지 확인하는 문제입니다.

( x || y ) && ( !y || z ) && ( x || !z ) && ( z || y )

표현식은 괄호로 분리된 이중 구조를 가지고 있습니다. 괄호 안쪽으로는 두 변수 혹은 NOT 변수들과 OR 연산으로 이루어져 있고, 바깥엔 AND 연산이 있습니다.

이때 괄호 단위를 절(Clause)이라 하며, 이렇게 절의 AND 연산으로만 표현된 식의 형태를 CNF(Conjunctive Normal Form)라고 합니다.

각 절이 모두 true여야만 전체식도 true가 될 것이고, 따라서 각 절의 변수들 중 하나라도 true가 되도록 만드는 것이 문제를 푸는 방향입니다. 이때 각 절의 변수 개수가 최대 2개인 경우를 2-SAT이라고 합니다.

const fs = require("fs");
const input = fs.readFileSync("/dev/stdin", "utf8").trim().split("\n");

function solution() {
  const { n, sections, variableCount } = parseInput();
  const { connection, reverseConnection } = makeConnection(sections, variableCount);
  const topologicalSort = makeTopologicalSort(connection, variableCount);
  const group = decideGroup(reverseConnection, topologicalSort, variableCount);
  const res = validateResult(n, group);
  printResult(res);
}

function parseInput() {
  const [n, m] = input[0].split(" ").map(Number);
  const sections = input.slice(1, 1 + m).map((line) => line.split(" ").map(Number));
  const variableCount = (n << 1) + 1;
  return { n, m, sections, variableCount };
}

function makeConnection(sections, variableCount) {
  const connection = Array.from({ length: variableCount + 1 }, () => []);
  const reverseConnection = Array.from({ length: variableCount + 1 }, () => []);
  sections.forEach(([a, b]) => {
    a = a > 0 ? toTrue(a) : toFalse(-a);
    b = b > 0 ? toTrue(b) : toFalse(-b);
    connection[not(a)].push(b);
    connection[not(b)].push(a);
    reverseConnection[b].push(not(a));
    reverseConnection[a].push(not(b));
  });
  return { connection, reverseConnection };
}

function not(variable) {
  return variable ^ 1;
}

function toTrue(variable) {
  return variable << 1;
}

function toFalse(variable) {
  return (variable << 1) | 1;
}

function makeTopologicalSort(connection, variableCount) {
  const visit = Array(variableCount + 1);
  const topologicalSort = [];
  for (let variable = 2; variable <= variableCount; variable += 1) {
    if (!visit[variable]) {
      makeTopologicalSortUnit(variable, visit, topologicalSort, connection);
    }
  }
  return topologicalSort;
}

function makeTopologicalSortUnit(current, visit, topologicalSort, connection) {
  visit[current] = true;
  connection[current].forEach((next) => {
    if (!visit[next]) {
      makeTopologicalSortUnit(next, visit, topologicalSort, connection);
    }
  });
  topologicalSort.push(current);
}

function decideGroup(reverseConnection, topologicalSort, variableCount) {
  const group = Array(variableCount + 1);
  for (let i = topologicalSort.length - 1; i >= 0; i -= 1) {
    const variable = topologicalSort[i];
    if (group[variable] === undefined) {
      decideGroupUnit(variable, i, group, reverseConnection);
    }
  }
  return group;
}

function decideGroupUnit(current, id, group, reverseConnection) {
  group[current] = id;
  reverseConnection[current].forEach((next) => {
    if (group[next] === undefined) {
      decideGroupUnit(next, id, group, reverseConnection);
    }
  });
}

function validateResult(n, group) {
  for (let num = 1; num <= n; num += 1) {
    const numTrue = toTrue(num);
    const numFalse = toFalse(num);
    if (group[numTrue] === group[numFalse]) {
      return false;
    }
  }
  return true;
}

function printResult(res) {
  console.log(res ? 1 : 0);
}

solution();