2010年12月17日星期五

Proof of my CNF converter

定义:
一个句子是一个变量或一个满足下列条件的list,至少有3个元素,第一个元素是连词AND或OR,其余元素是句子(递归定义),这些句子称作子句。没有NOT这种连词。
称一个句子是CNF的,若它是一个变量或满足下列条件的list。第一个元素是AND,其余元素是变量或满足下列条件的list。第一个元素是OR,其余元素是变量。(非递归定义)
对偶地可以定义DNF。
称一个句子是melt的,若任何一个子句的连词都不同于这个句子的连词。显然CNF和DNF是melt的
称两个句子等价,若他们用到的变量相同,且对于任何一种变量分配,他们表达式求值后同真同假。
任何句子可以转化成等价的melt形式,只需要将多余的连词合并即可。

命题:
如果句子x1,...,xn都是melt的,则melt(Op,x1,...,xn)=[Op]+trim(x1,Op)+...+trim(xn,Op)也是melt的,其中Op是AND或OR
其中,trim(x,Op)=x[1:]若Op是x的连词,否则trim(x,Op)=[x]
证明:显然

命题:
如果句子x1,...,xn都是CNF的,
那么melt(AND,x1,...,xn)也是CNF的
证明:显然

命题:
如果句子x1,...,xn都是CNF的,将他们的子句(n个列向量)的卡氏积写成一串n阶向量y1,...,ym,|yk|=n,
那么AND,OR(y1),...,OR(ym)也是CNF的
证明:反复应用交换律即可。

基于上述命题,可知昨天的递归算法正确。

按照定义验证也很直接,只需代入全部可能的变量分配即可。python可以帮你方便地对表达式求值。
import itertools

def is_leaf(x):
    return type(x)==type("")

def to_str(x):
    return is_leaf(x) and x or "(" + (" "+x[0]+" ").join(map(lambda e : to_str(e), x[1:])) + ")"

def _nfy(x, O1, O2):
    if is_leaf(x):   return x
    if x[0]==O1:  return melt([O1] + map(lambda e : _nfy(e, O1, O2), x[1:]))
    return [O1] + [[O2]+list(c) for c in itertools.product(*map(lambda e : is_leaf(e) and [e] or _nfy(e, O1, O2)[1:], x[1:]))]       

def cnfy(x): return _nfy(x, "and", "or")

def dnfy(x): return _nfy(x, "or", "and")

def melt(x):
    if is_leaf(x): return x
    ret = x[:1]
    for e in x[1:]:
        if not is_leaf(e) and e[0]==ret[0]:   ret+=melt(e)[1:]
        else:                                 ret.append(melt(e))
    return ret

def terms(x):
    ret = set()
    q=[x]
    while len(q)>0:
        head = q.pop(0)
        if is_leaf(head):
            ret.add(head)
        else:
            q+=head[1:]
    return ret

def eq(x, y):
    xterms = terms(x)
    yterms = terms(y)
    if xterms != yterms:
        return False
    xstr=to_str(x)
    ystr=to_str(y)
    termlist = list(xterms)
    for assignment in itertools.product(*([("True", "False")]*len(termlist))):
        x1=xstr
        y1=ystr
        for i, a in enumerate(assignment):
            x1=x1.replace(termlist[i], a)
            y1=y1.replace(termlist[i], a)
        if eval(x1) != eval(y1):
            return False
    return True
       
def main():
    x = ["or", "x1", ["and", ["or", "x2", ["and", "x3", "x4", ["or", ["and", "x5", "x6"], "x7", ["or", ["and", "x8", "x9"], "x10"]]]], "x11"]]
    print terms(x)
    print eq(x, x),
    print eq(x, cnfy(x)),
    print eq(x, dnfy(x))
   
main()

P.S.
修正了_nfy函数最后一行:用不着melt

没有评论: