3D matching reduction to SAT

3dm-to-sat.py

def match_to_sat(xyz, T):
    coverage = [[[] for _ in range(xyz[i])] for i in range(3)]
    for i, t in enumerate(T):
        for j, v in enumerate(t):
            coverage[j][v].append(i)

    instance = set()
    for c in coverage:
        for x in c:
            # if there is points not covered by any set, add a always false statement.
            if len(x) == 0:
                instance.add("~x%i" % len(T))
                instance.add("x%i" % len(T))
            elif len(x) == 1:
                instance.add("x%i" % x[0])
            else:
                for i, m in enumerate(x):
                    for n in x[i + 1:]:
                        instance.add("(x%i v x%i)" % (m, n))
                        instance.add("(~x%i v ~x%i)" % (m, n))
    return " ^ ".join(instance)

if __name__ == "__main__":
    # Number of points per set
    XYZ = [2, 2, 2]
    # Groups
    L = [[0, 0, 1], [1, 1, 0], [0, 0, 0]]
    print(match_to_sat(XYZ, L))
    # (x0 v x2) ^ (~x0 v ~x2) ^ x0 ^ (~x1 v ~x2) ^ x1 ^ (x1 v x2)