9. DPLL Algoritms practice

Practica de algoritmo DPLL.

Para la actividad de programación generamos la clase DPLL. Hemos agregado el cascarón del método que deberás implementar. El método se denomina 'satisfiable' y recibe como entrada una fórmula en FNC. Hemos agregado la primera verificación que hace el algoritmo para que veas como debes entregar la respuesta. Se espera que el método regrese una tupla con dos elementos. El primer elemento de la tupla de respuesta es un valor booleano: verdadero si la fórmula es satisfactible, falso si no lo es. El segundo elemento de la tupla es una asignación en caso de que la fórmula sea satisfactible. En caso de que la fórmula no sea satisfactible deberás regresar None en el segundo elemento de la tupla, es decir la tupla deberá ser (False,None).

class DPLL:
    """
    DPLL algorithm
    """
    
    @staticmethod
    def satisfiable(phi):
        """
        determines if phi is satisfiable
        :param phi: a CNF formula
        :returs: una tupla cuyo primer elemento indica
        si la fórmula es satisfactible o no, y el segundo
        la asignación que logró hacer la fórmula verdadera
        """
        log.info("phi: "+str(phi))
        if phi.empty_sentence():
            log.info("sentencia vacia")
            return (True, phi.assignment)
        
        # Verificar si hay una cláusula vacía (contradicción)
        if phi.has_empty_clause():
            log.info("clausula vacia encontrada")
            return (False, None)
        
        # Propagación de literales unitarios
        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}")
            # Asignar el valor que hace verdadero al literal puro
            value = True
            new_phi = phi.assign(pure_literal, value)
            return DPLL.satisfiable(new_phi)
        
        # Elegir un literal para ramificación
        literal = phi.choose_literal()
        log.info(f"ramificando en literal: {literal}")
        
        # Intentar con el literal como verdadero
        new_phi_true = phi.assign(literal, True)
        result = DPLL.satisfiable(new_phi_true)
        if result[0]:
            return result
        
        # Si falló, intentar con el literal como falso
        new_phi_false = phi.assign(literal, False)
        return DPLL.satisfiable(new_phi_false)

relatedInteligencia Artificial