module Logic.Propositional.Classical.SAT where

# 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
$Ο_{0}β§Pβ§Ο_{1}$
β that is, we have a clause which consists of a single literal, then
itβs necessary for
$β¨Ο$
that
$β¨P.$
Not only does this give us one datum of our satisfying assignment, it
also lets us get rid of any clauses that mention
$P,$
since they must also be true!

Even better, we can also remove any occurrences of $Β¬P$ from our clauses β since weβve decided that $P$ is true, having $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
$Ο$
and a formula in
$Ξ_{0},Ο,Ξ_{1},$
weβll return a formula in
$Ξ_{0},Ξ_{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

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 $x$ appears as a unit clause in $Ο,$ then we know that $Ο(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, $Ο.$ 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
$Ο[true/0].$
*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 $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].$ 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 *un*satisfiable. In this case we can return
βUNSATβ: if anyone claims to have a satisfying assignment
$Οβ¨Ο,$
they must have chosen one of two values for
$Ο(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.