← inteligencia-artificial
10. Examen de Implementación de algoritmo DPLL
import logging
# Configuración del logger
logging.basicConfig(level=logging.INFO)
log = logging.getLogger(__name__)
class DPLL:
"""
DPLL algorithm
"""
@staticmethod
def satisfiable(phi):
"""
Determines if phi is satisfiable
:param phi: a CNF formula
:returns: (True/False, assignment)
"""
log.info("phi: " + str(phi))
# Caso base: fórmula vacía (satisfactible)
if phi.empty_sentence():
log.info("sentencia vacía")
return (True, phi.assignment)
# Caso base: cláusula vacía (contradicción)
if phi.has_empty_clause():
log.info("cláusula vacía encontrada")
return (False, None)
# Propagación de cláusulas unitarias
unit_literal = phi.find_unit_clause()
if unit_literal is not None:
log.info(f"literal unitario encontrado: {unit_literal}")
new_phi = phi.assign(unit_literal, True)
return DPLL.satisfiable(new_phi)
# Eliminación de literales puros
pure_literal = phi.find_pure_literal()
if pure_literal is not None:
log.info(f"literal puro encontrado: {pure_literal}")
new_phi = phi.assign(pure_literal, True)
return DPLL.satisfiable(new_phi)
# Ramificación
literal = phi.choose_literal()
log.info(f"ramificando en literal: {literal}")
# Intentar literal = True
new_phi_true = phi.assign(literal, True)
result = DPLL.satisfiable(new_phi_true)
if result[0]:
return result
# Intentar literal = False
new_phi_false = phi.assign(literal, False)
return DPLL.satisfiable(new_phi_false)
# ===================== EJECUCIÓN =====================
phi_1 = FormulaCNF(
"(~x1 | x3 | x4) & (~x2 | x6 | x4) & (~x2 | ~x6 | ~x3) & "
"(~x4 | ~x2) & (x2 | ~x3 | ~x1) & (x2 | x6 | x3) & "
"(x2 | ~x6 | ~x4) & (x1 | x5) & (x1 | x6) & "
"(~x6 | x3 | ~x5) & (x1 | ~x3 | ~x5)"
)
resultado = DPLL.satisfiable(phi_1)
print("\nRESULTADO:")
print(resultado)
relatedInteligencia Artificial