Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
(This file is a part of MIOS.) Minisat-based Implementation and Optimization Study on SAT solver
Synopsis
- versionId :: String
- data CNFDescription = CNFDescription {
- _numberOfVariables :: !Int
- _numberOfClauses :: !Int
- _pathname :: !FilePath
- module SAT.Mios.OptionParser
- type SolverResult = Either SolverException Certificate
- data Certificate
- buildOption :: Either FilePath String -> MiosProgramOption
- buildSolver :: MiosProgramOption -> IO Solver
- buildDescription :: FilePath -> Solver -> IO CNFDescription
- executeSolver :: MiosProgramOption -> Solver -> IO ()
- executeValidator :: MiosProgramOption -> Solver -> IO ()
- runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int])
- solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]
- solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int]
- showAnswerFromString :: String -> IO String
- validate :: Traversable t => Solver -> t Int -> IO Bool
- validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool
- dumpAssigmentAsCNF :: MiosProgramOption -> Certificate -> IO String
Interface to the core of solver
data CNFDescription Source #
Misc information on a CNF
CNFDescription | |
|
Instances
Eq CNFDescription Source # | |
Defined in SAT.Mios.Types (==) :: CNFDescription -> CNFDescription -> Bool # (/=) :: CNFDescription -> CNFDescription -> Bool # | |
Ord CNFDescription Source # | |
Defined in SAT.Mios.Types compare :: CNFDescription -> CNFDescription -> Ordering # (<) :: CNFDescription -> CNFDescription -> Bool # (<=) :: CNFDescription -> CNFDescription -> Bool # (>) :: CNFDescription -> CNFDescription -> Bool # (>=) :: CNFDescription -> CNFDescription -> Bool # max :: CNFDescription -> CNFDescription -> CNFDescription # min :: CNFDescription -> CNFDescription -> CNFDescription # | |
Read CNFDescription Source # | |
Defined in SAT.Mios.Types readsPrec :: Int -> ReadS CNFDescription # readList :: ReadS [CNFDescription] # | |
Show CNFDescription Source # | |
Defined in SAT.Mios.Types showsPrec :: Int -> CNFDescription -> ShowS # show :: CNFDescription -> String # showList :: [CNFDescription] -> ShowS # |
module SAT.Mios.OptionParser
Main Interace
type SolverResult = Either SolverException Certificate Source #
the type that Mios returns This captures the following three cases: * solved with a satisfiable assigment, * proved that it's an unsatisfiable problem, and * aborted due to Mios specification or an internal error
data Certificate Source #
terminate and find an SAT/UNSAT answer
Instances
Eq Certificate Source # | |
Defined in SAT.Mios.Types (==) :: Certificate -> Certificate -> Bool # (/=) :: Certificate -> Certificate -> Bool # | |
Ord Certificate Source # | |
Defined in SAT.Mios.Types compare :: Certificate -> Certificate -> Ordering # (<) :: Certificate -> Certificate -> Bool # (<=) :: Certificate -> Certificate -> Bool # (>) :: Certificate -> Certificate -> Bool # (>=) :: Certificate -> Certificate -> Bool # max :: Certificate -> Certificate -> Certificate # min :: Certificate -> Certificate -> Certificate # | |
Read Certificate Source # | |
Defined in SAT.Mios.Types readsPrec :: Int -> ReadS Certificate # readList :: ReadS [Certificate] # readPrec :: ReadPrec Certificate # readListPrec :: ReadPrec [Certificate] # | |
Show Certificate Source # | |
Defined in SAT.Mios.Types showsPrec :: Int -> Certificate -> ShowS # show :: Certificate -> String # showList :: [Certificate] -> ShowS # |
buildOption :: Either FilePath String -> MiosProgramOption Source #
returns a MiosProgramOption for the target
buildSolver :: MiosProgramOption -> IO Solver Source #
returns a new solver injected a problem
buildDescription :: FilePath -> Solver -> IO CNFDescription Source #
returns the data on a given CNF file. Only solver knows it.
executeSolver :: MiosProgramOption -> Solver -> IO () Source #
executes a solver on the given 'arg :: MiosConfiguration'. This is another entry point for standalone programs.
executeValidator :: MiosProgramOption -> Solver -> IO () Source #
validates a given assignment for the problem (2nd arg). This is another entry point for standalone programs; see app/mios.hs.
Simple Interface
runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int]) Source #
NOT MAINTAINED NOW new top-level interface that returns:
- conflicting literal set :: Left [Int]
- satisfiable assignment :: Right [Int]
solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int] Source #
The easiest interface for Haskell programs.
This returns the result ::[[Int]]
for a given (CNFDescription, [[Int]])
.
The first argument target
can be build by Just target <- cnfFromFile targetfile
.
The second part of the first argument is a list of vector, which 0th element is the number of its real elements.
solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int] Source #
solves the problem (2rd arg) under the configuration (1st arg). and returns an assignment as list of literals :: Int.
showAnswerFromString :: String -> IO String Source #
executes a solver on the given 'arg :: MiosConfiguration'. This is another entry point for standalone programs.
Assignment Validator
validate :: Traversable t => Solver -> t Int -> IO Bool Source #
validates the assignment even if the implementation of Solver
is wrong; we re-implement some functions here.
validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool Source #
File IO
dumpAssigmentAsCNF :: MiosProgramOption -> Certificate -> IO String Source #
FIXME: swtich to DRAT
dumps an assigment to file. 2nd arg is
True
if the assigment is satisfiable assigmentFalse
if not
>>>
do y <- solve s ... ; dumpAssigmentAsCNF (Just "result.cnf") y <$> model s