module Logic.Propositional.Classical.SAT where

SAT solvingπŸ”—

SAT solving is the process of determining if we can find some assignment of variables ρ\rho that makes a given formula Ο•\phi in classical propositional logic true. Such an assignment is called a satisfying assignment, hence the name SAT. This is a classic problem in the field of computer science, and many other important and interesting problems can be reduced to finding satisfying assignments to huge formulae.

Unfortunately, SAT solving is provably hard, from a complexity standpoint. However, this will not stop us from writing a solver anyways! For the sake of efficiency, our solver will operate on expressions in conjunctive normal form.

Unit propagationπŸ”—

The algorithm we will use is a simplified version of the classic DPLL algorithm, which combines backtracking search with a mechanism for pruning the search space, known as unit propagation.

The idea behind this is the observation unit-clause-sat. Translated into symbolic notation, it says that if our overall formula Ο•\phi breaks down as Ο•0∧Pβˆ§Ο•1\phi_0 \land P \land \phi_1 β€” that is, we have a clause which consists of a single literal, then it’s necessary for βŠ¨Ο•\vDash \phi that ⊨P\vDash P. Not only does this give us one datum of our satisfying assignment, it also lets us get rid of any clauses that mention PP, since they must also be true!

Even better, we can also remove any occurrences of Β¬P\neg P from our clauses β€” since we’ve decided that PP is true, having false\mathrm{false} as a disjunct has no effect on the remaining clauses. This reduces the size of the search space considerably, and makes the problem a bit more tractable.

Luckily, unit propagation is rather easy to implement. The workhorse is the recursive function delete-literal. Pay attention to its type: expressed non-numerically, it says that given the index of Ο•\phi and a formula in Ξ“0,Ο•,Ξ“1\Gamma_0, \phi, \Gamma_1, we’ll return a formula in Ξ“0,Ξ“1.\Gamma_0, \Gamma_1.

delete-literal
  : (x : Fin (suc Ξ“)) (Ο• : Clause (suc Ξ“))
  β†’ Clause Ξ“
delete-literal {Ξ“ = zero}  i Ο•  = []
delete-literal {Ξ“ = suc Ξ“} i [] = []
delete-literal {Ξ“ = suc Ξ“} i (x ∷ Ο•) with i ≑? lit-var x
... | yes _  = delete-literal i Ο•
... | no iβ‰ x = avoid-lit i x iβ‰ x ∷ delete-literal i Ο•

Unit propagation is then applying this function to all the clauses in a CNF expression.

unit-propagate : Literal (suc Ξ“) β†’ CNF (suc Ξ“) β†’ CNF Ξ“
unit-propagate x [] = []
unit-propagate x (Ο• ∷ Ο•s) with elem? x Ο•
... | yes _ = unit-propagate x Ο•s
... | no _  = delete-literal (lit-var x) Ο• ∷ unit-propagate x Ο•s

However, while this procedure is easy to implement, it’s actually slightly tricky to prove correct. We’ll start by showing a couple of quick lemmas regarding assignment of variables.

avoid-lit-insert
  : (x y : Literal (suc Ξ“)) (xβ‰ y : Β¬ (lit-var x ≑ lit-var y)) (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ y ⟧ (ρ [ lit-var x ≔ lit-val x ])
  ≑ ⟦ avoid-lit (lit-var x) y xβ‰ y ⟧ ρ

lit-assign-neg-false
  : (x : Literal (suc Ξ“)) (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ x ⟧ (ρ [ lit-var (Β¬lit x) ≔ lit-val (Β¬lit x) ]) ≑ false

lit-assign-true
  : (x : Literal (suc Ξ“)) (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ x ⟧ (ρ [ lit-var x ≔ lit-val x ]) ≑ true

Next, we show that deleting literals preserves the truth value of a given assignment, as long as the literal doesn’t show up in the clause. This is not hard to show, just tedious.

delete-literal-sound
  : (x : Literal (suc Ξ“)) (Ο• : Clause (suc Ξ“))
  β†’ Β¬ (x βˆˆβ‚— Ο•)
  β†’ (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ Ο• ⟧ (ρ [ lit-var x ≔ lit-val x ]) ≑ ⟦ delete-literal (lit-var x) Ο• ⟧ ρ

delete-literal-sound {zero} x [] xβˆ‰Ο• ρ = refl
delete-literal-sound {zero} (lit fzero) (lit fzero ∷ Ο•) xβˆ‰Ο• ρ =
  absurd (xβˆ‰Ο• (here refl))
delete-literal-sound {zero} (lit fzero) (neg fzero ∷ Ο•) xβˆ‰Ο• ρ =
  delete-literal-sound (lit fzero) Ο• (xβˆ‰Ο• ∘ there) ρ
delete-literal-sound {zero} (neg fzero) (lit fzero ∷ Ο•) xβˆ‰Ο• ρ =
  delete-literal-sound (neg fzero) Ο• (xβˆ‰Ο• ∘ there) ρ
delete-literal-sound {zero} (neg fzero) (neg fzero ∷ Ο•) xβˆ‰Ο• ρ =
  absurd (xβˆ‰Ο• (here refl))

delete-literal-sound {suc Ξ“} x []      xβˆ‰Ο• ρ = refl
delete-literal-sound {suc Ξ“} x (y ∷ Ο•) xβˆ‰Ο• ρ with lit-var x ≑? lit-var y
... | yes x=y =
  apβ‚‚ or
    (subst (Ξ» e β†’ ⟦ y ⟧ (ρ [ lit-var e ≔ lit-val e ]) ≑ false)
      (sym (literal-eq-negate x y (xβˆ‰Ο• ∘ here) x=y))
      (lit-assign-neg-false y ρ)) refl
  βˆ™ delete-literal-sound x Ο• (xβˆ‰Ο• ∘ there) ρ
... | no x≠y = ap₂ or
  (avoid-lit-insert x y xβ‰ y ρ)
  (delete-literal-sound x Ο• (xβˆ‰Ο• ∘ there) ρ)

Soundness and completeness of unit propagation follow quickly.

unit-propagate-sound
  : (x : Literal (suc Ξ“)) (Ο•s : CNF (suc Ξ“)) (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ Ο•s ⟧ (ρ [ lit-var x ≔ lit-val x ]) ≑ ⟦ unit-propagate x Ο•s ⟧ ρ
unit-propagate-sound x []       ρ = refl
unit-propagate-sound x (Ο• ∷ Ο•s) ρ with elem? x Ο•
... | yes xβˆˆΟ• = apβ‚‚ and
  (any-one-of (Ξ» l β†’ ⟦ l ⟧ (ρ [ lit-var x ≔ lit-val x ]))
    x Ο• xβˆˆΟ• (lit-assign-true x ρ))
  (unit-propagate-sound x Ο•s ρ)
... | no Β¬xβˆ‰Ο• = apβ‚‚ and
  (delete-literal-sound x Ο• Β¬xβˆ‰Ο• ρ)
  (unit-propagate-sound x Ο•s ρ)

unit-propagate-complete
  : (x : Literal (suc Ξ“)) (Ο•s : CNF (suc Ξ“)) (ρ : Fin (suc Ξ“) β†’ Bool)
  β†’ ⟦ x  ⟧ ρ ≑ true
  β†’ ⟦ Ο•s ⟧ ρ ≑ ⟦ unit-propagate x Ο•s ⟧ (delete ρ (lit-var x))
unit-propagate-complete x Ο•s ρ x-true =
  ap ⟦ Ο•s ⟧ (sym $ funext $
    Fin.insert-delete ρ (lit-var x) (lit-val x) (literal-sat-val x ρ x-true))
  βˆ™ unit-propagate-sound x Ο•s (delete ρ (lit-var x))

Since the syntax of CNF is a very β€œdiscrete” object (it consists of lists of lists of numbers), it’s possible to write a decision procedure which traverses a list of clauses and picks a clause consisting of a literal, if one exists.

has-unit-clause? : (Ο•s : CNF Ξ“) β†’ Dec (Ξ£[ x ∈ Literal Ξ“ ] ((x ∷ []) βˆˆβ‚— Ο•s))
has-unit-clause? [] = no (¬some-[] ∘ snd)

has-unit-clause? ([] ∷ Ο•s) with has-unit-clause? Ο•s
... | yes (x , xβˆˆΟ•s) = yes (x , there xβˆˆΟ•s)
... | no  ¬ϕ-unit    = no Ξ» where
  (x , here  ∷=[]) β†’ βˆ·β‰ [] ∷=[]
  (x , there xβˆˆΟ•s) β†’ ¬ϕ-unit (x , xβˆˆΟ•s)

has-unit-clause? ((x ∷ []) ∷ Ο•s)    = yes (x , here refl)
has-unit-clause? ((x ∷ y ∷ Ο•) ∷ Ο•s) with has-unit-clause? Ο•s
... | yes (x , xβˆˆΟ•s) = yes (x , there xβˆˆΟ•s)
... | no  ¬ϕ-unit    = no Ξ» where
  (x , here  p)    β†’ βˆ·β‰ [] (∷-tail-inj (sym p))
  (x , there xβˆˆΟ•s) β†’ ¬ϕ-unit (x , xβˆˆΟ•s)

We can now piece together the result which justifies unit propagation: If we have a satisfying assignment ΟβŠ¨Ο•\rho \vDash \phi, and a literal xx appears as a unit clause in Ο•\phi, then we know that ρ(x)\rho(x) must be true.

unit-clause-sat
  : (x : Literal Ξ“) (Ο•s : CNF Ξ“)
  β†’ (x ∷ []) βˆˆβ‚— Ο•s
  β†’ (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ Ο•s ⟧ ρ ≑ true β†’ ⟦ x ⟧ ρ ≑ true
unit-clause-sat x (Ο• ∷ Ο•s) (here [x]=Ο•) ρ Ο•s-sat =
  ⟦ x ⟧ ρ      β‰‘βŸ¨ sym (or-falser _) βŸ©β‰‘
  ⟦ x ∷ [] ⟧ ρ β‰‘βŸ¨ ap (Ξ» e β†’ (⟦ e ⟧ ρ)) [x]=Ο• βŸ©β‰‘
  ⟦ Ο• ⟧ ρ      β‰‘βŸ¨ and-reflect-true-l Ο•s-sat βŸ©β‰‘
  true         ∎
unit-clause-sat x (y ∷ Ο•s) (there [x]βˆˆΟ•s) ρ Ο•s-sat =
  unit-clause-sat x Ο•s [x]βˆˆΟ•s ρ (and-reflect-true-r Ο•s-sat)

We also note that it is impossible to find a satisfying assignment to a clause with no atoms.

Β¬empty-clause-sat : (Ο• : Clause 0) (ρ : Fin 0 β†’ Bool) β†’ ⟦ Ο• ⟧ ρ ≑ true β†’ βŠ₯
Β¬empty-clause-sat []           ρ sat = trueβ‰ false (sym sat)
Β¬empty-clause-sat (lit () ∷ Ο•) ρ sat
Β¬empty-clause-sat (neg () ∷ Ο•) ρ sat

Next, we observe that if the result of unit propagation is satisfiable, then the original expression must be satisfiable. Likewise, if the result of unit propagation is unsatisfiable, then the original expression is unsatisfiable.

unit-propagate-sat
  : (x : Literal (suc Ξ“)) (Ο•s : CNF (suc Ξ“))
  β†’ Ξ£[ ρ ∈ (Fin Ξ“ β†’ Bool) ]       (⟦ unit-propagate x Ο•s ⟧ ρ ≑ true)
  β†’ Ξ£[ ρ ∈ (Fin (suc Ξ“) β†’ Bool) ] (⟦ Ο•s ⟧ ρ ≑ true)
unit-propagate-sat x Ο•s (ρ , ρ-sat) =
    ρ [ lit-var x ≔ lit-val x ]
  , unit-propagate-sound x Ο•s ρ βˆ™ ρ-sat

unit-propagate-unsat
  : (x : Literal (suc Ξ“))
  β†’ (Ο•s : CNF (suc Ξ“))
  β†’ Β¬ Ξ£[ ρ ∈ (Fin Ξ“ β†’ Bool) ]       (⟦ unit-propagate x Ο•s ⟧ ρ ≑ true)
  β†’ Β¬ Ξ£[ ρ ∈ (Fin (suc Ξ“) β†’ Bool) ] ((⟦ Ο•s ⟧ ρ ≑ true) Γ— (⟦ x ⟧ ρ ≑ true))
unit-propagate-unsat x Ο•s Β¬sat (ρ , ρ-sat , x-sat) = Β¬sat $
    delete ρ (lit-var x)
  , sym (unit-propagate-complete x Ο•s ρ x-sat) βˆ™ ρ-sat

Armed with these lemmas, we can finally write our SAT solver. We shall perform induction on the number of atoms in our CNF expression, Ο•\phi. If Ο•\phi has no atoms, then we know its satisfiability by looking at the clauses: having no clauses is the CNF representation of ⊀\top, while having an empty clause is the CNF representation of βŠ₯\bot.

cnf-sat? : (Ο•s : CNF Ξ“) β†’ Dec (Ξ£[ ρ ∈ (Fin Ξ“ β†’ Bool) ] (⟦ Ο•s ⟧ ρ ≑ true))
cnf-sat? {Ξ“ = zero} []       = yes ((Ξ» ()) , refl)
cnf-sat? {Ξ“ = zero} (Ο• ∷ Ο•s) = no Ξ» where
  (ρ , sat) β†’ Β¬empty-clause-sat Ο• ρ (and-reflect-true-l sat)

The interesting case is when Ο•\phi contains at least one atom. Ideally, Ο•\phi has a unit clause, in which case we can perform unit propagation, and recursively and check satisfiability of the (hopefully much smaller!) resulting formula.

cnf-sat? {Ξ“ = suc Ξ“} Ο•s with has-unit-clause? Ο•s
... | yes (x , [x]βˆˆΟ•s) with cnf-sat? (unit-propagate x Ο•s)
...   | yes sat = yes (unit-propagate-sat x Ο•s sat)
...   | no Β¬sat = no Ξ» (ρ , ρ-sat) β†’
        unit-propagate-unsat x Ο•s Β¬sat
          (ρ , ρ-sat , unit-clause-sat x Ο•s [x]βˆˆΟ•s ρ ρ-sat)

If there aren’t, then we’re slightly out of luck. We’ll have to guess: We pick the first atom in Ο•\phi and arbitrarily decide that it must be true. We can then propagate this choice, using the same unit-propagation procedure, to obtain a formula Ο•[true/0]\phi[\mathrm{true}/0]. If this formula is satisfiable, we know that Ο•\phi is, too.

cnf-sat? {Ξ“ = suc Ξ“} Ο•s
    | no ¬ϕs-unit with cnf-sat? (unit-propagate (lit fzero) Ο•s)
...   | yes sat-true = yes (unit-propagate-sat (lit fzero) Ο•s sat-true)

But choosing true\mathrm{true} was a guess, and it might have been wrong! If it was, then we’ll try again: we’ll check satisfiability of Ο•[false/0]\phi[\mathrm{false}/0]. Once again, satisfiability of this new formula implies satisfiability of the original.

...   | no Β¬sat-true with cnf-sat? (unit-propagate (neg fzero) Ο•s)
...     | yes sat-false = yes (unit-propagate-sat (neg fzero) Ο•s sat-false)

However, we might have been wrong again! It might be the case that the expression is unsatisfiable. In this case we can return β€œUNSAT”: if anyone claims to have a satisfying assignment ΟβŠ¨Ο•\rho \vDash \phi, they must have chosen one of two values for ρ(0)\rho(0), and we know that neither can work.

...     | no Β¬sat-false = no Ξ» (ρ , ρ-sat) β†’ Bool-elim (Ξ» b β†’ ρ fzero ≑ b β†’ βŠ₯)
  (Ξ» ρ₀-true  β†’ unit-propagate-unsat (lit fzero) Ο•s Β¬sat-true
    (ρ , ρ-sat , ρ₀-true))
  (Ξ» ρ₀-false β†’ unit-propagate-unsat (neg fzero) Ο•s Β¬sat-false
    (ρ , ρ-sat , ap not ρ₀-false))
  (ρ fzero) refl

And that’s it! Note that β€œclassic” DPLL also includes a second rule known as pure literal elimination. The idea here is that if a literal only shows up as negated or not negated, then we can delete all occurrences of that literal. However, this operation is somewhat expensive to perform, and also rather annoying to program in Agda. Therefore, it has been omitted from this implementation.