1. 07 Oct, 2018 3 commits
  2. 17 Jun, 2018 1 commit
    • shuji narazaki's avatar
      Mios version 1.6.1 (#71) · 1051b1ef
      shuji narazaki authored
      - Better benchmarking
      - Introduce new algorithms: 
        - ACIDS #79 
        - An EMA-based restart heuristics #72 
        - A new clause scoring scheme #76 
      - The clause sorter doesn't allocate a temporal vector #84 
      - Set a maximum heap size as a terminating trigger (default: 7GB)   
      1051b1ef
  3. 16 Jun, 2018 2 commits
  4. 20 Dec, 2017 1 commit
  5. 17 Dec, 2017 1 commit
  6. 13 Dec, 2017 1 commit
    • shuji narazaki's avatar
      mios version 1.5.3 (#61) · b11e2104
      shuji narazaki authored
      - implement EMA based Glucose heuristics (Biere 2015) #62 
      - implement two-phase restart
      - 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 search result #64
      - learnt clause simplification uses 64-bit computation
      b11e2104
  7. 24 Nov, 2017 2 commits
    • shuji narazaki's avatar
      mios version 1.5.2 · db9d637a
      shuji narazaki authored
      - add options for benchmark, using a timeout thread (#56)
      db9d637a
    • shuji narazaki's avatar
      mios version 1.5.1 · 106ba8af
      shuji narazaki authored
      * fix a bug in simplifyDB (#52)
      * revise VARUPDATEACTIVITY (#52)
      * revise blockers (#53)
      * refactor mios.cabal (#47)
      106ba8af
  8. 23 Oct, 2017 1 commit
    • shnarazk's avatar
      update README.md · e8ba0e62
      shnarazk authored
      - capitalize 'mios'
      - withdraw a doubtful cactus plot.
      e8ba0e62
  9. 21 Oct, 2017 2 commits
  10. 29 Aug, 2017 1 commit
    • shuji narazaki's avatar
      mios version 1.4.1 · 6cb753e7
      shuji narazaki authored
      A maintenance release:
       - use ByteArray; no performance boost
       - add a copy of a branch: MultiConflict
      6cb753e7
  11. 13 Sep, 2016 1 commit
  12. 01 Sep, 2016 1 commit
  13. 28 Jun, 2016 1 commit
    • shuji narazaki's avatar
      mios version 1.2.0 (#18) · 41b10b36
      shuji narazaki authored
      mios version 1.2.0
      
      * 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
      41b10b36
  14. 12 Apr, 2016 1 commit
  15. 09 Apr, 2016 1 commit
  16. 07 Apr, 2016 1 commit
    • shnarazk's avatar
      mios version 1.1.1 · f0c14275
      shnarazk authored
      * tiny changes on `randomDecisionRate`; the default value is zero
      f0c14275
  17. 31 Mar, 2016 1 commit
    • shnarazk's avatar
      mios version 1.1.0 · 5481c229
      shnarazk authored
       * This version is based on MiniSat-1.14
      
       * new option `--stat` to show misc statistics
       * new option `--time`to show execution time
       * new option `--output` to save results
       * new option '--validate' to verify answer
      
       * new function `getModel`
       * new function `unsafeAssume`
       * new function `asVec` to `VectorFamily` class
       * new function `analyzeRemovable` and `analyzeFinal`
       * new DIMACS parser
       * new `Lit` coding
       * new type `LiftedBool`
      
       * `solveSAT` and `validateAssignment` were curried
       * uses bits operations
       * all fields are strict
       * no `varBumpActivity` on literals in new learnts
       * `propQ` was removed; use `trail` as stack and queue like MiniSat-1.14
      5481c229
  18. 03 Mar, 2016 1 commit
  19. 29 Feb, 2016 1 commit
    • shnarazk's avatar
      mios version 1.0.3 · d864ce77
      shnarazk authored
      * use vector-based clause containers
      * add `--validate` option to self-check (satisfied) answers
      d864ce77
  20. 20 Feb, 2016 1 commit
    • shnarazk's avatar
      mios version 1.0.2 · 16bbc902
      shnarazk authored
      * fix a bug in DIMACS CNF reader
      * validator checks an empty assignment
      * internal cleanup and refactoring
      16bbc902
  21. 28 Jan, 2016 1 commit
    • NARAZAKI, Shuji's avatar
      mios version 1.0.1 · dcf0740d
      NARAZAKI, Shuji authored
      * no more parsec
      * `sortOnActivity`
      * assignment validator
      * new interface
      * phase saving
      * add a missing pattern to `reduceDB`
      dcf0740d
  22. 12 Jan, 2016 2 commits
    • shnarazk's avatar
      mios version 1.0 · c0aaf9fc
      shnarazk authored
      * update 'versionId' (renamed from idString)
      * add a sample for Haskell programmers
      c0aaf9fc
    • shnarazk's avatar
      mios version 1.0 RC3 · 5d3161db
      shnarazk authored
      * add `randomDecisionRate :: Int ` to `MiosConfiguration`
      * add `config :: MiosConfiguration` to `Solver`
      * add '--random-decision-rate' otion
      * fix a wrong initial value of `claInc` in `Solver` (though this causes a performance regression)
      5d3161db
  23. 11 Jan, 2016 6 commits
    • shnarazk's avatar
      mios version 1.0 RC2 · 437f5de2
      shnarazk authored and NARAZAKI, Shuji's avatar NARAZAKI, Shuji committed
      * add codes used in benchmark
      * activate command options for decay parameters
      437f5de2
    • shnarazk's avatar
      mios version 1.0 RC1 · 872d248b
      shnarazk authored and NARAZAKI, Shuji's avatar NARAZAKI, Shuji committed
       * micro tuning on inlining
       * +.gitignore, +stack.yaml
       * add `IntSingleton`, `ClausePointer`
       * parser uses strict data
      872d248b
    • shnarazk's avatar
      mios verision 0.9 (rebased) · b5ccdd9f
      shnarazk authored and NARAZAKI, Shuji's avatar NARAZAKI, Shuji committed
      20ca17e * tiny refactoring and tuning
      5b682bd * reverted the restart period to 100, which is used in the paper
      c823738 * move sih4.cabal to mios.cabal
      5bf77f6 * tiny refactoring and tuning
      d09142e * bumped to mios 0.9
      861dd56 * fix `reduceDB` based on the paper and version 1.14
      f374f8f * HeapVar controlled by useHeap and useRand
      91ae34a * [WIP] `VarHeap` works but becomes slow
      afd0c54 * embed `VarOrderHeap` into Solver.hs
      ff661a5 * VarOrderHeap works
      04ab767 * [WIP] under debugging  VarOrderHeap.hs
      15b2d16 * [WIP] update VarOrderHeap.hs
      921e525 * [WIP] implementing heap
      7b485cd * + VarOrderHeap.hs
      5b682bd * reverted the restart period to 100, which is used in the paper
      
      update help messages
      
      add README.md
      b5ccdd9f
    • shnarazk's avatar
      mios version 0.8 · 1f217530
      shnarazk authored and NARAZAKI, Shuji's avatar NARAZAKI, Shuji committed
       * 3389bad updated exposed-modules
       * 160521f [this is the final preparation for 0.8] simplified imports
       * 9d3ee63 added strictness to `Solver.loop`
       * f57b76c changed the type of `trail` to `ListOfInt` from `StackOfBoundedInt`
       * db48602 CSE merge, more strictness in `analyze`
       * f1e5186 + ListOfInt; use it for `Solver.trailLim`
       * 7b10184 reverted to b16186e and anded the the changes on calcReason:
       * 72215b6 Merge branch 'WIP-mios' of github.com:shnarazk/sih4 into WIP-mios
       * 0561258 misc trials
       * 0aa9624 changed the hack on litsInLearnt into one-liner
       * eada420 deleted `clear` class method from ContainerLike
       * 0eddd4d comment out `calcReason`
       * 80e9a24 made hand fusion on analyze to eliminate calcReason
       * d647f65 use `ListOf` instead of `VecOf`
       * 1ef3510 by the results of criterion; update enqueue, analyze,
       * 800bf9f delete old files
       * 51d48c8 criterion uses only uf200-012.cnf
       * ffe7fff update the cabal
       * 86234f6 deleted `VectorLike`; renamed VecOf to ListOf
       * 7305b47 deleted (.!), setAt from VectorLike
       * b16186e refactored `propagate`: add `currentWatch` to Solver, add `mergeWatcher`
       * 4d769e9 renamed to {Queue|Stack}OfBoundedInt
       * 7c4b6c6 deleted the last `setAt` from Slover.hs
       * 8ad0c02 don't call `newVar` any more (Mios.hs)
       * a0731e8 refactored on constructors on `VectorLike`
       * 3634e67 deleted `copyTo`, `moveTo` and `checkConsistency` from `VectorLike`
       * 337ca35 deleted `lastE` and `removeElem` from `VectorLike`
       * 7203474 deleted push/pop from `VectorLike`
       * 35c550f deleted all size operations from `VectorLike`
       * 9b72fc1 various de-polymorphic optimization + misc refactoring
       * 4d9e678 delete obsolete codes
       * 1759058 use an explict loop in `setClauseActivities`
       * 0db21da `WatcherList` changed to immutable
       * 6fca30a newClause accepts `SizedVecInt` instead of `VecOf Int`; use more unsafe functions
       * 1054743 add addClause' to add better interface from reader to solver
       * 896d434 add `WatcherList` and `push'` for `VecOf Int`
       * ac08dc6 add interfaces for literals in clause
       * 84b7141 more de-polymoprhism, +FixedQueueInt.hs, StackOfLit -> StackOfInt
       * ef5b2e3 Merge branch 'WIP-mios' of https://this.is-saved.org/rep/sih into WIP-mios
       * 67e1093 use `-funfolding-use-threshold=200` again
       * cd64f5d add sih4-wip-prof target (sih.cabal)
       * 0a0bd71 delete dead codes
       * 4bd1b1a implemented ClauseLink
       * 186ffd4 de-polymorphism; +newClauseFromVec
       * ff4a492 set `-funfolding-use-threshold=50`
       * 9f1ba08 update library
      1f217530
    • shnarazk's avatar
      mios version 0.7 · 4bd2c82e
      shnarazk authored and NARAZAKI, Shuji's avatar NARAZAKI, Shuji committed
       * 6a0b259 changed to unsafeRead/Write and newtype
       * 71906f5 add INLINE
       * ec42786 add `swapVecInt` to FixedVecInt.hs
       * ce978ea mios uses a derived version of DIMACSReader.hs
       * 0552e9c reduced export/import symbols
       * 901b62a add more `-fno-warn-tabs` (sih.cabal)
       * a95a8df refactored `reduceDB`
       * c0edd61 use point-free style in `sortVecClause`
       * 7cef31a delete implementation/V07.hs
       * 229de5f fix performance on structured problems (closed #41)
       * 9efcafa WIP: debug for the un-terminating strict-bmc-ibm-10.cnf
       * 73532af add default-language
       * ff321ab add benchmark section using criterion
       * 30600a6 refactoring top-level interface
       * 5247e2c update SPECIALIZE pragmas
       * 0b923d3 rename FixedLitVec to FixedVecInt
       * c4edf84 divided Implementations
       * 5e0ade4 mios-0.7: add `VecOfClause`, `fixedUVecOf`
       * 00ccbda mios-0.7:  refactored `WatchList`
      4bd2c82e
    • shnarazk's avatar
      mios version 0.6 · a5293605
      shnarazk authored and NARAZAKI, Shuji's avatar NARAZAKI, Shuji committed
      * d14594a start mios-0.6; set the initial value for `varInc`; use `activities` in `select`
      * aef0cbb mios 0.6; set varInc
      * b212882 add sortVecOn for `sortOnActivity
      * 5ccafcc unsafe selectWatcher
      * edef342 mios 0.6: fix id string
      * 2ff67be changed to unsafeRead/Write
      * f96f175 fix bugs about reduceDB
      * 6cc5c67 micro tunings
      * afe7a44 fixed a bug on structured problems  that include a satisifed clause
      * f3a16a9 optimized `ghc-options` for ghc-7.10.2 (sih.cabal)
      
      mios 0.6; set varInc
      
      add sortVecOn for `sortOnActivity
      
      unsafe selectWatcher
      
      mios 0.6: fix id string
      
      changed to unsafeRead/Write
      
      fix bugs about reduceDB
      
      micro tunings
      
      fixed a bug on structured problems  that include a satisifed clause
      
      optimized `ghc-options` for ghc-7.10.2 (sih.cabal)
      a5293605
  24. 14 Dec, 2015 3 commits
    • shnarazk's avatar
      mios version 0.5 · fb66b938
      shnarazk authored
        * 760144c: add `StackOfLit` to resolve #32
        * baf989f: renamed to `FixedQueueOf`; closed #31
        * 864ddf3: delete `deleteWOEq`
        * 5e03bda: check queue implementation for mios 0.5
        * 0e108cb: fixed #26
        * e5b0c50: debug on locked
        * a797a03: WIP; under debug or reduce
        * f7c6aa5: this is slow with a full of garbage but seems to fix #26 completely up to 125vars
        * dd036b1: [WIP] might fixed a bug #26
        * a356d1c: changed to a much better occurrenceCheck
        * 5511b9b: fixed a bug by adding `occurrenceCheck` for propQ
        * 0fed32a: mios 0.5: used fixed vectors more
        * 35ce1c6: fix the bug on queue #19
        * 0760dca: implement ring based queue again
        * 62382bd: mios 0.5; fix #23
        * 942422d: modify codes on occurs in staticVarOrder
        * baa22d9: add shrink for Clause
        * 8640a2b: mios 0.5; made Clause shrinkable
        * bdf5bc1: mios 0.5; change the type of occurs, heat; update sortByFst
        * 67964c3: WIP; mios version 0.5: don't use UV.unsafe{Read,Write}, fix a bug
        * c198c2e: WIP; mios 0.5: change misc settings for eliminating strange bugs
        * 4559d5c: WIP; fixed a bug on `propagate` of upcoming mios version 0.5
        * 16631c1: [WIP] start the development of mios version 0.5
      
      WIP; mios 0.5; under debug
      
      [WIP] with logical bug
      
      $ mios-prof ~/SATbench/3-SAT/uf10.cnf  +RTS -xc
      setInternalState done
      addClause done
      simplifyDB done
      propagate : 1
      propagate : 2
      propagate : 3
      *** Exception (reporting due to +RTS -xc): (THUNK_1_0), stack trace:
        SAT.Solver.Mios.Solver.selectWatcher,
        called from SAT.Solver.Mios.Solver.nextWatcher,
        called from SAT.Solver.Mios.Solver.propagate,
        called from SAT.Solver.Mios.Solver.search,
        called from SAT.Solver.Mios.Solver.solve,
        called from Main.execute,
        called from Main.main
      mios-prof: no watcher(3,(-10,8),[-10,8,-1])
      
      [WIP] under development of  mios version 0.5
      
      [WIP] under heavy debugging of mios version 0.5
      
      WIP; fixed a bug on `propagate` of upcoming mios version 0.5
      
      WIP; mios 0.5: change misc settings for eliminating strange bugs
      
      mios 0.5; refactoring
      
      WIP; mios version 0.5: don't use UV.unsafe{Read,Write}, fix a bug
      
      mios 0.5; change the type of occurs, heat; update sortByFst
      
      revert a temporal setting in `cancel`
      
      mios 0.5; made Clause shrinkable
      
      add shrink for Clause
      
      modify codes on occurs in staticVarOrder
      
      WIP; mios 0.5
      
      mios 0.5; fix a bug.
      
      mios 0.5; fix #23
      
      implement ring based queue again
      
      fix the bug on queue #19
      
      mios 0.5: used fixed vectors more
      
      fixed a bug by adding `occurrenceCheck` for propQ
      
      changed to a much better occurrenceCheck
      
      debug; back to the version 0.1 of queue
      
      [WIP] might fixed a bug #26
      
      under debug
      
      this is slow with a full of garbage but seems to fix #26 completely up to 125vars
      
      WIP; under debug or reduce
      
      debug on locked
      
      fixed #26
      
      delete debug codes
      
      clean up for mios 0.5
      
      check queue implementation for mios 0.5
      
      1st preparation for mios 0.5 that works really
      
      delete `deleteWOEq`
      
      preparation for 0.5
      
      preparation for 0.5
      
      renamed to `FixedQueueOf`; closed #31
      
      add `StackOfLit` to resolve #32
      fb66b938
    • shnarazk's avatar
      mios version 0.4 · be0fa370
      shnarazk authored
      * add`FixedVecOf a`
      * add `FixedLitVector`
      * use UV.IOVector for `QueueOf` (because the queue in minisat is bounded)
      * executable for profiling
      * `QueueOf` is not an instance of `VectorLike`
      * use SAT.Solver.Mios.Internal to switch implementation
      * fixed wrong definitions in SAT.Solver.Mios.hs
      * add `OpitonParser.sh`
      * study real used methods
      be0fa370
    • NARAZAKI, Shuji's avatar
      initialize repository; mios-0.1 · e6fa800c
      NARAZAKI, Shuji authored
      mios (MINISAT Implementation On Sih4) version 0.1
      e6fa800c