1087. 2-SAT Problem Using Implication Graph

Given n boolean variables and a list of clauses, each clause (a OR b) over literals encoded as +(i+1) for variable i true and -(i+1) for false, determine whether the formula is satisfiable. Build the implication graph and use strongly connected components. Return true or false. The input is JSON {n, clauses}.

Input: JSON {n, clauses} with literals +/-(index+1).

Output: Boolean — true or false.

Examples

Input: {"n":2,"clauses":[[1,2],[-1,2],[1,-2]]}
Output: true
Explanation: Satisfiable, e.g. both true.

Input: {"n":1,"clauses":[[1,1],[-1,-1]]}
Output: false
Explanation: x and not-x cannot both hold.

Input: {"n":2,"clauses":[[1,2]]}
Output: true
Explanation: Easily satisfiable.

Constraints

• 1<=n<=10^5
• 1<=clauses<=10^5

Asked by