Differences

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

Link to this comparison view

lbx [2016/11/17 16:08] (current)
ajrm created
Line 1: Line 1:
  
 +====== Literal-Based eXtractor (LBX) ======
 +
 +==== Description ====
 +
 +LBX [1] is a tool for the extraction of Minimal Correction Subsets (MCSes) of unsatisfiable CNF formulas. It also allows for enumerating MCSes, as well as approximating MaxSAT by selective MCS enumeration.
 +
 +
 +==== Distribution ====
 +
 +A Linux (64-bit) executable can be downloaded here: {{:​lbx.tar.gz|lbx.tar.gz}}
 +
 +
 +==== Benchmarks ====
 +
 +The problem instances used in the experiments in [1] can be downloaded from the following links: ​
 +
 +   * [[http://​logos.ucd.ie/​Drops/​ijcai13-bench.tgz|ijcai13-bench.tgz]] (~1.8 GByte)
 +   * [[http://​logos.ucd.ie/​Drops/​ijcai15-mus-bench.tgz|mus-bench.tgz]] (~474 MByte)
 +   * [[http://​logos.ucd.ie/​Drops/​ijcai15-maxsat-bench.tgz|maxsat-bench.tgz]] (~629 MByte)
 +
 +
 +
 +
 +==== References ====
 +[1] Carlos Mencía, Alessandro Previti and Joao Marques-Silva. Literal-Based MCS Extraction. IJCAI 2015
Print/export