# PBO-IHS

### Pseudo-Boolean optimization (PBO) solver that utilizes the implicit hitting set (IHS) approach

## Dependencies

- Python version >= 3.6.9
- pybind11 version >= 2.5.0
- GCC version >= 8.4.0
- CPLEX version >= 12.8
- C++17 (i.e., a reasonably recent compiler)
- Boost library: https://www.boost.org
- Optionally: SoPlex LP solver: https://soplex.zib.de/download.php?fname=soplex-5.0.1.tgz

### Following libraries are only necessary to enable abstract cores
- Louvain community python library: https://github.com/taynaud/python-louvain
- NetworkX version >= 2.5: https://networkx.org/documentation/stable/install.html

## How to set up

PBO-IHS algorithm is implemented as solver/pbhs.py python script.

The python script depends on two libraries that need to be compiled by the user: **ihssolver** and **roundingsat** (modified from https://gitlab.com/MIAOresearch/roundingsat)

### ihssolver
- cd solver/ihssolver
- Open compile.sh in text editor
- Make sure that CPLEXDIR, CONCERTDIR, CPLEXLIBDIR, CONCERTLIBDIR variables point to appropriate CPLEX directories in your system.
- Change file paths if needed and save changes
- chmod u+x compile.sh
- ./compile.sh
- mv ihssolver.cpython-36m-x86_64-linux-gnu.so ..
- Notice that ihssolver library file may have a different suffix

### roundingsat
- cd solver/roundingsat
- Follow instructions in solver/roundingsat/README.md file, chapter Compilation
  - Alternatively follow instructions in chapter SoPlex if you want to utilise the LP relaxation feature
- mv roundingsat.cpython-36m-x86_64-linux-gnu.so ..
- Notice that roundingsat library file may have a different suffix

Once both ihssolver.cpython-36m-x86_64-linux-gnu.so and roundingsat.cpython-36m-x86_64-linux-gnu.so are placed in the same directory as pbhs.py,
the pbhs.py script can be executed.

## Usage

    ./pbhs.py [-h] [--optimalhs {0,1,2}] [--shuffles [0-1000]]
           [--usedcores [1-1000]] [--mincore {0,1,2}] [--nohsrc] [--pbrc]
           [--nounitcorefix] [--noseed] [--nowce] [--alths] [--fliplits]
           [--clearlearnts] [--abs #abs]
           xxx.opb

or to run in default configuration:

    ./pbhs.py xxx.opb

xxx.opb is a PBO instance encoded into .opb file format.

PBO-IHS currently only supports .opb files, as described in solver/roundingsat/InputFormats.md

###Optional arguments

-  `-h`, `--help`
    show the help message and exit
-  `--optimalhs`
    - 0 - always optimal hs
    - 1 - always non-optimal hs
    - 2 - always non-optimal hs except when non-optimal hs returns SAT (default)
-  `--shuffles` [0-1000]
    Number of times assumption set is shuffled for each core extraction call (default: 20)
-  `--usedcores` [1-1000]
    From at most #shuffles number of cores, #usedcores smallest cores are added to the hs solver (default: 1)
-  `--mincore`
    Use subset minimization algorithm to minimize cores
    - 0 - do not minimize cores (default)
    - 1 - minimization algorithm 1
    - 2 - minimization algorithm 2
-  `--nohsrc`
    Disable reduced cost fixing based on MCHS LP
-  `--pbrc`
    Disable reduced cost fixing based on PBO LP
-  `--nounitcorefix`
    Disable variable fixing based on unit cores
-  `--noseed`
    Disable constraint seeding
-  `--nowce`
    Disable WCE during disjoint phase
-  `--alths`
    Alternative way of using a hitting set as an assumption set
-  `--fliplits`
    Transform PBO instance so all literals in the objective function have non-negative coefficients
-  `--clearlearnts`
    Clear learnt clauses from the memory on the PB solver after each disjoint phase
-  `--abs`
    Abstract cores are extracted after LB has not increased in #abs iterations. Disables abstract core extraction if #abs <= 0 (default: -1)