from typing import List, Set, Dict, Tuple, Optional
from dataclasses import dataclass
from abc import ABC, abstractmethod
print('Libraries imported')class Expr(ABC):
@abstractmethod
def evaluate(self, model: Dict[str, bool]) -> bool:
pass
@abstractmethod
def get_symbols(self) -> Set[str]:
pass
class Symbol(Expr):
def __init__(self, name: str):
self.name = name
def evaluate(self, model):
return model.get(self.name, False)
def get_symbols(self):
return {self.name}
def __str__(self):
return self.name
class Not(Expr):
def __init__(self, operand):
self.operand = operand
def evaluate(self, model):
return not self.operand.evaluate(model)
def get_symbols(self):
return self.operand.get_symbols()
def __str__(self):
return f'~{self.operand}'
class And(Expr):
def __init__(self, *operands):
self.operands = list(operands)
def evaluate(self, model):
return all(op.evaluate(model) for op in self.operands)
def get_symbols(self):
return set().union(*(op.get_symbols() for op in self.operands))
def __str__(self):
return '(' + ' & '.join(str(op) for op in self.operands) + ')'
class Or(Expr):
def __init__(self, *operands):
self.operands = list(operands)
def evaluate(self, model):
return any(op.evaluate(model) for op in self.operands)
def get_symbols(self):
return set().union(*(op.get_symbols() for op in self.operands))
def __str__(self):
return '(' + ' | '.join(str(op) for op in self.operands) + ')'
class Implies(Expr):
def __init__(self, ant, cons):
self.antecedent = ant
self.consequent = cons
def evaluate(self, model):
return not self.antecedent.evaluate(model) or self.consequent.evaluate(model)
def get_symbols(self):
return self.antecedent.get_symbols() | self.consequent.get_symbols()
def __str__(self):
return f'({self.antecedent} -> {self.consequent})'
print('Expression classes defined')def truth_table(expr, show=True):
symbols = sorted(expr.get_symbols())
n = len(symbols)
if show:
print(' | '.join(symbols) + ' | ' + str(expr))
print('-' * 50)
for i in range(2**n):
model = {}
row = []
for j, sym in enumerate(symbols):
val = bool((i >> (n-j-1)) & 1)
model[sym] = val
row.append('T' if val else 'F')
result = expr.evaluate(model)
row.append('T' if result else 'F')
if show:
print(' | '.join(row))
print('Truth table function defined')print('=== Example: Implication ===')
P = Symbol('P')
Q = Symbol('Q')
impl = Implies(P, Q)
truth_table(impl)class KnowledgeBase:
def __init__(self):
self.facts = set()
self.rules = []
def tell_fact(self, fact):
self.facts.add(fact)
def tell_rule(self, premises, conclusion):
self.rules.append((premises, conclusion))
def forward_chain(self, query, verbose=True):
inferred = set(self.facts)
agenda = list(self.facts)
while agenda:
fact = agenda.pop(0)
if fact == query:
if verbose: print(f'Proved: {query}')
return True
for premises, conclusion in self.rules:
if conclusion not in inferred and all(p in inferred for p in premises):
inferred.add(conclusion)
agenda.append(conclusion)
if verbose: print(f'Inferred: {conclusion}')
return False
print('KnowledgeBase implemented')print('=== Example: Animal Classification ===')
kb = KnowledgeBase()
kb.tell_fact('hasFur')
kb.tell_fact('produceMilk')
kb.tell_rule(['hasFur', 'produceMilk'], 'mammal')
kb.tell_rule(['mammal', 'eatsMeat'], 'carnivore')
print('Query: mammal')
kb.forward_chain('mammal')Next Steps¶
This notebook covers expressions, truth tables and forward chaining. The lab notebook (Chapter 4 Lab: Propositional Logic) asks you to implement CNF conversion, resolution, backward chaining, DPLL and a Wumpus World agent.
Extension: Sudoku as SAT. Once DPLL works, a Sudoku puzzle can be encoded with one Boolean symbol per cell and value (729 symbols). The clauses say that every cell has at least one value, no cell has two values, and no value repeats in a row, column or 3×3 box; the given digits are unit clauses. A model returned by the solver is a solution.