mios-1.6.2: A Minisat-based CDCL SAT solver in Haskell

Safe HaskellSafe




(This file is a part of MIOS.) Minisat-based Implementation and Optimization Study on SAT solver


Interface to the core of solver

versionId :: String Source #

version name

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

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 #

returns True if a given assignment (2nd arg) satisfies the problem (1st arg). if you want to check the answer which a slover returned, run solver validate answer, where validate :: Traversable t => Solver -> t Lit -> IO Bool.

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 assigment
  • False if not
>>> do y <- solve s ... ; dumpAssigmentAsCNF (Just "result.cnf") y <$> model s