open import 1Lab.Prelude

open import Data.Id.Base
open import Data.Bool
open import Data.List hiding (_++_)
open import Data.Dec
open import Data.Fin using (Fin; fzero; fsuc; avoid; _[_β_]; delete)
open import Data.Nat
open import Data.Sum

open import Logic.Propositional.Classical.CNF
open import Logic.Propositional.Classical

open import Meta.Brackets

import Data.Fin as Fin

module Logic.Propositional.Classical.SAT where

private variable
Ξ Ξ Ξ : Nat
Ο ΞΈ ΞΆ : Ctx Ξ
P Q R : Proposition Ξ


# SAT solvingπ

SAT solving is the process of determining if we can find some assignment of variables that makes a given formula 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 breaks down as β that is, we have a clause which consists of a single literal, then itβs necessary for that Not only does this give us one datum of our satisfying assignment, it also lets us get rid of any clauses that mention since they must also be true!

Even better, we can also remove any occurrences of from our clauses β since weβve decided that is true, having 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 and a formula in weβll return a formula in

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

avoid-lit-insert {Ξ = Ξ} x (lit y) xβ y Ο =
Fin.avoid-insert Ο (lit-var x) (lit-val x) y xβ y
avoid-lit-insert {Ξ = Ξ} x (neg y) xβ y Ο =
ap not (Fin.avoid-insert Ο (lit-var x) (lit-val x) y xβ y)

lit-assign-neg-false (lit x) Ο = Fin.insert-lookup Ο x false
lit-assign-neg-false (neg x) Ο = ap not (Fin.insert-lookup Ο x true)

lit-assign-true (lit x) Ο = Fin.insert-lookup Ο x true
lit-assign-true (neg x) Ο = ap not (Fin.insert-lookup Ο x false)


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 Ξ» ()

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 and a literal appears as a unit clause in then we know that 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, If has no atoms, then we know its satisfiability by looking at the clauses: having no clauses is the CNF representation of while having an empty clause is the CNF representation of

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 contains at least one atom. Ideally, 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 and arbitrarily decide that it must be true. We can then propagate this choice, using the same unit-propagation procedure, to obtain a formula If this formula is satisfiable, we know that 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 was a guess, and it might have been wrong! If it was, then weβll try again: weβll check satisfiability of 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 they must have chosen one of two values for 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.