#!/usr/bin/python
# -*- coding: utf-8 -*-
"""Solve SAT by brute force.

"""

import sys

def main(args):
    solve(parse(args[1]))

def solve(expr):
    v = sorted(vars(expr))
    py = eval('lambda env: ' + compile(expr))
    env = {var: False for var in v}
    while True:
        if py(env):
            print "satisfiable:", env
            return
        if all(env[var] for var in v):
            break
        increment(env, v)

    print "not satisfiable"

def increment(env, v):
    for var in v:
        if env[var]:
            env[var] = False
        else:
            env[var] = True
            break

def parse(expr):
    "Maybe this is stupid and I should have just written the expression in Python."
    return_value = Constant(True)
    for disjunction in expr.split('&'):
        literals = Constant(False)
        assert disjunction.startswith('(') and disjunction.endswith(')'),\
            disjunction
        for literal in disjunction[1:-1].split('|'):
            negated = literal.startswith('~')
            var = variable(literal[1:] if negated else literal)
            literals = Or(literals, Not(var) if negated else var)

        return_value = And(return_value, literals)
    return return_value

def vars(expr):
    if isinstance(expr, Constant):
        return set()
    if isinstance(expr, Variable):
        return set([expr.name])
    if isinstance(expr, Not):
        return vars(expr.operand)
    if isinstance(expr, Binop):
        return vars(expr.left) | vars(expr.right)

    assert False, expr

def compile(expr):
    if isinstance(expr, Constant):
        return repr(expr.value)
    if isinstance(expr, Variable):
        return "env[%r]" % expr.name
    if isinstance(expr, Not):
        return "not (" + compile(expr.operand) + ")"
    if isinstance(expr, And):
        return "(%s) and (%s)" % (compile(expr.left),
                                  compile(expr.right))
    if isinstance(expr, Or):
        return "(%s) or (%s)" % (compile(expr.left),
                                 compile(expr.right))
    assert False, expr

class Expr: pass
class Binop(Expr):
    def __init__(self, left, right):
        self.left = left
        self.right = right
class And(Binop): pass
class Or(Binop): pass
class Not(Expr):
    def __init__(self, operand):
        self.operand = operand
class Constant(Expr):
    def __init__(self, value):
        self.value = value
class Variable(Expr):
    def __init__(self, name):
        self.name = name

variables = {}
def variable(name):
    if name not in variables:
        variables[name] = Variable(name)
    return variables[name]

if __name__ == '__main__':
    main(sys.argv)