Popularity
7.6
Stable
Activity
0.0
Stable
34
4
3
Monthly Downloads: 23
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.
-
constraints-deriving
Programmatically create new instances using core-to-core plugins
Clean code begins in your IDE with SonarLint
Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today.
Promo
www.sonarlint.org
Do you think we are missing an alternative of mios or a related project?
Popular Comparisons
README
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, usesData.Primitive.ByteArray
mainly andreallyUnsafePtrEquality
. - 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
...>