LBX-cache

A minimal correction subset (MCS) enumerator using premise set caching

LBX-cache is developed by the Constraint Optimization and Reasoning Group at the Department of Computer Science, University of Helsinki. The system is implemented by Alessandro Previti.

About

LBX-cache is a tool for enumerating MCSes implementing the ideas presented in [1]. The tool reimplements the LBX algorithm extended with a caching mechanism for premise sets.

USAGE

    USAGE: ./lbx-cache [options] <input-file>

    where input may be either in plain or gzipped DIMACS.
    
    OPTIONS:
    
    -print_num_mcs, -no-print_num_mcs (default: off) # When on the number of MCSes computed so far is printed every 5 seconds
    -print_mcs, -no-print_mcs         (default: off) # When on MCSes are printed to the screen during enumeration
    -cache, -no-cache                 (default: on)  # When on the cache is used

    -mem-lim      =   [   0 .. imax] (default: 0) # Used to limit the memory usage
    -cpu-lim      =   [   0 .. imax] (default: 0) # Used to limit the CPU usage

    --help        # Print help message

Downloads

The latest version of LBX-cache is available for download here.

References

[1] Premise Set Caching for Enumerating Minimal Correction Subsets.
Alessandro Previti, Carlos Mencia, Matti Järvisalo, and Joao Marques-Silva.
In ???, editors, Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pages ????-????. AAAI Press, 2018.
[pdf] [abstract/bibtex]