All Versions
20
Latest Version
Avg Release Cycle
100 days
Latest Release
-

Changelog History
Page 2

  • v1.4.0 Changes

    September 13, 2016
    • 🆕 new classes and methods

  • v1.3.0 Changes

    September 01, 2016
    • replace LBD heuristics with a simpler metrics, inspired by S. Jabbour et al.: “Revisiting the Learned Clauses Database Reduction Strategies,” 2013.
    • 🔄 change the module structure

  • v1.2.1 Changes

    July 21, 2016
    • tiny changes for uploading to hackage
    • ➕ add a CNF handling library under 'SAT.Util'

    Note: Mios requires optimization flag -O2; it's crucial.

  • v1.2.0 Changes

    • use blocking literals
    • implement literal block distance (LBD) (not tested well)
    • revise reduceDB
    • 👉 use phase-saving
    • ✂ remove random literal selection
    • ✂ remove 'Criterion' from dependency list

  • v1.1.2 Changes

    • 🛠 fix a bug in DIMACS CNF parser; only single space between literals was accepted

    This would be the last version based on MiniSat 1.14.

  • v1.1.1 Changes

    • tiny changes on the output format
    • tiny changes on random variable decision rate
    • ⚡️ update REDAME.md with a figure on a benchmark run sequentially; the old ones were multi-threaded and got very inaccurate numbers.

  • v1.1.0 Changes

    • Based on MiniSat 1.14, but lacks the binary clause implementation so far.
    • The arguments of solveSATand validateAssignment were curried.
    • Solver holds a literal set internally in the case of contradiction.
    • literals are encoded to positive integers
    • 🔀 no more queue; propQ was merged to trail
    • ➕ added a simple pre-processor
    • 📜 a new CNF DIMACS parser
    • solutions can be saved to a file with --output option

  • v1.0.3 Changes

    • 👉 uses vector-based containers instead of pointer-based clause containers
    • ➕ adds self-checking option (--validate), which works only on satisfiable problems
    • stack install installs mios. stack install --flag mios:devel installs mios-1.0.3 for developers.

    This is the last version based on “An extensible SAT-solver [extended version 1.2].”

  • v1.0.2 Changes

    • 🛠 fixes a bug on CNF reader at 1.0.1

  • v1.0.1 Changes

    • CNF reader was changed from a parser based on 'Parsec' to a simple reader based on Data.ByteString.Char8.readInt
    • 👉 uses a true sortOnActivity implementation
    • phase saving
    • 👀 provides assignment validation mode (see below)
    $ mios test/data/uf200-012.cnf | mios -: test/data/uf200-012.cnf      # `-:` is the option for validation.
It's a valid assignment.
$ echo "[1,2,-3,4,-5]" | mios -: test/data/uf200-012.cnf
It's an invalid assignment.