Lógica computacional · SAT

Aprende o algoritmo de Davis‑Putnam, passo a passo

Escreve um conjunto de cláusulas e vê cada propagação, cada escolha e cada conflito até à resposta.

Experimenta um exemplo: {p, ¬p ∨ q, ¬q} Dois ramos 3 pombos, 2 poleiros

O que podes fazer

Resolver

Resposta e valoração

Passo a passo

O DLL evento a evento, com a árvore

Aprender

Lição curta, interativos e quiz

O que é o DPLL?

O DPLL (Davis–Putnam–Logemann–Loveland), a que aqui chamamos DLL, é o algoritmo clássico da lógica computacional para decidir a satisfazibilidade (SAT) de um conjunto de cláusulas: junta a propagação unitária à ramificação, e continua a ser a base dos SAT solvers modernos.