Functional CDCL

Cdcl.hs

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)