2-SAT Implication Edge Set

Problem

Build the implication graph of a 2-SAT instance as a sorted edge list.

Literal +k (variable k true) maps to node 2*(k-1) and literal -k (false) maps to node 2*(k-1)+1. Each clause [a, b] adds the two implications not(a) -> b and not(b) -> a, deduplicated. Return all implication edges as sorted [from, to] pairs. clauses is a list of signed literal pairs.

Hint

A clause is equivalent to two contrapositive implications.

Test cases

case 1

in: [2,[[1,-2]]]

expected: [[1,3],[2,0]]

case 2

in: [3,[[1,2],[-1,3]]]

expected: [[0,4],[1,2],[3,0],[5,1]]

case 3

in: [1,[[1,1]]]

expected: [[1,0]]

case 4

in: [2,[[1,2],[-1,-2],[1,-2]]]

expected: [[0,3],[1,2],[1,3],[2,0],[2,1],[3,0]]

Starter codePython

def two_sat_implication_edges(n, clauses):
    # Your code here
    pass

4 test cases · run your code against them in the editor