features / todo list / ideas

• main solver
  • clause learning
    • UIP style
    • full resolution to one variable per level (default=off)
    • on-the-fly minimization of learnt clauses
    • lazy hyper-binary-resolution
  • branching heuristic
    • VSIDS
    • polarity saving
    • dominating-literal branching (default=off)
  • clause-cleaning heuristic
    • size
    • glue (computed once when learning)
    • glue (dynamicically adjusted during propagation)
    • activity
  • restart heuristic
    • linear
    • geometric
    • luby
    • dynamic
• preprocessing / inprocessing
  • top-level in-tree probing (including hyper-binary resolution)
  • subsumption / self-subsuming resolution (includes HTE)
  • vivification (more exhaustive than typical heuristics)
  • transitive reduction of binary clauses
  • disconnected components
  • strongly-connected-components
  • blocked-clause elimination
  • bounded variable elimination (preprocessing only)
  • bounded variable addition (default=off)
  • xor discovery and gaussian elimination
• data-structures
  • two-watch scheme
  • implicit binary clauses
  • implicit ternary clauses (and blocking literal)
  • packed long clauses with 32-bit references
  • small-vector optimization for binaries and watches
• other
  • unsat proofs
  • multithreading
  • interface for incremental problems