Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
(This file is a part of MIOS.) Minisat-based Implementation and Optimization Study on SAT solver
- versionId :: String
- data CNFDescription = CNFDescription {}
- module SAT.Mios.OptionParser
- 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]
- solve :: Foldable t => Solver -> t Lit -> IO SolverResult
- type SolverResult = Either SolverException Certificate
- data Certificate
- validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool
- validate :: Traversable t => Solver -> t Int -> IO Bool
- executeSolverOn :: FilePath -> IO ()
- executeSolver :: MiosProgramOption -> IO ()
- executeValidatorOn :: FilePath -> IO ()
- executeValidator :: MiosProgramOption -> IO ()
- parseCNF :: Maybe FilePath -> IO (CNFDescription, ByteString)
- injectClausesFromCNF :: Solver -> CNFDescription -> ByteString -> IO ()
- dumpAssigmentAsCNF :: Maybe FilePath -> Certificate -> IO ()
Interface to the core of solver
data CNFDescription Source #
Misc information on a CNF
CNFDescription | |
|
module SAT.Mios.OptionParser
runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int]) Source #
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.
solve :: Foldable t => Solver -> t Lit -> IO SolverResult Source #
Fig. 16. (p.20) Main solve method.
Pre-condition: If assumptions are used, simplifyDB
must be
called right before using this method. If not, a top-level conflict (resulting in a
non-usable internal state) cannot be distinguished from a conflict under assumptions.
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
Assignment Validator
validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool Source #
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.
For standalone programs
executeSolverOn :: FilePath -> IO () Source #
executes a solver on the given CNF file. This is the simplest entry to standalone programs; not for Haskell programs.
executeSolver :: MiosProgramOption -> IO () Source #
executes a solver on the given 'arg :: MiosConfiguration'. This is another entry point for standalone programs.
executeValidatorOn :: FilePath -> IO () Source #
validates a given assignment from STDIN for the CNF file (2nd arg). this is the entry point for standalone programs.
executeValidator :: MiosProgramOption -> IO () Source #
validates a given assignment for the problem (2nd arg). This is another entry point for standalone programs; see app/mios.hs.
File IO
parseCNF :: Maybe FilePath -> IO (CNFDescription, ByteString) Source #
parses the header of a CNF file
injectClausesFromCNF :: Solver -> CNFDescription -> ByteString -> IO () Source #
parses ByteString then injects the clauses in it into a solver
dumpAssigmentAsCNF :: Maybe FilePath -> Certificate -> IO () Source #
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