Function libprop_sat_solver::tableaux_solver::is_satisfiable

pub fn is_satisfiable(propositional_formula: &PropositionalFormula) -> bool

Checks if the given propositional formula is satisfiable.

Propositional Tableaux Algorithm

Key Terminology

Term	Meaning
Theory	A set of propositional formulas.
Tableau	A queue of alternative theories.

Core Algorithm

The original algorithm is given by the pseudocode:

begin procedure Satisfiable(phi: PropositionalFormula) -> bool
    // Initialize `phi` as the single element of the single set contained
    // within the theory queue.
    Tableau <- [{ phi }]

    while !IsEmpty(Tab) do
        Theory <- Dequeue(Tableau)

        if FullyExpanded(Theory) && !ContainsContradictions(Theory) then
            return true
        else
            NonLiteral <- PickNonLiteral(Theory)

            ExpansionType <- DetermineExpansionType(NonLiteral)

            match ExpansionType
                case ALPHA => {
                    Theory = Theory[alpha <- {alpha_1, alpha_2}]
                    if !ContainsContradictions(Theory) && !(Theory in Tableau) then
                        Enqueue(Theory)
                    end if
                }
                case BETA => {
                    Theory_1 = Theory[beta <- beta_1]
                    Theory_2 = Theory[beta <- beta_2]

                    if !(Theory_1 in Tableau) && !ContainsContradictions(Theory_1) then
                        Enqueue(Theory_1)
                    end if

                    if !(Theory_2 in Tableau) && !ContainsContradictions(Theory_2) then
                        Enqueue(Theory_2)
                    end if
                }
            end match
        end if
    end while

    assert IsEmpty(Tableau)
    return false
end procedure

Notice that the algorithm performs an optimization for early return by fusing the contradiction checking logic (i.e. determining if a branch closes) with the branch construction logic.