SAT.Mios

(This file is a part of 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 a CNF

Constructors

CNFDescription

Fields

• _numberOfVariables :: !Int

  the number of variables

• _numberOfClauses :: !Int

  the number of clauses

• _pathname :: !FilePath

  given filename

Instances

Eq CNFDescription

Defined in SAT.Mios.Types

Methods

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

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

Ord CNFDescription

Defined in SAT.Mios.Types

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

Read CNFDescription

Defined in SAT.Mios.Types

Methods

readsPrec :: Int -> ReadS CNFDescription

readList :: ReadS [CNFDescription]

readPrec :: ReadPrec CNFDescription

readListPrec :: ReadPrec [CNFDescription]

Show CNFDescription

Defined in SAT.Mios.Types

Methods

showsPrec :: Int -> CNFDescription -> ShowS

show :: CNFDescription -> String

showList :: [CNFDescription] -> ShowS

module SAT.Mios.OptionParser

Main Interace

type SolverResult = Either SolverException Certificate

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

terminate and find an SAT/UNSAT answer

Constructors

SAT [Int]

UNSAT [Int]

Instances

Eq Certificate

Defined in SAT.Mios.Types

Methods

(==) :: Certificate -> Certificate -> Bool

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

Ord Certificate

Defined in SAT.Mios.Types

Methods

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

Defined in SAT.Mios.Types

Methods

readsPrec :: Int -> ReadS Certificate

readList :: ReadS [Certificate]

readPrec :: ReadPrec Certificate

readListPrec :: ReadPrec [Certificate]

Show Certificate

Defined in SAT.Mios.Types

Methods

showsPrec :: Int -> Certificate -> ShowS

show :: Certificate -> String

showList :: [Certificate] -> ShowS

buildOption :: Either FilePath String -> MiosProgramOption

returns a MiosProgramOption for the target

buildSolver :: MiosProgramOption -> IO Solver

returns a new solver injected a problem

buildDescription :: FilePath -> Solver -> IO CNFDescription

returns the data on a given CNF file. Only solver knows it.

executeSolver :: MiosProgramOption -> Solver -> IO ()

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

executeValidator :: MiosProgramOption -> Solver -> IO ()

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])

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]

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.

showAnswerFromString :: String -> IO String

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

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

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

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