Ponder This - August 2009

ponder.py

#! /usr/bin/env python3
# Solution to http://domino.research.ibm.com/Comm/wwwr_ponder.nsf/Challenges/August2009.html
import string
import sys


def main():
    a = Expression('a', int('00001111', 2))
    b = Expression('b', int('00110011', 2))
    c = Expression('c', int('01010101', 2))
    closure = make_closure((a, b, c))
    v = (~a).val
    w = (~b).val
    x = (~c).val
    tested_negation_pairs = set()
    count = 0
    for v1 in closure:
        e1 = ~closure[v1]
        e1_val = e1.val
        if e1_val in closure:
            continue
        closure2 = derive_closure(closure, e1)
        for v2 in closure2:
            e2 = ~closure2[v2]
            e2_val = e2.val
            if e2_val in closure2:
                continue
            p = (e1_val, e2_val) if e1_val < e2_val else (e2_val, e1_val)
            if p in tested_negation_pairs:
                continue
            tested_negation_pairs.add(p)
            closure3 = derive_closure(closure2, e2)
            count += 1
            if count % 50 == 0:
                print('Iteration #{0}'.format(count))
            if v in closure3 and w in closure3 and x in closure3:
                solution = (closure3[v], closure3[w], closure3[x])
                print('A solution has found at iteration #{0}'.format(count))
                print('not(a) = {0}'.format(solution[0]))
                print('not(b) = {0}'.format(solution[1]))
                print('not(c) = {0}'.format(solution[2]))
                print(encode_solution(solution))


class Expression:

    def __init__(self, name, val, sub1=None, sub2=None, bits=8):
        self.name = name
        self.val = val
        self.sub1 = sub1
        self.sub2 = sub2
        self.size = 1 + (sub1.size if sub1 else 0) + (sub2.size if sub2 else 0)
        self.bits = sub1.bits if sub1 else bits
        self.mask = (1 << bits) - 1
        if sub2 and sub1.bits != sub2.bits:
            raise ValueError('subexpression bit lengths not match')

    def __and__(self, e):
        return Expression('and', self.val & e.val, self, e)

    def __or__(self, e):
        return Expression('or', self.val | e.val, self, e)

    def __invert__(self):
        return Expression('not', self.val ^ self.mask, self)

    def __str__(self):
        name = self.name
        if name == 'and':
            return 'and(%s, %s)' % (str(self.sub1), str(self.sub2))
        if name == 'or':
            return 'or(%s, %s)' % (str(self.sub1), str(self.sub2))
        if name == 'not':
            return 'not(%s)' % str(self.sub1)
        return name


def make_closure(initial_exprs):
    closure = {}
    for e in initial_exprs:
        derive_closure(closure, e, in_place=True)
    return closure


def derive_closure(closure, new_expr, in_place=False):
    closure = closure if in_place else dict(closure)
    if new_expr.val in closure and new_expr.size > closure[new_expr.val].size:
        return closure
    closure[new_expr.val] = new_expr
    candidates = []
    candidates.extend(new_expr & e for e in closure.values())
    candidates.extend(new_expr | e for e in closure.values())
    new_exprs = []
    for e in candidates:
        v = e.val
        if v not in closure:
            closure[v] = e
            new_exprs.append(e)
        elif e.size < closure[v].size:
            replace(closure, v, e)
    for e in new_exprs:
        derive_closure(closure, e, in_place=True)
    return closure


def replace(closure, val, expr):
    old = closure[val]
    closure[val] = expr
    for x in closure.values():
        if x.sub1 is old:
            x.sub1 = expr
            x.size += expr.size - old.size
        if x.sub2 is old:
            x.sub2 = expr
            x.size += expr.size - old.size


def encode_solution(solution):
    code = []
    table = {}
    for e in solution:
        encode_expression(e.sub1, code, table)
        encode_expression(e.sub2, code, table)
    for e in solution:
        encode_expression(e, code, table)
    return ''.join(code)


def encode_expression(e, code, table):
    if e.val in table:
        return table[e.val]
    if e.size == 1:
        return e.name
    if e.name == 'not':
        a = encode_expression(e.sub1, code, table)
        return a.upper() if a.islower() else a.lower()
    a = encode_expression(e.sub1, code, table)
    b = encode_expression(e.sub2, code, table)
    c = (a, b) if (a.lower() < b.lower()) == (e.name == 'and') else (b, a)
    code.extend(c)
    x = chr(ord('d') + len(table))
    table[e.val] = x
    return x


if __name__ == "__main__":
    main()