Faça um algoritmo (pseudo-código) que receba uma sentença da lógica proposicional e verifique se ela é satisfatível, tautologia ou contradição.
Obs.: Caso prefira, no lugar do algoritmo, faça um programa em C ou em Python.

Passo 1

O que o problema pede e quais informações eu vou assumir
  • O enunciado pede um algoritmo que receba uma sentença da lógica proposicional e verifique se ela é:
    • satisfatível (existe pelo menos uma atribuição de verdade que torna a sentença verdadeira),
    • tautologia (a sentença é verdadeira para todas as atribuições possíveis),
    • contradição (a sentença é falsa para todas as atribuições possíveis).
  • Vou assumir uma sintaxe prática para a entrada (preciso definir isto para implementar):
    • variáveis proposicionais são identificadores formados por letras/ dígitos/underscore, ex.: p, q1, is_r.
    • operadores escritos com os símbolos:
      • negação: ~ ou !
      • conjunção: &
      • disjunção: |
      • implicação: ->
      • bi-implicação (equivalência): <->
    • parênteses ( ) para controle de precedência.
  • O algoritmo deve aceitar uma string contendo a fórmula e devolver qual das três categorias ela pertence (e opcionalmente uma atribuição que a satisfaz, quando houver).
  • Observações importantes que vêm do enunciado (mas não me perguntou nada adicional): o algoritmo deve ser correto (exhaustivo) e didático para aplicar na prova.

Passo 2

Definições formais (muito úteis para entender o que vamos testar)
  • Satisfatibilidade:
    • Uma fórmula é satisfatível se existir uma atribuição de valores verdadeiros/falsos às suas variáveis que torne a fórmula verdadeira.
    • Em termos de contagem de avaliações: existe pelo menos uma atribuição que dá valor verdadeiro.
  • Tautologia:
    • Uma fórmula é tautologia se for verdadeira para todas as atribuições possíveis. Em outras palavras, se o número de atribuições que a tornam verdadeira for exatamente 2^n, onde n é o número de variáveis distintas da fórmula.
  • Contradição:
    • Uma fórmula é contradição se for falsa para todas as atribuições possíveis (ou seja, verdadeiro em 0 atribuições).
  • Relação entre elas:
    • Tautologia implica satisfatível (mas uma satisfatível nem sempre é tautologia).
    • Contradição é o caso oposto: não satisfatível.

Passo 3

Escolha do método de resolução (por que usar tabela-verdade / enumeração)
  • Existem vários métodos (redução a CNF + SAT solver, tableaux, resolução, álgebra booleana, etc.). Para uma prova e para entender passo a passo, a enumeração por todas as atribuições (tabela-verdade) é a abordagem mais básica e didática.
  • Complexidade: se a fórmula tem n variáveis distintas, a enumeração testa 2^n atribuições. Isso cresce rápido, então na prática não é boa para muitas variáveis, mas para exercícios de prova (ou para ensinar) é perfeita.
  • Vou implementar:
    1. Parse da fórmula em uma árvore sintática (AST).
    2. Extrair a lista de variáveis distintas.
    3. Gerar todas as 2^n atribuições de verdade.
    4. Avaliar a AST em cada atribuição e contar quantas vezes a fórmula dá verdadeiro.
    5. Concluir: se contador =0 => contradição; se contador =2^n => tautologia; caso contrário => satisfatível (e não tautologia).

Passo 4

Como transformar a fórmula textual em estrutura que dá pra avaliar (anatomia do parser)
  • Precisamos transformar a string em tokens e depois num AST. O AST terá nós do tipo:
    • Var(name) — variável proposicional
    • Not(child) — negação \lnot
    • And(left,right) — conjunção \land
    • Or(left,right) — disjunção \lor
    • Imp(left,right) — implicação \rightarrow
    • Iff(left,right) — equivalência \leftrightarrow
  • Gramática (informal) e precedência usada (de maior para menor):
    1. Not (unário, direita)
    2. And
    3. Or
    4. Imp (implicação, associatividade direita)
    5. Iff (bi-implicação, associatividade direita)
  • A técnica: usar um parser descendente recursivo com funções:
    • parse_iff -> parse_imp -> parse_or -> parse_and -> parse_not -> parse_atom
  • parse_atom trata variáveis e subfórmulas parentetizadas.

Passo 5

Como avaliar a AST para uma atribuição de variáveis (sem pular etapas)
  • Dado um nó da AST e um dicionário assign que associa cada variável a True/False, a avaliação recursiva segue:
    • Var(name): retorna assign[name].
    • Not(child): retorna \lnot v, onde v é a avaliação de child. Em código: not v.
    • And(l,r): retorna v_l \land v_r. Em código: v_l and v_r.
    • Or(l,r): retorna v_l \lor v_r. Em código: v_l or v_r.
    • Imp(l,r): l \rightarrow r é logicamente equivalente a \lnot l \lor r. Em código: (not v_l) or v_r.
    • Iff(l,r): l \leftrightarrow r é verdadeiro se v_l e v_r têm o mesmo valor. Em código: v_l == v_r.
  • Exemplo pequeno para fixar: se a fórmula for p -> q, e p=True, q=False, então:
    • p avalia True, q avalia False.
    • p -> q avalia (not True) or False = False or False = False.
  • Esta função de avaliação é a parte que será chamada para cada atribuição das 2^n possíveis.

Passo 6

Como gerar todas as atribuições de forma prática (sem usar muita memória)
  • Seja a lista de n variáveis: [v_0,v_1,\dots,v_{n-1}].
  • Para i variando de 0 a 2^n-1:
    • interpretar i em binário: o bit j (por exemplo (i >> j) & 1) informa se v_j é True (1) ou False (0).
    • construir o dicionário assign mapeando cada v_j para o booleano correspondente.
  • Assim evitamos criar uma lista enorme de atribuições na memória: gera-se uma por vez e avalia imediatamente.
  • Observação: 2^n pode ficar grande rapidamente — na prática, usar essa abordagem para n até, por exemplo, 20 é razoável em PC comum; acima disso, usar um SAT-solver seria recomendado.

Passo 7

Critérios de saída e resultados auxiliares que o algoritmo pode devolver
  • O algoritmo principal fará:
    • contar true_count = número de atribuições que avaliam a fórmula como verdadeira.
    • se true_count == 0: contradição.
    • se true_count == 2^n: tautologia.
    • senão: satisfatível (não tautologia).
  • Além disso é muito útil devolver:
    • uma atribuição que satisfaça a fórmula (quando true_count > 0), para que o estudante possa ver um exemplo concreto.
    • o número de variáveis n e 2^n para justificar o custo.

Passo 8

Implementação concreta em Python (explicada passo a passo antes de mostrar o código)
  • O código abaixo segue as ideias que descrevi:
    1. tokenize(s) — quebra a string em tokens (parênteses, operadores multi-caractere como -> e <->, nomes de variáveis).
    2. parser descentente com funções parse_iff, parse_imp, parse_or, parse_and, parse_not, parse_atom.
    3. AST representado por tuplas: ('var', name), ('not', child), ('and', l, r), etc.
    4. eval_ast(node, assign) — avalia recursivamente usando as regras lógicas.
    5. get_vars(node) — retorna o conjunto de variáveis na AST.
    6. check_formula(s) — função principal que recebe a string s, faz parse, gera todas as atribuições e classifica a fórmula. Retorna a classificação e, se aplicável, uma atribuição satisfatória.
  • Observação de estilo: o código é didático e evita otimizações complexas para que seja fácil de entender na prova.

Passo 9

Exemplo de uso (explicação rápida sem executar aqui)
  • Se chamar check_formula("p -> (q & p)"):
    • o parser reconhece p, ->, (, q, &, p, ).
    • as variáveis são {p,q} com n=2, logo 2^n=4 atribuições a testar.
    • o algoritmo testa as 4 atribuições, conta quantas tornam a fórmula verdadeira e conclui a classificação.
  • Se chamar check_formula("p | ~p") (lei do terceiro excluído), o algoritmo deve retornar tautologia.
  • Se chamar check_formula("p & ~p"), deve retornar contradição.
  • Se chamar check_formula("(p -> q) & p & ~q"), deve retornar contradição (contradição explícita).

Resposta

# Verificador simples de satisfatibilidade / tautologia / contradição
# Sintaxe aceita:
#  - variáveis: letras, dígitos e underscore, ex: p, q1, is_r
#  - negação: ~ ou !
#  - e: &
#  - ou: |
#  - implicação: ->
#  - equivalência: <->
#  - parênteses: ( )
#
# Saída de check_formula(formula_str):
#  - retorna ("tautology", None) se for tautologia
#  - retorna ("contradiction", None) se for contradição
#  - retorna ("satisfiable", example_assign) se satisfatível (example_assign é dict var->bool)

import re

# -------------------------
# Tokenizer
# -------------------------
_token_spec = [
    ("SKIP",    r"[ \t\n]+"),
    ("IFF",     r"<->"),
    ("IMP",     r"->"),
    ("AND",     r"&"),
    ("OR",      r"\|"),
    ("NOT",     r"[~!]"),
    ("LPAR",    r"\("),
    ("RPAR",    r"\)"),
    ("VAR",     r"[A-Za-z][A-Za-z0-9_]*"),
    ("MISMATCH",r"."),
]

_token_re = re.compile("|".join("(?P<%s>%s)" % pair for pair in _token_spec))

def tokenize(s):
    tokens = []
    for m in _token_re.finditer(s):
        kind = m.lastgroup
        val = m.group()
        if kind == "SKIP":
            continue
        if kind == "MISMATCH":
            raise SyntaxError(f"Caracter inválido na expressão: {val}")
        tokens.append((kind, val))
    tokens.append(("EOF",""))
    return tokens

# -------------------------
# Parser (recursive descent)
# -------------------------
class Parser:
    def __init__(self, tokens):
        self.tokens = tokens
        self.pos = 0

    def peek(self):
        return self.tokens[self.pos][0]

    def next(self):
        cur = self.tokens[self.pos]
        self.pos += 1
        return cur

    # Grammar (com precedências):
    # parse_iff -> parse_imp ( "<->" parse_imp )*
    # parse_imp -> parse_or ( "->" parse_imp )?    (implicação direita-associativa)
    # parse_or  -> parse_and ( "|" parse_and )*
    # parse_and -> parse_not ( "&" parse_not )*
    # parse_not -> ("~" | "!") parse_not | parse_atom
    # parse_atom -> VAR | "(" parse_iff ")"

    def parse(self):
        node = self.parse_iff()
        if self.peek() != "EOF":
            raise SyntaxError("Token extra após fim da expressão")
        return node

    def parse_iff(self):
        node = self.parse_imp()
        while self.peek() == "IFF":
            self.next()
            right = self.parse_imp()
            node = ("iff", node, right)
        return node

    def parse_imp(self):
        left = self.parse_or()
        if self.peek() == "IMP":
            self.next()
            # implicação é direita-associativa: a -> b -> c = a -> (b -> c)
            right = self.parse_imp()
            return ("imp", left, right)
        return left

    def parse_or(self):
        node = self.parse_and()
        while self.peek() == "OR":
            self.next()
            right = self.parse_and()
            node = ("or", node, right)
        return node

    def parse_and(self):
        node = self.parse_not()
        while self.peek() == "AND":
            self.next()
            right = self.parse_not()
            node = ("and", node, right)
        return node

    def parse_not(self):
        if self.peek() == "NOT":
            self.next()
            child = self.parse_not()
            return ("not", child)
        else:
            return self.parse_atom()

    def parse_atom(self):
        if self.peek() == "VAR":
            _, val = self.next()
            return ("var", val)
        if self.peek() == "LPAR":
            self.next()
            node = self.parse_iff()
            if self.peek() != "RPAR":
                raise SyntaxError("Parêntese fechado esperado")
            self.next()
            return node
        raise SyntaxError("Átomo esperado (variável ou parêntese)")

# -------------------------
# AST evaluation and helpers
# -------------------------
def get_vars(node):
    t = node[0]
    if t == "var":
        return {node[1]}
    if t == "not":
        return get_vars(node[1])
    # binary
    return get_vars(node[1]) | get_vars(node[2])

def eval_ast(node, assign):
    t = node[0]
    if t == "var":
        name = node[1]
        if name not in assign:
            raise KeyError(f"Variável {name} sem atribuição")
        return assign[name]
    if t == "not":
        return not eval_ast(node[1], assign)
    if t == "and":
        return eval_ast(node[1], assign) and eval_ast(node[2], assign)
    if t == "or":
        return eval_ast(node[1], assign) or eval_ast(node[2], assign)
    if t == "imp":
        l = eval_ast(node[1], assign)
        r = eval_ast(node[2], assign)
        return (not l) or r
    if t == "iff":
        l = eval_ast(node[1], assign)
        r = eval_ast(node[2], assign)
        return l == r
    raise ValueError("Tipo de nó AST desconhecido: " + t)

# -------------------------
# Função principal
# -------------------------
def check_formula(s):
    """
    Recebe string s com a fórmula. Retorna tupla:
      ("tautology", None) ou ("contradiction", None) ou ("satisfiable", example_assign)
    example_assign é um dict {var: bool} quando satisfatível.
    """
    tokens = tokenize(s)
    parser = Parser(tokens)
    ast = parser.parse()

    vars_set = sorted(list(get_vars(ast)))
    n = len(vars_set)
    total = 1 << n  # 2^n

    true_count = 0
    example = None

    for i in range(total):
        # construir atribuição a partir de bits de i
        assign = {}
        for j, var in enumerate(vars_set):
            assign[var] = bool((i >> j) & 1)
        val = eval_ast(ast, assign)
        if val:
            true_count += 1
            if example is None:
                example = assign.copy()

    if true_count == 0:
        return ("contradiction", None)
    if true_count == total:
        return ("tautology", None)
    return ("satisfiable", example)

# -------------------------
# Exemplo rápido (comentado)
# -------------------------
# print(check_formula("p | ~p"))        # tautology
# print(check_formula("p & ~p"))       # contradiction
# print(check_formula("(p -> q) & p")) # satisfiable, exemplo: {'p': True, 'q': True} possivelmente

Exercícios relacionados