Commit a037c2eb authored by Michael Hanus's avatar Michael Hanus
Browse files

Initial version of dimacs package

parents
*~
.cpm
.curry
*.cnf
Copyright (c) 2017, Michael Hanus
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. Neither the names of the copyright holders nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
dimacs
======
This package provides an interface to SAT solvers supporting
the DIMACS format.
Boolean formulas can be defined in Curry using the type
`Dimacs.Types.Boolean` and the constructor operations defined in
module `Dimacs.Build`.
Formulas can be checked for satisfiabilty using the operation
`Dimacs.Solver.solveWithDimacs`.
Examples can be found in the directory `examples`.
-- Examples for testing the satisfiability of Boolean formulas.
import Dimacs.Build
import Dimacs.Solver
import Dimacs.Types
-- A satisfiable formula.
b1 :: Boolean
b1 = (va 1 .\/ va 2) ./\ no (va 3)
solveb1 :: IO [(Int,Bool)]
solveb1 = solveWithDimacs z3Dimacs b1
-- An unsatisfiable formula.
b2 :: Boolean
b2 = (va 1 .\/ va 2) ./\ (va 1 .\/ no (va 2)) ./\
(no (va 1) .\/ va 2) ./\ (no (va 1) .\/ no (va 2))
solveb2 :: IO [(Int,Bool)]
solveb2 = solveWithDimacs z3Dimacs b2
{
"name": "dimacs",
"version": "0.0.1",
"author": "Sven Hueser, Michael Hanus <mh@informatik.uni-kiel.de>",
"maintainer": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "An interface to SAT solvers supporting DIMACS.",
"category": [ "Constraints", "Verification" ],
"license": "BSD-3-Clause",
"licenseFile": "LICENSE",
"dependencies": {
},
"exportedModules": [ "Dimacs.Types", "Dimacs.Build", "Dimacs.Solver" ],
"source": {
"git": "https://git.ps.informatik.uni-kiel.de/curry-packages/dimacs.git",
"tag": "$version"
}
}
------------------------------------------------------------------------------
--- A library with deterministic parser combinators.
---
--- Might be moved into a separate package in the future.
------------------------------------------------------------------------------
module DetParser where
type Parser token a = [token] -> Either ParseError ([token], a)
type ParseError = String
--- Combine parsers with resulting representation of first one.
(<*) :: Parser token a -> Parser token b -> Parser token a
a <* b = const <$> a <*> b
--- Combine parsers with resulting representation of second one.
(*>) :: Parser token a -> Parser token b -> Parser token b
a *> b = const id <$> a <*> b
(<*>) :: Parser token (a -> b) -> Parser token a -> Parser token b
a <*> b = \ts -> case a ts of
Left e -> Left e
Right (ts', f) -> case b ts' of
Left e -> Left e
Right (ts2, x) -> Right (ts2, f x)
--- Combines two parsers in an alternative manner.
(<|>) :: Parser token a -> Parser token a -> Parser token a
a <|> b = \ts -> case a ts of
Right (ts', x) -> Right (ts', x)
Left e -> case b ts of
Left e' -> Left $ "parse error: " ++ e' ++ " | " ++ e
Right (ts2, y) -> Right (ts2, y)
--- Apply unary function `f` to result of parser `p`
(<$>) :: (a -> b) -> Parser token a -> Parser token b
f <$> p = yield f <*> p
--- Apply binary function `f` to results of parsers `p1` and `p2`
liftP2 :: (a -> b -> r) -> Parser token a -> Parser token b -> Parser token r
liftP2 f p1 p2 = \ts -> case p1 ts of
Left e -> Left e
Right (ts', x) -> case p2 ts' of
Left e -> Left e
Right (ts2, y) -> Right (ts2, f x y)
--- A parser with `x` as representation while consuming no tokens.
yield :: a -> Parser token a
yield x ts = Right (ts, x)
--- A parser recognizing a particular terminal symbol.
terminal :: token -> Parser token ()
terminal _ [] = eof []
terminal x (t:ts) = case x == t of
True -> Right (ts, ())
False -> unexpected t ts
--- Returns parse error about unexpected end-of-file
eof :: Parser token a
eof _ = Left "unexpected end-of-file"
--- Returns parse error about unexpected token `t`
unexpected :: token -> Parser token a
unexpected t _ = Left $ "unexpected token " ++ show t
--- A star combinator for parsers. The returned parser
--- repeats zero or more times a parser p and
--- returns the representation of all parsers in a list.
star :: Parser token a -> Parser token [a]
star p = (\ts -> case p ts of
Left e -> Left e
Right (ts', x) -> (x:) <$> star p $ ts')
<|> yield []
--- A some combinator for parsers. The returned parser
--- repeats the argument parser at least once.
some :: Parser token a -> Parser token [a]
some p = \ts -> case p ts of
Left e -> Left e
Right (ts', x) -> (x:) <$> star p $ ts'
-- same as <$>
-- liftP :: (a -> r) -> Parser token a -> Parser token r
-- liftP f m = \ts -> let res = m ts
-- in case res of
-- Left e -> Left e
-- Right (ts', x) -> Right (ts', f x)
------------------------------------------------------------------------------
--- This module defines some operation to support the construction
--- of Boolean formulas.
---
--- @author Sven Hueser
--- @version September 2017
------------------------------------------------------------------------------
module Dimacs.Build where
import List (nub)
import Dimacs.Types
infixr 3 ./\
infixr 2 .\/
--- A Boolean variable with an index. Note that the index should be
--- a positive number.
va :: Int -> Boolean
va = Var
--- Boolean negation.
no :: Boolean -> Boolean
no = Not
--- Negated variable with an index. Note that the index should be
--- a positive number.
nv :: Int -> Boolean
nv = no . va
--- Conjunction.
(./\) :: Boolean -> Boolean -> Boolean
a ./\ b = case (a, b) of
(Var _, Var _) -> And [a,b]
(Var _, Not _) -> And [a,b]
(Var _, And l) -> And $ a:l
(Var _, Or _) -> And [a,b]
(_ , Var _) -> b ./\ a
(Not _, Not _) -> And [a,b]
(Not _, And l) -> And $ a:l
(Not _, Or _) -> And [a,b]
(_ , Not _) -> b ./\ a
(And p, And q) -> And $ p ++ q
(And l, Or _) -> And $ b:l
(Or _, Or _) -> And [a,b]
(Or _, And _) -> b ./\ a
--- Disjunction.
(.\/) :: Boolean -> Boolean -> Boolean
a .\/ b = case (a, b) of
(Var _, Var _) -> Or [a,b]
(Var _, Not _) -> Or [a,b]
(Var _, And _) -> Or [a,b]
(Var _, Or l) -> Or $ a:l
(_ , Var _) -> b .\/ a
(Not _, Not _) -> Or [a,b]
(Not _, And _) -> Or [a,b]
(Not _, Or l) -> Or $ a:l
(_ , Not _) -> b ./\ a
(And _, And _) -> Or [a,b]
(And _, Or l) -> Or $ a:l
(Or p, Or q) -> Or $ p ++ q
(Or _, And _) -> b .\/ a
--- Exclusive or.
xor :: Boolean -> Boolean -> Boolean
a `xor` b = (no a ./\ b) .\/ (a ./\ no b)
--------------------------------------------------------------------------------
nnf :: Boolean -> Boolean
nnf (Var x) = Var x
nnf n@(Not f) = case f of
(Var _) -> n
(Not g) -> nnf g
(And fs) -> Or (map (nnf . Not) fs)
(Or fs) -> And (map (nnf . Not) fs)
nnf (And fs) = And (map nnf fs)
nnf (Or fs) = Or (map nnf fs)
cnf :: Boolean -> Boolean
cnf (Var x) = Or [Var x]
cnf (Not v) = Or [Not v]
cnf (And fs) = And (map cnf fs)
cnf (Or []) = Or []
cnf (Or [f]) = cnf f
cnf (Or (f1:f2:fs)) = dist (cnf f1) (cnf (Or (f2:fs)))
dist :: Boolean -> Boolean -> Boolean
dist xs ys = case (xs, ys) of
(And [], _) -> And []
(_, And []) -> And []
(And [f1], f2) -> dist f1 f2
(f1, And [f2]) -> dist f1 f2
(And (f1:fs), f2) -> And [dist f1 f2, dist (And fs) f2]
(f1, And (f2:fs)) -> And [dist f1 f2, dist f1 (And fs)]
(f1, f2) -> Or [f1,f2]
flatten :: Boolean -> Boolean
flatten f = case f of
(And fs) -> And (flattenAnd fs)
(Or fs) -> Or (flattenOr fs)
_ -> f
flattenAnd :: [Boolean] -> [Boolean]
flattenAnd cs = case cs of
[] -> []
((And fs):gs) -> flattenAnd (fs ++ gs)
(f:fs) -> flatten f : flattenAnd fs
flattenOr :: [Boolean] -> [Boolean]
flattenOr ds = case ds of
[] -> []
((Or fs):gs) -> flattenOr (fs ++ gs)
(f:fs) -> f: flattenOr fs
nubB :: Boolean -> Boolean
nubB bs = case bs of
(And fs) -> And (map nubB fs)
(Or fs) -> Or (nub fs)
_ -> bs
toCNF :: Boolean -> Boolean
toCNF = filterTauts . nubB . flatten . cnf . nnf
filterTauts :: Boolean -> Boolean
filterTauts b = case b of
(And ls) -> And $ filter (not . isTaut) ls
_ -> b
isTaut :: Boolean -> Bool
isTaut b = case b of
(Or ls) -> isTaut' ls
_ -> False
where
isTaut' [] = False
isTaut' (x:xs) = containsInverted x xs || isTaut' xs
containsInverted x xs = case x of
(Var i) -> nv i `elem` xs
(Not (Var i)) -> va i `elem` xs
_ -> False
------------------------------------------------------------------------------
--- This module defines a simple parser for the output of a DIMACS solver.
---
--- @author Sven Hueser
--- @version September 2017
------------------------------------------------------------------------------
module Dimacs.Parser where
import DetParser
import Dimacs.Types
import Dimacs.Scanner
parse :: String -> Either ParseError [Boolean]
parse s = case parseDimacs $ scan s of
Left e -> Left e
Right ([], x) -> Right x
Right _ -> Left "incomplete parse"
parseDimacs :: Parser Token [Boolean]
parseDimacs [] = eof []
parseDimacs (t:ts) = case t of
KW_sat -> some parseVar <* terminal EOF $ ts
KW_unsat -> terminal EOF *> yield [] $ ts
_ -> unexpected t ts
parseVar :: Parser Token Boolean
parseVar [] = eof []
parseVar (t:ts) = case t of
VarNot -> Not <$> parseVar $ ts
VarNum i -> yield (Var i) ts
_ -> unexpected t ts
------------------------------------------------------------------------------
--- This module defines operations to show Boolean formulas in DIMACS format.
---
--- @author Michael Hanus, Sven Hueser
--- @version September 2017
------------------------------------------------------------------------------
module Dimacs.Pretty ( showDimacs, prettyDimacs, prettySolution )
where
import Pretty
import Dimacs.Types
import Dimacs.Build
--- Shows a Boolean formula in DIMACS format.
showDimacs :: Boolean -> String
showDimacs b = prettyDimacs (maxVar b) b
--- Pretty print a Boolean formula (second argument)
--- with a given number of variables (first argument) in DIMACS format.
prettyDimacs :: Int -> Boolean -> String
prettyDimacs nv = pPrint . (ppDimacs nv) . toCNF
--- Pretty print a solution of a Boolean formula.
prettySolution :: Boolean -> String
prettySolution = pPrint . (line <>) . ppCNF
ppDimacs :: Int -> Boolean -> Doc
ppDimacs nv b =
let nd = case b of
Or _ -> 1
And l -> length l
_ -> error "Dimacs.Pretty: need formula in CNF"
in (text "p cnf" <+> int nv <+> int nd) $$ (ppCNF b)
ppCNF :: Boolean -> Doc
ppCNF b = case b of
Var i -> int i
Not n -> text "-" <> ppCNF n
And bs -> vsep $ map ppCNF bs
Or bs -> (hsep $ map ppCNF bs) <+> text "0"
------------------------------------------------------------------------------
--- This module defines a simple scanner for the output of a DIMACS solver.
---
--- @author Sven Hueser
--- @version September 2017
------------------------------------------------------------------------------
module Dimacs.Scanner where
import ReadNumeric
import Char (isAlpha, isDigit, toLower)
data Token
-- keywords
= KW_sat
| KW_unsat
-- variables
| VarNum Int
| VarNot
-- other
| EOF
keywords :: [(String, Token)]
keywords =
[ ("sat" , KW_sat)
, ("satisfiable" , KW_sat)
, ("unsat" , KW_unsat)
, ("unsatisfiable" , KW_unsat)
]
keyword :: String -> Token
keyword k = maybe (error $ "unknown keyword: " ++ k) id (lookup (map toLower k) keywords)
scan :: String -> [Token]
scan str = case str of
"" -> [EOF]
('-':s) -> VarNot : scan s
('0':s) -> scan s -- minisat puts a 0 at the end of the variables, z3 doesn't; ignore it
('s':' ':s) -> scan s -- lingeling puts 's' at start of sat/unsat line
('v':' ':s) -> scan s -- lingeling puts 'v' at start of solution line
('c':' ':s) -> scan $ tail $ dropWhile (\c -> c /= '\n') s
_ -> scan' str
where
scan' :: String -> [Token]
scan' "" = [EOF] -- should not be possible, but removes missing pattern warning
scan' x@(c:cs) | isDigit c = scanNum x
| isAlpha c = scanKeyword x
| otherwise = scan cs
scanKeyword :: String -> [Token]
scanKeyword cs =
let (key, rest) = span isAlpha cs
in keyword key : scan rest
scanNum :: String -> [Token]
scanNum cs =
let v = readInt cs
in case v of
Just (num, rest) -> VarNum num : scan rest
Nothing -> error "should not be possible"
------------------------------------------------------------------------------
--- This module defines an operation to solve a Boolean formula
--- with some SAT solver supporting the DIMACS format.
--- It also defines configuration for various solvers.
---
--- @author Michael Hanus
--- @version September 2017
------------------------------------------------------------------------------
module Dimacs.Solver where
import IO
import IOExts
import Dimacs.Parser ( parse )
import Dimacs.Pretty ( showDimacs )
import Dimacs.Types
------------------------------------------------------------------------------
--- Type of solvers configuration with fields for the name of the executable
--- and command line flags.
data SolverConfig = Config
{ executable :: String
, flags :: [String]
}
--- The configuration of the Z3 solver for DIMACS.
z3Dimacs :: SolverConfig
z3Dimacs = Config { executable = "z3"
, flags = ["-in", "-dimacs"]
}
--- The configuration of the lingeling solver.
lingeling :: SolverConfig
lingeling = Config { executable = "lingeling"
, flags = ["-q"]
}
------------------------------------------------------------------------------
--- Checks the satisfiability of a Boolean formula with a SAT solver
--- supporting DIMACS format.
--- A list associating the variable indices to Boolean values so that
--- the formula is satisfied is returned.
--- If the formula is unsatisfiable, the returned list is empty.
solveWithDimacs :: SolverConfig -> Boolean -> IO [(Int,Bool)]
solveWithDimacs scfg boolean = do
let satcmd = unwords $ executable scfg : flags scfg
(inH, outH, _) <- execCmd satcmd
hPutStr inH $ showDimacs boolean
hFlush inH
hClose inH
response <- hGetContents outH
case parse response of
Left e -> error e
Right b -> return (boolVars2AssocList b)
--- Translates a list of Boolean variables into a list associating
--- the variable indices to Boolean values.
boolVars2AssocList :: [Boolean] -> [(Int,Bool)]
boolVars2AssocList = map bvar2assoc
where
bvar2assoc bv = case bv of
Var i -> (i,True)
Not (Var i) -> (i,False)
_ -> error $ "boolVars2AssocList: not a variable: " ++ show bv
------------------------------------------------------------------------------
\ No newline at end of file
------------------------------------------------------------------------------
--- This module defines the data type to represent Boolean formulas
--- together with some auxiliary operations.
---
--- @author Michael Hanus, Sven Hueser
--- @version September 2017
------------------------------------------------------------------------------
module Dimacs.Types where
import List ( maximum )
--- The type of Boolean formulas.
--- Not that variables should be numbered from 1.
data Boolean = Var Int
| Not Boolean
| And [Boolean]
| Or [Boolean]
--- Returns the maximal variable index in a Boolean formula.
maxVar :: Boolean -> Int
maxVar (Var n) = n
maxVar (Not b) = maxVar b
maxVar (And bs) = if null bs then 0 else maximum (map maxVar bs)
maxVar (Or bs) = if null bs then 0 else maximum (map maxVar bs)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment