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

Benchmarks

The problem instances used in the experiments in [1] can be downloaded from the following links:

References

[1] Carlos Mencía, Alessandro Previti and Joao Marques-Silva. Literal-Based MCS Extraction. IJCAI 2015

Print/export