A Minisat-based SAT solver in Haskell

Mios -- Minisat-based Implementation and Optimization Study

Mios is yet another minisat-based SAT solver implementation in Haskell, as a part of my research theme.

• [ChangeLog](ChangeLog.md)

> Features

• fundamentally it is developed based on Minisat-1.14 and 2.2.0.
  • Firstly, version 1.0 was based on N. Een and N. Sorensson, “An extensible SAT-solver [extended version 1.2],” in 6th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT2003), 2003, pp. 502–518.
  • Version 1.1 was a line-to-line translation of MiniSat 1.14.
  • Version 1.2 imported some idea used in Glucose 4.0.
  • Version 1.5 uses Literal Block Distance (LBD).
  • Version 1.6 adopts new ideas: EMA, ACIDS and so on.
• runs in IO monad, uses Data.Primitive.ByteArray mainly and reallyUnsafePtrEquality.
• very fast, compared with other SAT solvers written in Haskell; see below.

benchmark results

• SAT-Competition 2017 Main track, running 3 jobs in parallel with a 510 second timeout on Intel Core i7-3930K @ 12x 3.8GHz (Therefore results near the threshold should be affected by other threads more or less.)

> Install

Requirements

• ghc-8.0.1 or upper (By deleting default-extensions from mios.cabal, you can use ghc-7.10.x.)
• Stack
• If you want to build with cabal, please use the cabal file under utils directory.

Stack

git clone https://github.com/shnarazk/mios
stack init --resolver lts-11.X  # for ghc-8.2.X
stack install

Hackage/Cabal

Mios is registered in hackage now.

cabal install mios

> Usage

* As a standalone program

$ 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

* In Haskell

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
...>