Research Software

Software tools available for download, either developed by the SAT@UCD team members, or with the collaboration of UCD researchers:

Maximum Satisfiability (MaxSAT)

  • MSCG: state of the art MaxSAT solver

Minimal Unsatisfiable Subsets (MUSes)

  • MUSer: state of the art MUS extractor
  • nc-MUSer: circuit MUS (gate- and wire-based) extractor

Minimal Correction Subsets (MCSes)

  • mcsXL: state of the art MCS extractor & enumerator
  • LBX: another state of the art MCS extractor & enumerator
  • MCSls: MCS extractor & enumerator


  • minibones: state of the art backbone computation tool
  • BBones: tool for backbone computation

Axiom Pinpointing

  • EL2MUS: state of the art axiom pinpointing tool for the EL+ DL
  • EL2MCS: axiom pinpointing for the EL+ DL

Model Based Diagnosis (MBD)

  • DOE : MaxSAT encoding for model based diagnosis

Enumeration / Compilation Problems

  • HgMUS : efficient MUS Enumeration of Horn Formulae, with application to axiom pinpointing
  • eMUS : partial MUS enumerator
  • MARCO : recent partial MUS enumerator
  • primer : A prime implicants/implicates enumerator


  • RAReQS: recursive abstraction refinement QBF solver
  • MinUC: minimum unsatisfiable core finder
  • cmMUS: MUS-membership solver

Package Management

  • PackUp: framework for package upgradability solving

Formula Simplification

  • Bica: formula simplification tool (a replacement of Quine-McCluskey)

Other Tools

  • RPoly: state of the art haplotyping tool
  • SHIPs: SAT-Based haplotype inference
Function Decomposition
  • STEP: Satisfiability-based funcTion dEcomPosition system
Test Pattern Generation
Boolean Satisfiability (for reference purposes)
soft.txt · Last modified: 2017/09/21 07:47 by joao
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki