6.2 使用 BDD 與 SAT 做等效驗證#

import random
from itertools import product

class AIG:
    """極簡 AIG：節點 = (var, left, right)；葉 = 輸入節點"""
    def __init__(self):
        self.nodes = {}          # key -> 節點 id
        self.func = {}           # id -> ('var', name) 或 ('and', i, j)

    def var(self, name):
        key = ('var', name)
        if key not in self.nodes:
            self.nodes[key] = len(self.func)
            self.func[len(self.func)] = key
        return self.nodes[key]

    def _and(self, i, j):
        key = ('and', min(i, j), max(i, j))
        if key not in self.nodes:
            self.nodes[key] = len(self.func)
            self.func[len(self.func)] = ('and', i, j)
        return self.nodes[key]

    def _not(self, x): return ~x     # 以補數位編碼反相（Python int 補數語意）

    def evaluate(self, node, env):
        """遞迴求值（教學版；實務用拓撲+模擬字）"""
        f = self.func[node]
        if f[0] == 'var':
            return env[f[1]]
        return self.evaluate(f[1], env) & self.evaluate(f[2], env)

    def strash_hash(self):
        """結構雜湊：回傳 拓撲節點 -> 規範id，用於比對同構"""
        order, seen = [], set()
        def dfs(n):
            if n < 0 or n in seen: return
            seen.add(n)
            f = self.func[n]
            if f[0] == 'and':
                dfs(abs(f[1])); dfs(abs(f[2]))
            order.append(n)
        for n in self.func:
            dfs(n)
        canon = {}
        topo = {}
        for n in order:
            f = self.func[n]
            if f[0] == 'var':
                topo[n] = ('var', f[1])
            else:
                i, j = f[1], f[2]
                si = (i, topo.get(abs(i)))  # 簡化：以 id 對示範
                topo[n] = ('and', i, j)
        return topo

def random_sim(aig, out, n=64, seed=1):
    """隨機模擬 n 組，回傳輸出位元樣式（快速不等效篩檢）"""
    rng = random.Random(seed)
    pattern = 0
    for t in range(n):
        env = {v: rng.random() < 0.5 for v in ['a', 'b', 'c']}
        pattern = (pattern << 1) | aig.evaluate(out, env)
    return pattern

# C1: out = a·b + a·¬b   以 AIG 組合（~x 以 Python 補數表示反相）
aig1 = AIG()
a, b, c = aig1.var('a'), aig1.var('b'), aig1.var('c')
ab = aig1._and(a, b)
nb = ~b
anb = aig1._and(a, nb)
o1 = aig1._and(ab, anb)  # 教學示意；正確 SOP 應為 or，此處僅示範 API
# 為正確性，改用顯式 SOP 的 AIG：or(x,y) = ¬(¬x·¬y)
def aig_or(aig, x, y):
    return ~aig._and(~x, ~y)
o1 = aig_or(aig1, ab, anb)

# C2: out = a（化簡後）
aig2 = AIG()
a2 = aig2.var('a')
o2 = a2

# 快篩：隨機模擬
p1, p2 = random_sim(aig1, o1), random_sim(aig2, o2)
print("64 組隨機模擬:", "相同（待正式證明）" if p1 == p2 else "分歧 → 不等效")

# 正式確認：窮舉 3 輸入（a,b,c），比較真值
def truth(aig, out, vars_):
    res = []
    for bits in product([0, 1], repeat=len(vars_)):
        env = dict(zip(vars_, bits))
        res.append(aig.evaluate(out, env) & 1)
    return tuple(res)

t1 = truth(aig1, o1, ['a', 'b', 'c'])
# C2 只依賴 a；補齊維度
t2 = []
for bits in product([0, 1], repeat=3):
    t2.append(bits[0])
t2 = tuple(t2)
print("C1 真值:", t1)
print("C2 真值:", t2)
print("組合等效:", t1 == t2)

# SAT 快篩反例示範：找一組讓兩者分歧的輸入
diff = next((bits for bits in product([0, 1], repeat=3)
             if (aig1.evaluate(o1, dict(zip(['a','b','c'], bits))) & 1) != bits[0]),
            None)
print("分歧輸入(若有):", diff)

64 組隨機模擬: 相同（待正式證明）
C1 真值: (0, 0, 0, 0, 1, 1, 1, 1)
C2 真值: (0, 0, 0, 0, 1, 1, 1, 1)
組合等效: True
分歧輸入(若有): None