a SAT solver in javascript

• DPLL algorithm
• two-watched-literals
• very simple CDCL (only one clause from every conflict)

todo:

• how to choose the two watch literals? prefer uncommon vars?
• CDCL resolvent can be one single literal, simplify again. (that's a very useful case!)
• decision variable heuristic
• measure usefulness of the learn clauses, drop the least useful