# 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)