Chapter 4 Lab: Propositional Logic

from typing import Dict, List, Set
import itertools

class PropositionalFormula:
    def __init__(self, expression: str):
        self.expression = expression
        self.variables = self.extract_variables()
        
    def extract_variables(self) -> Set[str]:
        """Extract propositional variables from expression"""
        # YOUR CODE: Extract variables (single capital letters)
        pass
        
    def evaluate(self, assignment: Dict[str, bool]) -> bool:
        """
        TODO: Evaluate formula under given variable assignment
        Support operators: AND (&), OR (|), NOT (~), IMPLIES (=>), IFF (<=>)
        """
        pass

def generate_truth_table(formula: str) -> List[Dict]:
    """
    TODO: Generate complete truth table
    Return list of dicts with variable assignments and result
    """
    pass

def is_tautology(formula: str) -> bool:
    """Check if formula is always true"""
    # YOUR CODE
    pass

def is_satisfiable(formula: str) -> bool:
    """Check if formula can be true"""
    # YOUR CODE
    pass

# Test
formulas = [
    'P | ~P',  # Tautology
    'P & ~P',  # Contradiction
    '(P => Q) <=> (~Q => ~P)',  # Contrapositive (tautology)
    '(P | Q) & ~P => Q'  # Disjunctive syllogism (tautology)
]

for f in formulas:
    table = generate_truth_table(f)
    print(f'Formula: {f}')
    print(f'Tautology: {is_tautology(f)}')
    print(f'Satisfiable: {is_satisfiable(f)}')
    print(table)
    print()

class CNFConverter:
    """Convert formulas to CNF"""
    
    def eliminate_implications(self, formula: str) -> str:
        """
        TODO: Replace => and <=> with AND, OR, NOT
        P => Q becomes ~P | Q
        P <=> Q becomes (P => Q) & (Q => P)
        """
        pass
        
    def move_not_inward(self, formula: str) -> str:
        """
        TODO: Apply De Morgan's laws
        ~(P & Q) becomes ~P | ~Q
        ~(P | Q) becomes ~P & ~Q
        ~~P becomes P
        """
        pass
        
    def distribute_or_over_and(self, formula: str) -> str:
        """
        TODO: Distribute OR over AND
        P | (Q & R) becomes (P | Q) & (P | R)
        """
        pass
        
    def to_cnf(self, formula: str) -> str:
        """Convert to CNF using above steps"""
        f = self.eliminate_implications(formula)
        f = self.move_not_inward(f)
        f = self.distribute_or_over_and(f)
        return f

def parse_cnf(cnf_str: str) -> List[List[str]]:
    """
    TODO: Parse CNF string into list of clauses
    Each clause is a list of literals
    Example: '(A | B) & (~A | C)' -> [['A', 'B'], ['~A', 'C']]
    """
    pass

# Test
converter = CNFConverter()
test_formulas = [
    'P => Q',
    '(P | Q) => R',
    'P <=> Q',
    '~(P & Q) | R'
]

for f in test_formulas:
    cnf = converter.to_cnf(f)
    print(f'{f:25s} -> {cnf}')
    print(f'Clauses: {parse_cnf(cnf)}\n')

class ResolutionProver:
    def __init__(self, kb: List[List[str]]):
        """Knowledge base as list of clauses (CNF)"""
        self.kb = kb
        
    def resolve(self, clause1: List[str], clause2: List[str]) -> List[str]:
        """
        TODO: Apply resolution rule to two clauses
        
        If clause1 contains literal L and clause2 contains ~L:
        Return resolvent (union of clauses minus L and ~L)
        
        Example: [A, B] and [~A, C] -> [B, C]
        """
        pass
        
    def pl_resolution(self, query: str) -> bool:
        """
        TODO: Prove query using resolution
        
        Algorithm:
        1. Convert ~query to CNF and add to KB
        2. Repeatedly resolve pairs of clauses
        3. If empty clause derived, return True (query proved)
        4. If no new clauses, return False (query not provable)
        """
        pass

# Test with Socrates example
kb = [
    ['~Man', 'Mortal'],  # Man(x) => Mortal(x)
    ['Man']              # Man(Socrates)
]

prover = ResolutionProver(kb)
query = 'Mortal'
print(f'Can prove {query}? {prover.pl_resolution(query)}')

# Test with more complex example
kb2 = [
    ['~P', 'Q'],     # P => Q
    ['~Q', 'R'],     # Q => R
    ['P']            # P
]
prover2 = ResolutionProver(kb2)
print(f'Can prove R? {prover2.pl_resolution("R")}')

class HornClauseKB:
    def __init__(self):
        self.facts = set()
        self.rules = []  # List of (premises, conclusion)
        
    def add_fact(self, fact: str):
        self.facts.add(fact)
        
    def add_rule(self, premises: List[str], conclusion: str):
        self.rules.append((premises, conclusion))

def forward_chaining(kb: HornClauseKB, query: str) -> bool:
    """
    TODO: Implement forward chaining
    
    Algorithm:
    1. Start with known facts
    2. Apply rules whose premises are satisfied
    3. Add new facts
    4. Repeat until query derived or no new facts
    """
    pass

def backward_chaining(kb: HornClauseKB, query: str, known: Set[str] = None) -> bool:
    """
    TODO: Implement backward chaining (recursive)
    
    Algorithm:
    1. If query is a known fact, return True
    2. Find rules that conclude query
    3. Recursively prove all premises
    4. If any rule proves query, return True
    """
    pass

# Test with animal classification
kb = HornClauseKB()
# Facts
kb.add_fact('has_feathers')
kb.add_fact('lays_eggs')

# Rules
kb.add_rule(['has_feathers'], 'is_bird')
kb.add_rule(['is_bird', 'lays_eggs'], 'can_fly')
kb.add_rule(['is_bird', 'swims'], 'is_penguin')

queries = ['is_bird', 'can_fly', 'is_penguin']
for q in queries:
    fc = forward_chaining(kb, q)
    bc = backward_chaining(kb, q)
    print(f'{q:15s}: FC={fc}, BC={bc}')

class WumpusWorld:
    def __init__(self, size=4):
        self.size = size
        self.agent_pos = (0, 0)
        self.wumpus_pos = (1, 2)
        self.gold_pos = (2, 3)
        self.pits = {(3, 0), (3, 2), (0, 2)}
        
    def get_percepts(self, pos) -> Dict[str, bool]:
        """Get percepts at position"""
        x, y = pos
        percepts = {
            'stench': False,
            'breeze': False,
            'glitter': False,
            'bump': False,
            'scream': False
        }
        
        # Check adjacent cells
        adjacent = [(x+1,y), (x-1,y), (x,y+1), (x,y-1)]
        
        for adj in adjacent:
            if adj == self.wumpus_pos:
                percepts['stench'] = True
            if adj in self.pits:
                percepts['breeze'] = True
                
        if pos == self.gold_pos:
            percepts['glitter'] = True
            
        return percepts

class WumpusAgent:
    """Logical agent for Wumpus World"""
    
    def __init__(self):
        self.kb = []  # Propositional knowledge base
        self.visited = set()
        self.safe = {(0, 0)}
        self.danger = set()
        
    def add_percept_rules(self, pos, percepts):
        """
        TODO: Add logical rules based on percepts
        
        Rules:
        - If breeze at (x,y), then pit in adjacent cell
        - If stench at (x,y), then wumpus in adjacent cell
        - If no breeze, no pits adjacent
        - If no stench, no wumpus adjacent
        """
        pass
        
    def infer_safe_cells(self) -> Set[tuple]:
        """
        TODO: Use inference to determine safe cells
        Use resolution or model checking
        """
        pass
        
    def choose_action(self, percepts) -> str:
        """
        TODO: Choose action based on KB
        Actions: 'forward', 'turn_left', 'turn_right', 'grab', 'shoot', 'climb'
        """
        pass

# Simulate
world = WumpusWorld()
agent = WumpusAgent()

print('Wumpus World Simulation')
for step in range(20):
    percepts = world.get_percepts(agent.agent_pos)
    agent.add_percept_rules(agent.agent_pos, percepts)
    safe_cells = agent.infer_safe_cells()
    action = agent.choose_action(percepts)
    print(f'Step {step}: Pos={agent.agent_pos}, Percepts={percepts}, Action={action}')
    if action == 'grab' and agent.agent_pos == world.gold_pos:
        print('Gold found!')
        break

def dpll(clauses: List[List[str]], assignment: Dict[str, bool] = None) -> bool:
    """
    CHALLENGE: Implement DPLL SAT solver
    
    Algorithm:
    1. Unit propagation: If clause has one literal, must be true
    2. Pure literal elimination: If literal always appears with same polarity
    3. Choose literal and try both values (backtrack)
    
    Return True if satisfiable, False otherwise
    """
    pass

def unit_propagate(clauses, assignment):
    """Apply unit propagation rule"""
    # YOUR CODE
    pass

def pure_literal_eliminate(clauses, assignment):
    """Eliminate pure literals"""
    # YOUR CODE
    pass

# Test on hard SAT problems
test_cases = [
    [[['A'], ['~A']]],  # UNSAT
    [[['A', 'B'], ['~A', 'C'], ['~B', '~C']]],  # SAT
    [[['A', 'B', 'C'], ['~A', '~B'], ['~B', '~C'], ['~A', '~C']]]  # SAT
]

for i, clauses in enumerate(test_cases):
    result = dpll(clauses[0])
    print(f'Test {i+1}: {"SAT" if result else "UNSAT"}')