Research Topics

This page lists several research topics on which Reason Lab member's are working on (or have worked on), as well as tools developed on the topic. For more information on the topic please follow the respective link.

  • Minimal Unsatisfiable Subsets (MUSes)
    • MUSer: MUS extractor (legacy)
    • MUS checkers: utilities for testing/verifying various MUSes (legacy)
    • nc-MUSer: circuit MUS (gate- and wire-based) extractor (legacy)
  • Minimal Correction Subsets (MCSes)
    • mcsXL: state of the art MCS extractor & enumerator (legacy)
    • LBX: another state of the art MCS extractor & enumerator (legacy)
    • MCSls: MCS extractor & enumerator (legacy)
  • Backbones
    • minibones: state of the art backbone computation tool (legacy)
    • BBones: tool for backbone computation (legacy)
  • Axiom Pinpointing
    • EL2MUS: state of the art axiom pinpointing tool for the EL+ DL (legacy)
    • EL2MCS: axiom pinpointing for the EL+ DL (legacy)
  • Model Based Diagnosis (MBD)
    • DOE : MaxSAT encoding for model based diagnosis (legacy)
  • Enumeration / Compilation Problems
    • HgMUS : efficient MUS Enumeration of Horn Formulae, with application to axiom pinpointing (legacy)
    • eMUS : partial MUS enumerator (legacy)
    • MARCO : recent partial MUS enumerator (legacy)
    • primer : A prime implicants/implicates enumerator (legacy)
  • Quantification
    • RAReQS: recursive abstraction refinement QBF solver (legacy)
    • MinUC: minimum unsatisfiable core finder (legacy)
    • Forqes: Smallest MUS extractor (legacy)
    • cmMUS: MUS-membership solver (legacy)
  • Package Management
    • PackUp: framework for package upgradability solving (legacy)
    • PackUpHyb: hybrid package upgradability solving (legacy)
  • Formula Simplification
    • Bica: formula simplification tool (a replacement of Quine-McCluskey) (legacy)
  • Haplotyping
    • RPoly: state of the art haplotyping tool (legacy)
    • SHIPs: SAT-Based haplotype inference (legacy)
  • Function Decomposition
    • STEP: Satisfiability-based funcTion dEcomPosition system (legacy)
  • Test Pattern Generation
    • TG-PRO: SAT-based ATPG system (legacy)
  • Boolean Satisfiability (for reference purposes)
Print/export