Avg Release Cycle
- Mios saves the assignment to a file automatically.
- 🛠 A bug on a CNF file containing conflicting unit clauses was fixed.
- Restart heuristics was modified slightly (not evaluated well).
- 👉 Use CPU clock time in benchmark mode correctly
- Introduce new algorithms:
- ACIDS (average conflict-index decision score); Armin Biere and Andreas Fröhlich, "Evaluating CDCL Variable Scoring Schemes", LCSN, vol.9340, pp.405-422, 2015.
- An EMA-based restart heuristics (not evaluated well; might be canceled in a future release)
- A new clause scoring scheme
- The clause sorter doesn't allocate a temporal vector
- 0️⃣ Set a maximum heap size as a terminating trigger (default: 7GB)
- switch to hpack
- 0️⃣ set a default memory limit in compile-time (fixed in 188.8.131.52)
v184.108.40.206June 18, 2018
- 'sortClauses' didn't use clause activity correctly and now uses 2 * Int64 layout.
- implement EMA based Glucose heuristics (Biere 2015) #62
- 🛠 fix a bug on learnt clause reduction in a marginal situation
- ⏱ thread-based timeout handling #58
- ⚡️ update command line options
- ⚡️ update the benchmark report format #64
- ➕ add a new type to represent a search result #64
- further adaptation to 64-bit CPU
- ➕ add options for benchmark, using a timeout thread
- 🛠 fix a bug in simplifyDB
- ⚡️ revise VARUPDATEACTIVITY (#52)
- revise blockers (#53)
- ♻️ refactor mios.cabal
- implement LBD
- misc micro tuning
- ➕ add some utilities
- switch to SAT Competition 2017 main track for benchmark
🚀 A maintenance release:
- 🐎 use
ByteArray; no performance boost.
- ➕ add a copy of a branch: MultiConflict.
- 🐎 use