1405. 2-SAT Problem — Implication Graph + Bits

You are given numVars boolean variables and a list of clauses, each clause being a disjunction of two literals. A literal is encoded as a signed integer: v for variable v being true and -v for variable v being false (variables are numbered from 1). Determine whether some assignment satisfies every clause.

Input: A JSON object {"numVars": <variable count>, "clauses": [[literal, literal], ...]}.

Output: Return true if the formula is satisfiable, otherwise false.

Examples

Input: {"numVars":2,"clauses":[[1,2],[-1,2],[1,-2]]}
Output: true
Explanation: Setting both variables true satisfies every clause -> true.

Input: {"numVars":1,"clauses":[[1,1],[-1,-1]]}
Output: false
Explanation: One clause forces x1 true and another forces it false -> false.

Constraints

• 1 <= numVars <= 10^5
• 0 <= len(clauses) <= 10^5
• literals are non-zero and within the variable range

Asked by