From e68aea36d9559d98aed162cc7896fe081ca64b1d Mon Sep 17 00:00:00 2001 From: Dimitri Lozeve Date: Fri, 5 Aug 2016 08:16:32 +0100 Subject: [PATCH] Formatted comments for Haddock --- Civilisation.hs | 10 +++--- Sat.hs | 91 ++++++++++++++++++++++++++----------------------- 2 files changed, 54 insertions(+), 47 deletions(-) diff --git a/Civilisation.hs b/Civilisation.hs index b9537de..bae7583 100644 --- a/Civilisation.hs +++ b/Civilisation.hs @@ -10,12 +10,14 @@ Portability : portable -} +module Civilisation where + import Data.Maybe import Sat --- Main entry point of the program +-- | Main entry point of the program. main :: IO () main = do text <- readFile "test.cnf" @@ -24,11 +26,11 @@ main = do UNSAT -> putStrLn "UNSAT" SAT a -> putStrLn $ "SAT " ++ show a --- Parses a formula in the DIMACS CNF format. +-- | Parses a formula in the DIMACS CNF format. parseDIMACS :: String -> CNF parseDIMACS = mapMaybe parseClause . lines --- Parses a clause (a single line in the DIMACS file). +-- | Parses a clause (a single line in the DIMACS file). parseClause :: String -> Maybe Clause parseClause "" = Nothing parseClause ('c':_) = Nothing @@ -37,7 +39,7 @@ parseClause ('%':_) = Nothing parseClause ('0':_) = Nothing parseClause s = (Just . map (litFromInt . read) . init . words) s --- Interprets an Int, such as (-5), as a Lit, such as (Neg 5). +-- | Interprets an Int, such as -5, as a @Lit@, such as @Neg 5@. litFromInt :: Int -> Lit litFromInt n | n < 0 = Neg (-n) | otherwise = Pos n diff --git a/Sat.hs b/Sat.hs index 267b37a..988e35f 100644 --- a/Sat.hs +++ b/Sat.hs @@ -15,26 +15,26 @@ module Sat where import Data.List --- Variables are represented by positive integers +-- | Variables are represented by positive integers. type Var = Int --- A literal is either a variable, or the negation of a variable +-- | A literal is either a variable, or the negation of a variable. data Lit = Pos Var | Neg Var deriving (Eq, Show) --- A clause is a disjunction of literals, represented by a list of --- literals +-- | A clause is a disjunction of literals, represented by a list of +-- literals. type Clause = [Lit] --- A formula, represented in its Conjunctive Normal Form (CNF), is a --- conjunction of clauses, represented as a list +-- | A formula, represented in its Conjunctive Normal Form (CNF), is a +-- conjunction of clauses, represented as a list. type CNF = [Clause] --- An assignment is a list of literals. For instance, if an assignment --- contains (Pos 5), it means that in this assignment, the variable 5 --- is assigned to True. +-- | An assignment is a list of literals. For instance, if an assignment +-- contains @Pos 5@, it means that in this assignment, the variable 5 +-- is assigned to @True@. type Assignment = [Lit] --- The result of the SAT solver +-- | The result of the SAT solver. data Result = UNSAT | SAT Assignment deriving (Eq, Show) @@ -43,20 +43,21 @@ data Result = UNSAT | SAT Assignment deriving (Eq, Show) -- General-purpose functions --- Extracts a variable from a literal +-- | Extracts a variable from a literal. fromLit :: Lit -> Var fromLit (Pos x) = x fromLit (Neg x) = x --- Tests for positive/negative literals +-- | Tests for positive literals. isPos :: Lit -> Bool isPos (Pos _) = True isPos (Neg _) = False +-- | Tests for negative literals. isNeg :: Lit -> Bool isNeg = not . isPos --- Checks if a clause is always true, i.e. if it contains both a +-- | Checks if a clause is always true, i.e. if it contains both a -- literal and its negation. isClauseTrue :: Clause -> Bool isClauseTrue [] = False @@ -70,12 +71,12 @@ isClauseTrue (x:xs) -- Literal Evaluation --- Negates a literal +-- | Negates a literal. notLit :: Lit -> Lit notLit (Pos x) = Neg x notLit (Neg x) = Pos x --- Evaluates a CNF by fixing the value of a given literal +-- | Evaluates a CNF by fixing the value of a given literal. evalLit :: Lit -> CNF -> CNF evalLit _ [] = [] evalLit lit f = foldr g [] f @@ -86,19 +87,19 @@ evalLit lit f = foldr g [] f -- Pure Literal rule --- Tests whether a literal is pure, i.e. only appears as positive or --- negative +-- | Tests whether a literal is pure, i.e. only appears as positive or +-- negative. testPureLit :: Lit -> CNF -> Bool testPureLit _ [] = True testPureLit (Pos x) (c:cs) = Neg x `notElem` c && testPureLit (Pos x) cs testPureLit (Neg x) (c:cs) = Pos x `notElem` c && testPureLit (Neg x) cs --- Tests whether a variable appears only as a pure literal +-- | Tests whether a variable appears only as a pure literal. testPureVar :: Var -> CNF -> Bool testPureVar x f = testPureLit (Pos x) f || testPureLit (Neg x) f --- Given a pure literal (given as a variable), eliminates all the --- clauses containing it +-- | Given a pure literal (given as a variable), eliminates all the +-- clauses containing it. eliminatePure :: Var -> CNF -> CNF eliminatePure _ [] = [] eliminatePure x (c:cs) = @@ -106,23 +107,24 @@ eliminatePure x (c:cs) = then eliminatePure x cs else c : eliminatePure x cs --- Returns the set of positive or negative clauses of a formula +-- | Returns the set of positive clauses of a formula. posLits :: CNF -> [Lit] posLits = nub . filter isPos . concat +-- | Returns the set of negative clauses of a formula. negLits :: CNF -> [Lit] negLits = nub . filter isNeg . concat --- Returns the set of the pure literals of a formula +-- |Returns the set of the pure literals of a formula. pureLits :: CNF -> [Lit] pureLits f = (pos \\ map notLit neg) `union` (neg \\ map notLit pos) where pos = posLits f neg = negLits f --- Applies the pure literal rule: removes all clauses containing pure --- literals. The function also takes a preexisting assignment, and --- updates it by appending the value assigned to the eliminated pure --- literals. +-- | Applies the pure literal rule: removes all clauses containing +-- pure literals. The function also takes a preexisting assignment, +-- and updates it by appending the value assigned to the eliminated +-- pure literals. pureLitRule :: (CNF, Assignment) -> (CNF, Assignment) pureLitRule (f, asst) = (f', asst ++ pures) where pures = pureLits f @@ -131,11 +133,12 @@ pureLitRule (f, asst) = (f', asst ++ pures) -- Unit Propagation --- Evaluates the formula with all the unit clauses given in argument +-- | Evaluates the formula with all the unit clauses given in +-- argument. eliminateUnits :: [Lit] -> CNF -> CNF eliminateUnits xs f = foldr evalLit f xs --- Applies the unit propagation rule +-- | Applies the unit propagation rule. unitPropagate :: (CNF, Assignment) -> (CNF, Assignment) unitPropagate (f, asst) = let units = concat $ filter (\xs -> length xs == 1) f in @@ -146,22 +149,24 @@ unitPropagate (f, asst) = -- Resolution --- Returns the first common variable between two clauses, if it exists +-- | Returns the first common variable between two clauses, if it +-- exists. commonVar :: Clause -> Clause -> Maybe Lit commonVar _ [] = Nothing commonVar as (b:bs) = if b `elem` as || notLit b `elem` as then Just b else commonVar as bs --- Applies the resolution rule to two clauses sharing a variable. This --- function does not test whether the literals are of different sign. +-- | Applies the resolution rule to two clauses sharing a +-- variable. This function does not test whether the literals are of +-- different sign. resolve :: Clause -> Clause -> Maybe Clause resolve a b = do x <- commonVar a b return $ (a \\ [x, notLit x]) `union` (b \\ [x, notLit x]) --- Given a formula and a clause, returns a clause which can be reduced --- with the first one by applying the resolution rule. +-- | Given a formula and a clause, returns a clause which can be +-- reduced with the first one by applying the resolution rule. findMatchingClause :: CNF -> Clause -> Maybe Clause findMatchingClause _ [] = Nothing findMatchingClause f (x:xs) = @@ -169,7 +174,7 @@ findMatchingClause f (x:xs) = Nothing -> findMatchingClause f xs Just c -> Just c --- Returns a two clauses suitable for the resolution rule, if +-- | Returns a two clauses suitable for the resolution rule, if -- possible. findMatchingPair :: CNF -> Maybe (Clause, Clause) findMatchingPair [] = Nothing @@ -178,7 +183,7 @@ findMatchingPair (c:cs) = Nothing -> findMatchingPair cs Just d -> Just (c, d) --- Recursively applies the resolution rule to all suitable pairs of +-- | Recursively applies the resolution rule to all suitable pairs of -- clauses. resolveAll :: CNF -> CNF resolveAll f = case findMatchingPair f of @@ -191,10 +196,10 @@ resolveAll f = case findMatchingPair f of then resolveAll (f \\ [c,d]) else resolveAll $ e:(f \\ [c,d]) --- Applies the resolution rule to solve the formula. It recursively +-- | Applies the resolution rule to solve the formula. It recursively -- applies resolveAll and the unit propagation and pure literals --- rules, until it reaches the empty formula (therefore SAT) or an --- empty clause (therefore UNSAT). +-- rules, until it reaches the empty formula (therefore @SAT@) or an +-- empty clause (therefore @UNSAT@). resolutionSolve :: (CNF, Assignment) -> Result resolutionSolve ([], asst) = SAT asst resolutionSolve (f, asst) @@ -207,7 +212,7 @@ resolutionSolve (f, asst) -- Davis-Putnam-Logemann-Loveland (DPLL) --- DPLL algorithm, in its most simple form. Applies the unit +-- | DPLL algorithm, in its most simple form. Applies the unit -- propagation rule and the pure literal rule, and then select a -- literal (using the selectLit function) and calls itself on the two -- possible branches, stopping when a solution is found. @@ -221,10 +226,10 @@ solveDPLL (f, asst) SAT a -> SAT a UNSAT -> solveDPLL (evalLit (notLit lit) f', notLit lit : asst') --- Select a literal from a given formula. This function just takes the --- first available literal. The function head makes it unsafe, as it --- might fail if the formula is empty or if the first clause is --- empty. However, this function is only called by solveDPLL, which +-- | Select a literal from a given formula. This function just takes +-- the first available literal. The function @head@ makes it unsafe, +-- as it might fail if the formula is empty or if the first clause is +-- empty. However, this function is only called by @solveDPLL@, which -- checks beforehand to avoid these cases. selectLit :: CNF -> Lit selectLit = head . head