Last active
September 28, 2023 06:42
-
-
Save aspiwack/4830162f8d4054bfa6c98e7a485aadc9 to your computer and use it in GitHub Desktop.
Functional CDCL
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Cdcl where | |
import Data.Foldable | |
import Data.Maybe | |
import Data.Monoid | |
type Atom = Int | |
type Literal = (Bool, Atom) | |
neg :: Literal -> Literal | |
neg (p, a) = (not p, a) | |
-- Invariants: clause non-empty, no duplicate or contradictory literal | |
type Clause = [Literal] | |
-- 'Nothing' => contradiction | |
set_lit :: Literal -> [Clause] -> Maybe [Clause] | |
set_lit (p, a) cs = | |
catMaybes <$> traverse set_in_clause cs | |
where | |
-- 'Nothing' => empty clause (conflict), `Just Nothing` => true clause (must | |
-- be dropped) | |
set_in_clause :: Clause -> Maybe (Maybe Clause) | |
set_in_clause c = case catMaybes <$> traverse set_in_literal c of | |
Nothing -> Just Nothing | |
Just [] -> Nothing | |
Just c' -> Just (Just c') | |
-- 'Nothing' => set to true (clause must be dropped), `Just Nothing` => set | |
-- to false (literal must be dropped from clause) | |
set_in_literal :: Literal -> Maybe (Maybe Literal) | |
set_in_literal (p', a') | a == a' = if p == p' then Nothing else Just Nothing | |
set_in_literal l' = Just (Just l') | |
-- Possible refinement: make it obvious in the type that the returned clauses | |
-- all have at least two elements. Though honestly, without liquid types it's | |
-- probably a pain. | |
propagate :: [Clause] -> Maybe [Clause] | |
propagate cs = | |
case find_maybe unit cs of | |
Nothing -> Just cs | |
Just l -> do | |
cs' <- set_lit l cs | |
propagate cs' | |
where | |
unit :: Clause -> Maybe Literal | |
unit [l] = Just l | |
unit _ = Nothing | |
data Result = Sat | Unsat | |
data Intermediate | |
= Sat' | |
| Conflict [Clause] | |
sat :: [Clause] -> Result | |
sat cs = | |
case sat' cs of | |
Sat' -> Sat | |
Conflict _ -> Unsat | |
choose :: [Clause] -> Intermediate | |
choose [] = Sat' | |
choose ([] : _) = error "Can't happen" | |
choose cs@((l : _) : _) = | |
-- Because everything has two elements, can't yield the empty clause | |
let Just cs' = set_lit l cs | |
in case sat' cs' of | |
Sat' -> Sat' | |
Conflict conflicts -> | |
let conflicts' = map (neg l :) conflicts | |
in case sat' (cs' ++ conflicts') of | |
Sat' -> Sat' | |
Conflict conflicts'' -> Conflict (conflicts' ++ conflicts'') | |
sat' :: [Clause] -> Intermediate | |
sat' cs = | |
case propagate cs of | |
Nothing -> Conflict [[]] | |
Just cs' -> choose cs' | |
-- | 'find', but with a 'Maybe' | |
find_maybe :: (Foldable t) => (a -> Maybe b) -> t a -> Maybe b | |
find_maybe p = getFirst . foldMap (First . p) | |
set_in_literal (p',a') | a == a' = if p == p' then Nothing else Just Nothing | |
set_in_literal l' = Just (Just l') | |
-- Possible refinement: make it obvious in the type that the returned clauses | |
-- all have at least two elements. Though honestly, without liquid types it's | |
-- probably a pain. | |
propagate :: [Clause] -> Maybe [Clause] | |
propagate cs = | |
case find_maybe unit cs of | |
| Nothing -> Just cs | |
| Just l -> do | |
cs' <- set_lit l cs | |
propagate cs' | |
data Result = Sat | Unsat | |
data Intermediate | |
= Sat' | |
| Conflict [Clause] | |
sat :: [Clause] -> Result | |
sat cs = | |
case sat' cs of | |
Sat' -> Sat | |
Conflict _ -> Unsat | |
choose :: [Clause] -> Intermediate | |
choose [] = Sat' | |
choose ([]:_) = error "Can't happen" | |
choose cs@((l:_):_) = | |
-- Because everything has two elements, can't yield the empty clause | |
let Just cs' = set_lit l cs in | |
case sat' cs' of | |
Sat' -> Sat' | |
Conflict conflicts -> | |
let conflicts' = map (neg l:) conflicts in | |
case sat' (cs' ++ conflicts') of | |
Sat' -> Sat' | |
Conflict conflicts'' -> Conflict (conflicts' ++ conflicts'') | |
sat' :: [Clause] -> Intermediate | |
sat' cs = | |
case propagate cs of | |
Nothing -> Conflict [[]] | |
Just cs' -> choose cs' | |
--| 'find', but with a 'Maybe' | |
find_maybe :: Foldable t => (a -> Maybe b) -> t a -> Maybe b | |
find_maybe p = getFirst . fold (First . p) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment