Mios
is yet another minisat-based SAT solver implementation in Haskell, as
a part of my research theme.
IO
monad, uses Data.Primitive.ByteArray
mainly and reallyUnsafePtrEquality
.default-extensions
from mios.cabal, you can use ghc-7.10.x.)git clone https://github.com/shnarazk/mios
stack init --resolver lts-11.X # for ghc-8.2.X
stack install
Mios is registered in hackage now.
cabal install mios
$ mios a.cnf
an assignment :: [Int]
$ mios --help
mios 1.6.1 https://github.com/shnarazk/mios/
Usage: mios [OPTIONS] target.cnf
-d 0.95 --variable-decay-rate=0.95 [solver] variable activity decay rate (0.0 - 1.0)
-c 0.999 --clause-decay-rate=0.999 [solver] clause activity decay rate (0.0 - 1.0)
--Rb=1.2 [solver] expansion rate for blocking restart (>= 1.0)
--Rf=1.01 [solver] expansion rate for forcing restart (>= 1.0)
--Rs=100.0 [solver] a fixed number of conflicts between restarts
-: --validate-assignment [solver] read an assignment from STDIN and validate it
--validate [solver] self-check (satisfiable) assignment
-o file --output=file [option] filename to store result
-v --verbose [option] display misc information
-X --hide-solution [option] hide solution
--benchmark=-1/0/N [devel] No/Exhaustive/N-second timeout benchmark
--sequence=NUM [devel] set 2nd field of a CSV generated by benchmark
--dump=0 [devel] dump level; 1:solved, 2:reduction, 3:restart
-h --help [misc] display this message
--version [misc] display program ID
If you have GNU parallel, Mios works well with it:
parallel "mios --benchmark=0 --sequence={#} -o {.cnf}.result {}" ::: *.cnf
module Main where -- this is sample.hs in app/
import SAT.Mios (CNFDescription (..), solveSAT)
clauses = [[1, 2], [1, 3], [-1, -2], [1, -2, 3], [-3]] :: [[Int]]
desc = CNFDescription 3 5 Nothing -- #vars, #clauses, Just pathname or Nothing
main = do
asg <- solveSAT desc clauses -- solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]
putStrLn $ if null asg then "unsatisfiable" else show asg
$ stack ghc app/sample.hs
$ app/sample
[1,-2,-3]
Of course, you can use Mios in ghci similarly.
$ stack ghci
...>