Two SAT Implication Problem

Two SAT Implication Problem — ExecCode Hard DSA Practice

Solve the Two SAT Implication problem on ExecCode. Free online hard DSA practice in Graph. Write and run code in Java, C++, Python — no signup required to run.

Problem description

Each variable is true or false. A clause (a OR b) uses 1-based indices; a negative index is negation. Build the implication graph, take Tarjan strongly connected components, and reject if any variable lies in the same component as its negation. The condensation is a DAG you would use for assigning values. Offline edge updates would switch to DSU rollback; path queries on a tree would switch to Mo on trees. This problem is the 2-SAT core. Return 1 if the formula is satisfiable, otherwise 0. You are given: n — number of boolean variables clauses — list of [a, b] disjunctions, 1-based, negatives negate Return 1 if satisfiable, else 0. Both literals in a clause may be the same variable. (x OR x) forces x true.

Examples

Input {'n': 2, 'clauses': [[1, 2], [-1, 2]]}; Output 1. Input {'n': 1, 'clauses': [[1, 1], [-1, -1]]}; Output 0. Input {'n': 3, 'clauses': []}; Output 1

Constraints

Empty clause list is satisfiable a and b are never 0 n >= 1 in typical tests

Practice Two SAT Implication free on ExecCode. Browse DSA problems, topic map, and placement guides.