SAT.Mios

Minisat-based Implementation and Optimization Study on SAT solver

Interface to the core of solver

versionId :: String

version name

data CNFDescription

misc information on CNF

Constructors

CNFDescription

Fields

• _numberOfVariables :: !Int

  number of variables

• _numberOfClauses :: !Int

  number of clauses

• _pathname :: Maybe FilePath

  given filename

Instances

Eq CNFDescription

Methods

(==) :: CNFDescription -> CNFDescription -> Bool

(/=) :: CNFDescription -> CNFDescription -> Bool

Ord CNFDescription

Methods

compare :: CNFDescription -> CNFDescription -> Ordering

(<) :: CNFDescription -> CNFDescription -> Bool

(<=) :: CNFDescription -> CNFDescription -> Bool

(>) :: CNFDescription -> CNFDescription -> Bool

(>=) :: CNFDescription -> CNFDescription -> Bool

max :: CNFDescription -> CNFDescription -> CNFDescription

min :: CNFDescription -> CNFDescription -> CNFDescription

Show CNFDescription

Methods

showsPrec :: Int -> CNFDescription -> ShowS

show :: CNFDescription -> String

showList :: [CNFDescription] -> ShowS

module SAT.Mios.OptionParser

runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int])

new top-level interface that returns

• conflicting literal set :: Left [Int]
• satisfiable assignment :: Right [Int]

solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]

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]

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 Bool

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.

getModel :: Solver -> IO [Int]

return the model as a list of literal

Assignment Validator

validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool

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

validate :: Traversable t => Solver -> t Int -> IO Bool

validates the assignment even if the implementation of Solver is wrong; we re-implement some functions here.

For standalone programs

executeSolverOn :: FilePath -> IO ()

executes a solver on the given CNF file This is the simplest entry to standalone programs; not for Haskell programs

executeSolver :: MiosProgramOption -> IO ()

executes a solver on the given 'arg :: MiosConfiguration' | This is another entry point for standalone programs.

executeValidatorOn :: FilePath -> IO ()

validates a given assignment from STDIN for the CNF file (2nd arg) this is the entry point for standalone programs

executeValidator :: MiosProgramOption -> IO ()

validates a given assignment for the problem (2nd arg) this is another entry point for standalone programs; see app/mios.hs

File IO

dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO ()

dumps an assigment to file. 2nd arg is

• True if the assigment is satisfiable assigment
• False if not

>>> do y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s