CNF

cnf.py

bneg = lambda x: ('~', x)
band = lambda x, y: ('and', x, y)
bor = lambda x, y: ('or', x, y)
imp = lambda x, y: bor(bneg(x), y)
iff = lambda x, y: band(imp(x,y), imp(y,x))
v = lambda x: ('var', x)

b0 = lambda x: band(x, bneg(x))


def match(pattern, data, vs):
    if isinstance(pattern, tuple) and isinstance(data, tuple) and len(pattern) == len(data):
        return all([match(x, y, vs) for x, y in zip(pattern, data)])
    elif isinstance(pattern, int):
        vs[pattern] = data
        return True
    else:
        return pattern == data

def matchvars(num):
    return [None for x in range(num)]

def negform(phi):
    x = matchvars(2)
    if match(bneg(bneg(0)), phi, x):
        return negform(x[0])
    if match(bneg(band(0, 1)), phi, x):
        return bor(negform(bneg(x[0])), negform(bneg(x[1])))
    if match(bneg(bor(0, 1)), phi, x):
        return band(negform(bneg(x[0])), negform(bneg(x[1])))
    if match(band(0, 1), phi, x):
        return band(negform(x[0]), negform(x[1]))
    if match(bor(0, 1), phi, x):
        return bor(negform(x[0]), negform(x[1]))
    return phi


def cnfneg(phi):
    x = matchvars(2)
    if match(band(0,1), phi, x):
        return cnfneg(x[0]) + cnfneg(x[1])

    if match(bor(0,1), phi, x):
        cnf1 = cnfneg(x[0])
        cnf2 = cnfneg(x[1])
        cnf = []
        for cl1 in cnf1:
            for cl2 in cnf2:
                cl = cl1 + cl2
                cnf.append(cl)
        return cnf

    return [[phi]]


def cnf(phi):
    return cnfneg(negform(phi))


# print(negform( bneg(bor(bneg(bneg('x')), 'y'))))
# print(cnf( bneg(bor(bneg(bneg('x')), 'y'))))
# print(cnf( imp('x', 'y')))
# print(cnf( iff('x', 'y')))
# print(cnf(iff('x', b0(v(0)))))

import random

coinflip = lambda: random.randint(0,1)

n = 240
mat_a = [
        [ coinflip() for x in range(n) ]
        for y in range(n) ]



print(mat_a)