module SAT.DPLL (dpll, SATResult(..)) where

import SAT.CNF
import SAT.UnitProp
import qualified Data.Map.Strict as Map
import Data.List (nub, sortOn)

data SATResult
  = SAT (Map.Map Int Bool)
  | UNSAT
  deriving (Show)

dpll :: CNF -> SATResult
dpll (CNF clauses numVars) = solve Map.empty clauses
  where
    solve assignment [] = SAT assignment
    solve assignment cls =
      case unitPropagate assignment cls of
        Conflict -> UNSAT
        Propagated asgn' cls' ->
          if null cls' then SAT asgn'
          else
            let var = chooseVar asgn' cls'
            in case solve (Map.insert var True asgn') cls' of
                 SAT a -> SAT a
                 UNSAT -> solve (Map.insert var False asgn') cls'

chooseVar :: Map.Map Int Bool -> [Clause] -> Int
chooseVar asgn clauses =
  let allVars = nub $ map litVar $ concat clauses
      unassigned = filter (\v -> not (Map.member v asgn)) allVars
  in case unassigned of
       (v:_) -> v
       [] -> 0