logic.py

# logic.py
# --------
# Licensing Information:  You are free to use or extend these projects for
# educational purposes provided that (1) you do not distribute or publish
# solutions, (2) you retain this notice, and (3) you provide clear
# attribution to UC Berkeley, including a link to http://ai.berkeley.edu.
# 
# Attribution Information: The Pacman AI projects were developed at UC Berkeley.
# The core projects and autograders were primarily created by John DeNero
# (denero@cs.berkeley.edu) and Dan Klein (klein@cs.berkeley.edu).
# Student side autograding was added by Brad Miller, Nick Hay, and
# Pieter Abbeel (pabbeel@cs.berkeley.edu).


"""Representations and Inference for the CS 188 Logic Project

Code originally from https://code.google.com/p/aima-python/
Modified heavily with additional convenience classes and functions as well
as an interface to the pycosat (picoSAT wrapper) library.
https://pypi.python.org/pypi/pycosat.
Original package contained implementations of functions and data structures
for Knowledge bases and First-Order Logic.
"""

import itertools, re
import agents
from logic_utils import *
import pycosat

#______________________________________________________________________________

class Expr:
    """A symbolic mathematical expression.  We use this class for logical
    expressions, and for terms within logical expressions. In general, an
    Expr has an op (operator) and a list of args.  The op can be:
      Null-ary (no args) op:
        A number, representing the number itself.  (e.g. Expr(42) => 42)
        A symbol, representing a variable or constant (e.g. Expr('F') => F)
      Unary (1 arg) op:
        '~', '-', representing NOT, negation (e.g. Expr('~', Expr('P')) => ~P)
      Binary (2 arg) op:
        '>>', '<<', representing forward and backward implication
        '+', '-', '*', '/', '**', representing arithmetic operators
        '<', '>', '>=', '<=', representing comparison operators
        '<=>', '^', representing logical equality and XOR
      N-ary (0 or more args) op:
        '&', '|', representing conjunction and disjunction
        A symbol, representing a function term or FOL proposition

    Exprs can be constructed with operator overloading: if x and y are Exprs,
    then so are x + y and x & y, etc.  Also, if F and x are Exprs, then so is
    F(x); it works by overloading the __call__ method of the Expr F.  Note
    that in the Expr that is created by F(x), the op is the str 'F', not the
    Expr F.   See http://www.python.org/doc/current/ref/specialnames.html
    to learn more about operator overloading in Python.

    WARNING: x == y and x != y are NOT Exprs.  The reason is that we want
    to write code that tests 'if x == y:' and if x == y were the same
    as Expr('==', x, y), then the result would always be true; not what a
    programmer would expect.  But we still need to form Exprs representing
    equalities and disequalities.  We concentrate on logical equality (or
    equivalence) and logical disequality (or XOR).  You have 3 choices:
        (1) Expr('<=>', x, y) and Expr('^', x, y)
            Note that ^ is bitwose XOR in Python (and Java and C++)
        (2) expr('x <=> y') and expr('x =/= y').
            See the doc string for the function expr.
        (3) (x % y) and (x ^ y).
            It is very ugly to have (x % y) mean (x <=> y), but we need
            SOME operator to make (2) work, and this seems the best choice.

    WARNING: if x is an Expr, then so is x + 1, because the int 1 gets
    coerced to an Expr by the constructor.  But 1 + x is an error, because
    1 doesn't know how to add an Expr.  (Adding an __radd__ method to Expr
    wouldn't help, because int.__add__ is still called first.) Therefore,
    you should use Expr(1) + x instead, or ONE + x, or expr('1 + x').
    """

    def __init__(self, op, *args):
        "Op is a string or number; args are Exprs (or are coerced to Exprs)."
        assert isinstance(op, str) or (isnumber(op) and not args)
        self.op = num_or_str(op)
        self.args = list(map(expr, args)) ## Coerce args to Exprs
        if not args and not is_prop_symbol(self.op):
            raise SyntaxError("Unacceptable symbol base name (%s). Name must start with an upper-case alphabetic character that and is not TRUE or FALSE." % self.op)

    def __call__(self, *args):
        """Self must be a symbol with no args, such as Expr('F').  Create a new
        Expr with 'F' as op and the args as arguments."""
        assert is_symbol(self.op) and not self.args
        return Expr(self.op, *args)

    def __repr__(self):
        "Show something like 'P' or 'P(x, y)', or '~P' or '(P | Q | R)'"
        if not self.args:         # Constant or proposition with arity 0
            return str(self.op)
        elif is_symbol(self.op):  # Functional or propositional operator
            return '%s(%s)' % (self.op, ', '.join(list(map(repr, self.args))))
        elif len(self.args) == 1: # Prefix operator
            return self.op + repr(self.args[0])
        else:                     # Infix operator
            return '(%s)' % (' '+self.op+' ').join(list(map(repr, self.args)))

    def __eq__(self, other):
        """x and y are equal iff their ops and args are equal."""
        return (other is self) or (isinstance(other, Expr)
            and self.op == other.op and self.args == other.args)

    def __ne__(self, other):
        return not self.__eq__(other)

    def __hash__(self):
        "Need a hash method so Exprs can live in dicts."
        return hash(self.op) ^ hash(tuple(self.args))

    # See http://www.python.org/doc/current/lib/module-operator.html
    # Not implemented: not, abs, pos, concat, contains, *item, *slice
    def __lt__(self, other):     return Expr('<',  self, other)
    def __le__(self, other):     return Expr('<=', self, other)
    def __ge__(self, other):     return Expr('>=', self, other)
    def __gt__(self, other):     return Expr('>',  self, other)
    def __add__(self, other):    return Expr('+',  self, other)
    def __sub__(self, other):    return Expr('-',  self, other)
    def __and__(self, other):    return Expr('&',  self, other)
    def __div__(self, other):    return Expr('/',  self, other)
    def __truediv__(self, other):return Expr('/',  self, other)
    def __invert__(self):        return Expr('~',  self)
    def __lshift__(self, other): return Expr('<<', self, other)
    def __rshift__(self, other): return Expr('>>', self, other)
    def __mul__(self, other):    return Expr('*',  self, other)
    def __neg__(self):           return Expr('-',  self)
    def __or__(self, other):     return Expr('|',  self, other)
    def __pow__(self, other):    return Expr('**', self, other)
    def __xor__(self, other):    return Expr('^',  self, other)
    def __mod__(self, other):    return Expr('<=>',  self, other)

class PropSymbolExpr(Expr):
    """An extension of Expr intended to represent a symbol. This SymbolExpr
    is a convenience for naming symbols, especially symbols whose names
    indicate an indexed value (e.g. Position[x,y] or Fluent[t]).
    Symbol name must begin with a capital letter. This class helps to add
    brackets with enumerated indices to the end of the name.
    """
    def __init__(self, sym_str, *index):
        """Constructor taking a propositional logic symbol name and an optional set of index values,
        creating a symbol with the base name followed by brackets with the specific
        indices.
        sym_str: String representing base name for symbol. Must begin with a capital letter.
        Examples:
        >>> red = PropSymbolExpr("R")
        >>> print (red)
        R
        >>> turnLeft7 = PropSymbolExpr("Left",7)
        >>> print (turnLeft7)
        Left[7]
        >>> pos_2_3 = PropSymbolExpr("P",2,3)
        >>> print (pos_2_3)
        P[2,3]
        """
        if not is_prop_symbol(sym_str):
            raise SyntaxError("Unacceptable symbol base name (%s). Name must start with an upper-case alphabetic character that and is not TRUE or FALSE." % sym_str)
        self.sym_str = sym_str
        self.indicies = index
        
        if len(index) == 0:
            Expr.__init__(self, sym_str)
        elif len(index) == 1:
            Expr.__init__(self, '%s[%d]' % (sym_str, index[0]))
        elif len(index) == 2:
            Expr.__init__(self, '%s[%d,%d]' % (sym_str, index[0], index[1]))
        elif len(index) == 3:
            Expr.__init__(self, '%s[%d,%d,%d]' % (sym_str, index[0], index[1], index[2]))
        else:
            raise SyntaxError("Too many arguments to SymbolExpr constructor. SymbolExpr(symbol_str, [index1], [index2], [index3]")
        
    def getBaseName(self):
        return self.sym_str
    
    def getIndex(self):
        return self.indicies
    
    @staticmethod
    def parseExpr(symbol):
        tokens = re.findall(r"[\w]+", str(symbol))
        if len(tokens)==1:
            return tokens[0]
        elif len(tokens)==2:
            return tuple(tokens)
        else:
            return (tokens[0], tuple(list(map(int,tokens[1:]))))

def expr(s):
    """Create an Expr representing a logic expression by parsing the input
    string. Symbols and numbers are automatically converted to Exprs.
    In addition you can use alternative spellings of these operators:
      'x ==> y'   parses as   (x >> y)    # Implication
      'x <== y'   parses as   (x << y)    # Reverse implication
      'x <=> y'   parses as   (x % y)     # Logical equivalence
      'x =/= y'   parses as   (x ^ y)     # Logical disequality (xor)
    But BE CAREFUL; precedence of implication is wrong. expr('P & Q ==> R & S')
    is ((P & (Q >> R)) & S); so you must use expr('(P & Q) ==> (R & S)').
    >>> expr('P <=> Q(1)')
    (P <=> Q(1))
    >>> expr('P & Q | ~R(x, F(x))')
    ((P & Q) | ~R(x, F(x)))
    """
    if isinstance(s, Expr): return s
    if isnumber(s): return Expr(s)
    ## Replace the alternative spellings of operators with canonical spellings
    s = s.replace('==>', '>>').replace('<==', '<<')
    s = s.replace('<=>', '%').replace('=/=', '^')
    ## Replace a symbol or number, such as 'P' with 'Expr("P")'
    s = re.sub(r'([a-zA-Z0-9_.]+)', r'Expr("\1")', s)
    ## Now eval the string.  (A security hole; do not use with an adversary.)
    return eval(s, {'Expr':Expr})

def is_symbol(s):
    "A string s is a symbol if it starts with an alphabetic char."
    return isinstance(s, str) and s[:1].isalpha()

def is_var_symbol(s):
    "A logic variable symbol is an initial-lowercase string."
    return is_symbol(s) and s[0].islower()

def is_prop_symbol(s):
    """A proposition logic symbol is an initial-uppercase string other than
    TRUE or FALSE."""
    return is_symbol(s) and s[0].isupper() and s != 'TRUE' and s != 'FALSE'

def variables(s):
    """Return a set of the variables in expression s.
    >>> ppset(variables(F(x, A, y)))
    set([x, y])
    >>> ppset(variables(F(G(x), z)))
    set([x, z])
    >>> ppset(variables(expr('F(x, x) & G(x, y) & H(y, z) & R(A, z, z)')))
    set([x, y, z])
    """
    result = set([])
    def walk(s):
        if is_variable(s):
            result.add(s)
        else:
            for arg in s.args:
                walk(arg)
    walk(s)
    return result

def is_definite_clause(s):
    """returns True for exprs s of the form A & B & ... & C ==> D,
    where all literals are positive.  In clause form, this is
    ~A | ~B | ... | ~C | D, where exactly one clause is positive.
    >>> is_definite_clause(expr('Farmer(Mac)'))
    True
    >>> is_definite_clause(expr('~Farmer(Mac)'))
    False
    >>> is_definite_clause(expr('(Farmer(f) & Rabbit(r)) ==> Hates(f, r)'))
    True
    >>> is_definite_clause(expr('(Farmer(f) & ~Rabbit(r)) ==> Hates(f, r)'))
    False
    >>> is_definite_clause(expr('(Farmer(f) | Rabbit(r)) ==> Hates(f, r)'))
    False
    """
    if is_symbol(s.op):
        return True
    elif s.op == '>>':
        antecedent, consequent = s.args
        return (is_symbol(consequent.op)
                and every(lambda arg: is_symbol(arg.op), conjuncts(antecedent)))
    else:
        return False

def parse_definite_clause(s):
    "Return the antecedents and the consequent of a definite clause."
    assert is_definite_clause(s)
    if is_symbol(s.op):
        return [], s
    else:
        antecedent, consequent = s.args
        return conjuncts(antecedent), consequent

## Useful constant Exprs used in examples and code:
class SpecialExpr(Expr):
    """Exists solely to allow the normal Expr constructor to assert valid symbol
    syntax while still having some way to create the constants 
    TRUE, FALSE, ZERO, ONE, and, TWO
    """
    def __init__(self, op, *args):
        "Op is a string or number; args are Exprs (or are coerced to Exprs)."
        assert isinstance(op, str) or (isnumber(op) and not args)
        self.op = num_or_str(op)
        self.args = list(map(expr, args)) ## Coerce args to Exprs

TRUE, FALSE = list(map(SpecialExpr, ['TRUE', 'FALSE']))
ZERO, ONE, TWO = list(map(SpecialExpr, [0, 1, 2]))
A, B, C, D, E, F, G, P, Q  = list(map(Expr, 'ABCDEFGPQ'))

#______________________________________________________________________________

def tt_entails(kb, alpha):
    """Does kb entail the sentence alpha? Use truth tables. For propositional
    kb's and sentences. [Fig. 7.10]
    >>> tt_entails(expr('P & Q'), expr('Q'))
    True
    """
    assert not variables(alpha)
    return tt_check_all(kb, alpha, prop_symbols(kb & alpha), {})

def tt_check_all(kb, alpha, symbols, model):
    "Auxiliary routine to implement tt_entails."
    if not symbols:
        if pl_true(kb, model):
            result = pl_true(alpha, model)
            assert result in (True, False)
            return result
        else:
            return True
    else:
        P, rest = symbols[0], symbols[1:]
        return (tt_check_all(kb, alpha, rest, extend(model, P, True)) and
                tt_check_all(kb, alpha, rest, extend(model, P, False)))

def prop_symbols(x):
    "Return a list of all propositional symbols in x."
    if not isinstance(x, Expr):
        return []
    elif is_prop_symbol(x.op):
        return [x]
    else:
        return list(symbol for arg in x.args
                        for symbol in prop_symbols(arg))

def tt_true(alpha):
    """Is the propositional sentence alpha a tautology? (alpha will be
    coerced to an expr.)
    >>> tt_true(expr("(P >> Q) <=> (~P | Q)"))
    True
    """
    return tt_entails(TRUE, expr(alpha))

def pl_true(exp, model={}):
    """Return True if the propositional logic expression is true in the model,
    and False if it is false. If the model does not specify the value for
    every proposition, this may return None to indicate 'not obvious';
    this may happen even when the expression is tautological."""
    op, args = exp.op, exp.args
    if exp == TRUE:
        return True
    elif exp == FALSE:
        return False
    elif is_prop_symbol(op):
        return model.get(exp)
    elif op == '~':
        p = pl_true(args[0], model)
        if p is None: return None
        else: return not p
    elif op == '|':
        result = False
        for arg in args:
            p = pl_true(arg, model)
            if p is True: return True
            if p is None: result = None
        return result
    elif op == '&':
        result = True
        for arg in args:
            p = pl_true(arg, model)
            if p is False: return False
            if p is None: result = None
        return result
    p, q = args
    if op == '>>':
        return pl_true(~p | q, model)
    elif op == '<<':
        return pl_true(p | ~q, model)
    pt = pl_true(p, model)
    if pt is None: return None
    qt = pl_true(q, model)
    if qt is None: return None
    if op == '<=>':
        return pt == qt
    elif op == '^':
        return pt != qt
    else:
        raise ValueError ("illegal operator in logic expression" + str(exp))

#______________________________________________________________________________

## Convert to Conjunctive Normal Form (CNF)

def to_cnf(s):
    """Convert a propositional logical sentence s to conjunctive normal form.
    That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253]
    >>> to_cnf("~(B|C)")
    (~B & ~C)
    >>> to_cnf("B <=> (P1|P2)")
    ((~P1 | B) & (~P2 | B) & (P1 | P2 | ~B))
    >>> to_cnf("a | (b & c) | d")
    ((b | a | d) & (c | a | d))
    >>> to_cnf("A & (B | (D & E))")
    (A & (D | B) & (E | B))
    >>> to_cnf("A | (B | (C | (D & E)))")
    ((D | A | B | C) & (E | A | B | C))
    """
    if isinstance(s, str): s = expr(s)
    s = eliminate_implications(s) # Steps 1, 2 from p. 253
    s = move_not_inwards(s) # Step 3
    return distribute_and_over_or(s) # Step 4

def eliminate_implications(s):
    """Change >>, <<, and <=> into &, |, and ~. That is, return an Expr
    that is equivalent to s, but has only &, |, and ~ as logical operators.
    >>> eliminate_implications(A >> (~B << C))
    ((~B | ~C) | ~A)
    >>> eliminate_implications(A ^ B)
    ((A & ~B) | (~A & B))
    """
    if not s.args or is_symbol(s.op): return s     ## (Atoms are unchanged.)
    args = list(map(eliminate_implications, s.args))
    a, b = args[0], args[-1]
    if s.op == '>>':
        return (b | ~a)
    elif s.op == '<<':
        return (a | ~b)
    elif s.op == '<=>':
        return (a | ~b) & (b | ~a)
    elif s.op == '^':
        assert len(args) == 2   ## TODO: relax this restriction
        return (a & ~b) | (~a & b)
    else:
        assert s.op in ('&', '|', '~')
        return Expr(s.op, *args)

def move_not_inwards(s):
    """Rewrite sentence s by moving negation sign inward.
    >>> move_not_inwards(~(A | B))
    (~A & ~B)
    >>> move_not_inwards(~(A & B))
    (~A | ~B)
    >>> move_not_inwards(~(~(A | ~B) | ~~C))
    ((A | ~B) & ~C)
    """
    if s.op == '~':
        NOT = lambda b: move_not_inwards(~b)
        a = s.args[0]
        if a.op == '~': return move_not_inwards(a.args[0]) # ~~A ==> A
        if a.op =='&': return associate('|', list(map(NOT, a.args)))
        if a.op =='|': return associate('&', list(map(NOT, a.args)))
        return s
    elif is_symbol(s.op) or not s.args:
        return s
    else:
        return Expr(s.op, *list(map(move_not_inwards, s.args)))

def distribute_and_over_or(s):
    """Given a sentence s consisting of conjunctions and disjunctions
    of literals, return an equivalent sentence in CNF.
    >>> distribute_and_over_or((A & B) | C)
    ((A | C) & (B | C))
    """
    if s.op == '|':
        s = associate('|', s.args)
        if s.op != '|':
            return distribute_and_over_or(s)
        if len(s.args) == 0:
            return FALSE
        if len(s.args) == 1:
            return distribute_and_over_or(s.args[0])
        conj = find_if((lambda d: d.op == '&'), s.args)
        if not conj:
            return s
        others = [a for a in s.args if a is not conj]
        rest = associate('|', others)
        return associate('&', [distribute_and_over_or(c|rest)
                               for c in conj.args])
    elif s.op == '&':
        return associate('&', list(map(distribute_and_over_or, s.args)))
    else:
        return s

def associate(op, args):
    """Given an associative op, return an expression with the same
    meaning as Expr(op, *args), but flattened -- that is, with nested
    instances of the same op promoted to the top level.
    >>> associate('&', [(A&B),(B|C),(B&C)])
    (A & B & (B | C) & B & C)
    >>> associate('|', [A|(B|(C|(A&B)))])
    (A | B | C | (A & B))
    """
    args = dissociate(op, args)
    if len(args) == 0:
        return _op_identity[op]
    elif len(args) == 1:
        return args[0]
    else:
        return Expr(op, *args)

_op_identity = {'&':TRUE, '|':FALSE, '+':ZERO, '*':ONE}

def conjoin(exprs, *args):
    """Given a list of expressions, returns their conjunction. Can be called either
    with one argument that is a list of expressions, or with several arguments that
    are each an expression.
    >>> conjoin([(A&B),(B|C),(B&C)])
    (A & B & (B | C) & B & C)
    >>> conjoin((A&B), (B|C), (B&C))
    (A & B & (B | C) & B & C)
    """
    if args:
        return conjoin([exprs] + list(args))
    return associate('&', exprs)

def disjoin(exprs, *args):
    """Given a list of expressions, returns their disjunction. Can be called either
    with one argument that is a list of expressions, or with several arguments that
    are each an expression.
    >>> disjoin([C, (A&B), (D&E)])
    (C | (A & B) | (D & E))
    >>> disjoin(C, (A&B), (D&E))
    (C | (A & B) | (D & E))
    """
    if args:
        return disjoin([exprs] + list(args))
    return associate('|', exprs)

def dissociate(op, args):
    """Given an associative op, return a flattened list result such
    that Expr(op, *result) means the same as Expr(op, *args)."""
    result = []
    def collect(subargs):
        for arg in subargs:
            if arg.op == op: collect(arg.args)
            else: result.append(arg)
    collect(args)
    return result

def conjuncts(s):
    """Return a list of the conjuncts in the sentence s.
    >>> conjuncts(A & B)
    [A, B]
    >>> conjuncts(A | B)
    [(A | B)]
    """
    return dissociate('&', [s])

def disjuncts(s):
    """Return a list of the disjuncts in the sentence s.
    >>> disjuncts(A | B)
    [A, B]
    >>> disjuncts(A & B)
    [(A & B)]
    """
    return dissociate('|', [s])

def is_valid_cnf(exp):
    if not isinstance(exp, Expr):
        print ("Input is not an expression.")
        return False
    
    clauses = conjuncts(exp);
    
    for c in clauses:
        literals = disjuncts(c)
        
        for lit in literals:
            if len(lit.args) == 0:
                symbol = lit;
            elif len(lit.args) == 1:
                symbol = lit.args[0]
                
                if len(symbol.args) != 0:
                    print ("Found a NOT outside of %s" % symbol)
                    return False
                
            else:
                print ("Found %s where only a literal should be." % lit)
                return False
    
            symbol_str = str(symbol)
    
            if not is_symbol(symbol_str):
                print ("%s is not a valid symbol." % symbol_str)
                return False
            elif not symbol_str[0].isupper():
                print ("The symbol %s must begin with an upper-case letter." % symbol_str)
                return False
            elif symbol_str == 'TRUE':
                print ("TRUE is not a valid symbol.")
                return False
            elif symbol_str == 'FALSE':
                print ("FALSE is not a valid symbol.")
                return False
        
    return True

#______________________________________________________________________________
# pycosat python wrapper around PicoSAT software.
# https://pypi.python.org/pypi/pycosat

def pycoSAT(expr):
    """Check satisfiability of an expression.
    Given a CNF expression, returns a model that causes the input expression
    to be true. Returns false if it cannot find a satisfible model.
    A model is simply a dictionary with Expr symbols as keys with corresponding values
    that are booleans: True if that symbol is true in the model and False if it is
    false in the model.
    Calls the pycosat solver: https://pypi.python.org/pypi/pycosat
    >>> ppsubst(pycoSAT(A&~B))
    {A: True, B: False}
    >>> pycoSAT(P&~P)
    False
    """
    assert is_valid_cnf(expr), "{} is not in CNF.".format(expr)

    clauses = conjuncts(expr)

    # Load symbol dictionary
    symbol_dict = mapSymbolAndIndices(clauses)
    # Convert Expr to integers
    clauses_int = exprClausesToIndexClauses(clauses, symbol_dict)
    
    model_int = pycosat.solve(clauses_int)
    
    if model_int == 'UNSAT' or model_int == 'UNKNOWN':
        return False
    
    model = indexModelToExprModel(model_int, symbol_dict)
    
    return model

def mapSymbolAndIndices(clauses):
    """
    Create a dictionary that maps each clause to an integer index.
    Uses a bidirectional dictionary {key1:value1, value1:key1, ...} for quick
    access from symbol to index and index to symbol.
    """
    symbol_dict = {}
    idx = 1
    for clause in clauses:
        symbols = prop_symbols(clause)
        for symbol in symbols:
            if symbol not in symbol_dict:
                symbol_dict[symbol] = idx
                symbol_dict[idx] = symbol
                idx +=1

    return symbol_dict

def exprClausesToIndexClauses(clauses, symbol_dict):
    """
    Convert each Expr in a list of clauses (CNF) into its corresponding index in
    the symbol_dict (see mapSymbolAndIndices) 
    """
    clauses_int = []
    for c in clauses:
        c_disj = disjuncts(c)
            
        c_int = []
        for lit in c_disj:
            # If literal is symbol, convert to index and add it.
            # Otherwise it is ~symbol, in which case, we extract the symbol, 
            # convert it to index, and add the negative of the index
            if len(lit.args) == 0:
                c_int += [symbol_dict[lit]]
            else:
                c_int += [-symbol_dict[lit.args[0]]]
        clauses_int += [c_int]

    return clauses_int

def indexModelToExprModel(model_int, symbol_dict):
    """
    Convert a model with indices into a model with the corresponding Expr in
    the symbol_dict (see mapSymbolAndIndices)
    >>>
    """
    model = {}
    for lit_int in model_int:
        if lit_int > 0:
            model[symbol_dict[lit_int]] = True
        else:
            model[symbol_dict[-lit_int]] = False
            
    return model