Differences

This shows you the differences between two versions of the page.

Link to this comparison view

nc-muser [2016/11/17 15:29] (current)
ajrm created
Line 1: Line 1:
 +====== 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 
 +  * Anton Belov, Joao Marques-Silva:​ {{:​papers:​ncmus-sat11.pdf| Minimally Unsatisfiable Boolean Circuits}}. SAT 2011. LNCS 6695, pp 145-158
 +
 +==== 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.belov|Anton]] in case of any questions or problems. ​  
 +
 +Download Linux and Mac OS X binaries {{:​tools:​ncmuser-proto-08072011.tgz|here}}.
 +==== Documentation ====
 +The instructions for using ''​ncmuser-proto''​ are available {{:​docs:​readme-ncmuser-proto.txt|here}}. The circuit-MUSes produced by the tool can be validated using the ''​[[muschk|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 {{:​benchmarks:​sat11-circuits.tgz|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 ====
 +  * [[anton.belov|Anton Belov]]
 +  * [[joao.marques-silva| Joao Marques-Silva]] (Principal Investigator)
 +
 +==== Funding ====
 +The research on circuit-based MUS extraction and the developement of nc-MUSer were partially supported by [[http://​www.sfi.ie/​ | Science Foundation Ireland]]
 +
 +{{:​images:​sfi.jpeg?​nolink&​200|}}
 +
  
Print/export