This is an old revision of the document!

Research Software

This page list the software tools developed by Reason Lab members, some in collaboration. The page topics includes more information about the problems solved by these tools.


  • Hyper and Hyper* : Implicit Hitting Set solvers for the Propositional Abduction problem
  • MSCG: state of the art MaxSAT solver
  • PySAT: a Python toolkit for Prototyping with SAT oracles

Legacy Software

The following list refers to research software that was developed by Reason Lab members (or with their input) and is no longer maintained.

  • BBones: tool for backbone computation
  • Bica: formula simplification tool (a replacement of Quine-McCluskey)
  • cmMUS: MUS-membership solver
  • DOE : MaxSAT encoding for model based diagnosis
  • Forqes: Smallest MUS extractor
  • EL2MCS: axiom pinpointing for the EL+ DL
  • EL2MUS: state of the art axiom pinpointing tool for the EL+ DL
  • eMUS : partial MUS enumerator
  • GRASP: the original CDCL SAT solver
  • HgMUS : efficient MUS Enumeration of Horn Formulae, with application to axiom pinpointing
  • LBX: another state of the art MCS extractor & enumerator
  • MARCO : recent partial MUS enumerator
  • MCSls: MCS extractor & enumerator
  • mcsXL: state of the art MCS extractor & enumerator
  • minibones: state of the art backbone computation tool
  • MinUC: minimum unsatisfiable core finder
  • MSUnCore: MaxSAT solver
  • MUS checkers: utilities for testing/verifying various MUSes
  • MUSer: MUS extractor
  • nc-MUSer: circuit MUS (gate- and wire-based) extractor
  • PackUp: framework for package upgradability solving
  • PackUpHyb: hybrid package upgradability solving
  • primer : A prime implicants/implicates enumerator
  • RAReQS: recursive abstraction refinement QBF solver
  • RPoly: state of the art haplotyping tool
  • SHIPs: SAT-Based haplotype inference
  • STEP: Satisfiability-based funcTion dEcomPosition system
  • TG-PRO: SAT-based ATPG system