Monthly Downloads: 12
Programming language: Haskell
License: GNU General Public License v3.0 only
Latest version: v1.6.2

mios alternatives and similar packages

Based on the "Constraints" category.
Alternatively, view mios alternatives based on common mentions on social networks and blogs.

Do you think we are missing an alternative of mios or a related project?

Add another 'Constraints' Package


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

Cactus plot with Mios-1.6.1: SAT Competition 2017 main

> Install

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

> 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

Of course, you can use Mios in ghci similarly.

$ stack ghci