nc-MUSer - circuit-MUS extraction tool


nc-MUSer is a tool for the computation of minimally unsatisfiable sub-circuits of Boolean circuits (circuit-MUSes). The theory behind the tool and the preliminary experimental results obtained using the prototype version of nc-MUSer (available on this page) are presented in


Jun 9, 2011: New wiki page published for nc-MUSer.


The prototype version of the tool, called ncmuser-proto is available for research and teaching purposes only. The current version was used for the experiments reported in SAT 2011 paper. Please not that this is a *prototype*, and, as such, not particularly user-friendly and likely to contain bugs. Please contact Anton in case of any questions or problems.

Download Linux and Mac OS X binaries here.


The instructions for using ncmuser-proto are available here. The circuit-MUSes produced by the tool can be validated using the cmuschk tool.

Example Usage

1. computation of a gate-MUS:

 ncmuser-proto td+rddm: incr ../examples/2pipe.iscas.gz  

2. computation of a wire-MUS:

 ncmuser-proto :bu+r incr ../examples/


Over 500 benchmark circuits are available in this archive. The benchmarks are described in the SAT 2011 paper. The .list files inside the archive specify various subsets of benchmarks: sat11-circuits.paper-subset.list and sat11-circuits.gatetests.list are the subsets used in the paper.



The research on circuit-based MUS extraction and the developement of nc-MUSer were partially supported by Science Foundation Ireland