6.1 組合等效性檢查#

def tseitin_and(z, a, b): return [[-z, a], [-z, b], [z, -a, -b]]
def tseitin_or(z, a, b):  return [[z, -a], [z, -b], [-z, a, b]]
def tseitin_not(z, a):    return [[-z, -a], [z, a]]
def tseitin_xor(z, a, b): return [[-z, a, b], [-z, -a, -b],
                                  [z, a, -b], [z, -a, b]]

def tseitin(net, next_var):
    """
    net: list of (gate_id, 'and'/'or'/'not'/'xor'/'buf', inputs, output)
    回傳 (clauses, var_map)；var_map 把節點映射到 CNF 變數
    """
    clauses, vmap = [], {}
    def var_of(node):
        nonlocal next_var
        if node not in vmap:
            vmap[node] = next_var; next_var += 1
        return vmap[node]
    for gid, op, ins, out in net:
        z = next_var; next_var += 1
        vmap[gid] = z
        a, b = (var_of(ins[0]), var_of(ins[1]) if len(ins) > 1 else None)
        if op == 'and':   clauses += tseitin_and(z, a, b)
        elif op == 'or':  clauses += tseitin_or(z, a, b)
        elif op == 'not': clauses += tseitin_not(z, a)
        elif op == 'xor': clauses += tseitin_xor(z, a, b)
    return clauses, vmap, next_var

def miter_cnf(net1, net2, outputs1, outputs2, next_var):
    clauses, vmap1, next_var = tseitin(net1, next_var)
    clauses2, vmap2, next_var = tseitin(net2, next_var)
    clauses += clauses2
    # 輸出 XOR + 全 OR
    xors = []
    for o1, o2 in zip(outputs1, outputs2):
        z = next_var; next_var += 1
        clauses += tseitin_xor(z, vmap1[o1], vmap2[o2])
        xors.append(z)
    z = next_var; next_var += 1
    for x in xors:                              # OR of xors
        clauses += tseitin_or(z, x, x) if False else []
    # 直接編碼 OR(z, x1..xk)：z=1 當任一 xi=1
    clauses.append([z] + [-x for x in xors])
    for x in xors:
        clauses.append([-z, x])
    return clauses, vmap1, vmap2, next_var, z

# ---- 簡化 SAT：小實例用窮舉（教學用；實務接 MiniSat） ----
def sat_bruteforce(clauses, nvars):
    from itertools import product
    for bits in product([True, False], repeat=nvars):
        env = {i + 1: bits[i] for i in range(nvars)}
        if all(any(env[abs(l)] == (l > 0) for l in c) for c in clauses):
            return env
    return None

# 例：C1 = a·b + a·¬b  （兩閘）；C2 = a  （合成後化簡）
net1 = [("n1", "and", ["a", "b"], None),
        ("n2", "not",  ["b"], None),
        ("n3", "and", ["a", "n2"], None),
        ("out1", "or", ["n1", "n3"], None)]
net2 = [("buf", "and", ["a", "a"], None),
        ("out2", "and", ["buf", "a"], None)]
clauses, v1, v2, nv, z = miter_cnf(net1, net2,
                                   ["out1"], ["out2"], 1)
model = sat_bruteforce(clauses, nv)
if model is None:
    print("UNSAT → 兩電路組合等效")
else:
    print("SAT → 不等效! 反例輸入:",
          {k: model[v] for k, v in v1.items() if k in ('a', 'b')})

# 反例驗證：故意改 C2 為 a∨b 製造不等效
net3 = [("out2", "or", ["a", "b"], None)]
clauses, v1, v2, nv, z = miter_cnf(net1, net3,
                                   ["out1"], ["out2"], 1)
model = sat_bruteforce(clauses, nv)
print("第二組:", "等效" if model is None else
      f"不等效! 反例 a={model[v1['a']]}, b={model[v1['b']]}")

UNSAT → 兩電路組合等效
第二組: 不等效! 反例 a=False, b=True