Skip to content

v1.3

Compare
Choose a tag to compare
@czengler czengler released this 01 Sep 10:04
· 565 commits to master since this release

Added

  • MiniSat and Glucose have a new option for proof tracing. A DRUP implementation stores all the necessary information for generating a proof for unsatisfiable
    formulas after
    solving them. The new method can be found in the SAT solver class: unsatCore()
  • A new simplifier which applies the distributive law was added: DistributiveSimplifier

Changed

  • Unsat Cores are now parametrized with the proposition type

Fixed

  • Some minor bug-fixes in handling corner cases of cardinality and pseudo-Boolean constraints