nc-MUSer - circuit-MUS extraction tool

Description

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

News

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

Distribution

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.

Documentation

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/smulov1bw08.aig

Benchmarks

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.

Contributors

Funding

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

Print/export