TODO for 1.1 and 1.2

[shnarazk]

Though the purpose of 1.0 is to translate the codes in the paper (Eén, Niklas, and Niklas Sörensson. "An extensible SAT-solver." Theory and applications of satisfiability testing. Springer Berlin Heidelberg, 2003.) and some parts from MiniSat 1.14 into a program written in Haskell, I found there are a lot of differences between the paper and MiniSat 1.14; version 1.14 is not close to the paper but to MiniSat 2.2. It makes difficult to develop mios further; most part of the solver core should be updated. So stopping to improve the performance of the current mios 1.0.X based on the paper, I decided to switch the reference code to MiniSat 2.2 after the release of 1.0.3.

• mios 1.0 is a study on the paper.
• mios 1.1 is a study based on MiniSat 2.2. This is the current branch M22 and a one month sprint I hope.

It is a shorter way to archive an expected high-performance SAT solver in Haskell.

---

random note

• [x] reorder functions
• [ ] GClause for binary clauses
• [x] analyzeRemovable and 3 variables for analyze family
• [ ] current target is not simp but core
• [x] var heap is ready
• [ ] Luby is ready
• [ ] LBD is ready
• [x] write the output to a file in DIMACS CNF format

[shnarazk]

memo

• bit encoding for literal/var
• lightweight stack implementation
• change naming policy
• vector-based operations for Stack/Queue/Clause
• litRedundant
• now you can use mios in ghci
• single stack (no more propQ queue)

[shnarazk]