npSolver -- a SAT based solver for optimization problems
The performance of SAT solvers improved impressively in the last decade.
To utilize this power, many different encodings for PB constraints have been developed.
In 2006, MiniSat+ combined three of these encodings to a PB solver.
Since that time, new encodings have been proposed.
We recently implemented npSolver, a pseudo-Boolean (PB) solver that translates PB to SAT similar to MiniSat+, but which incorporates novel techniques.
The used SAT solver can be exchanged, enabling the usage of most recent and even parallel systems.
To keep learned clauses and avoid re-encodings, we also provide incremental solving of optimization instances.
The search for the optimum supports simple bounding, binary search and a novel approximation technique.
Besides the encodings for general PB constraints we furthermore provide special encodings for cardinality constraints.
The solver is still in an early stage of research.
The source code of the current stage is available here. If you have any problems with the tools, please report them to Norbert Manthey or Peter Steinke.
Usage of the PB solver
In this section a brief overview of the usage for the solver is given to enable a quick and easy start with the tool.
How to get the solver? Follow this link download and extract the tar ball.
How to get the source code? Follow this link download and extract the tar ball.
How to use the tool for solving PB? To run the solver type ./npSolver-pbo INSTANCE TMPDIR.
How can I force an encoding? To use the SWC encoding, type ./npSolver-pbo INSTANCE TMPDIR -justSWC. To force using BDDs only, type ./npSolver-pbo.sh INSTANCE TMPDIR -justBDD
How do I enable the preprocessor? Add the parameter -useCP2=1 and type ./npSolver-pbo INSTANCE TMPDIR -useCP2=1
How do I use the incremental version? The incremental solver is used by running ./npSolver-pbo INSTANCE TMPDIR -useInc=1. Note, that you have to store the binary of glucosInc in the directory of the solver. Currently, the call to this binary is fixed in the source code.
We executed the default configuration of npSolver on all SMALLINT instances of the last two PB competitions. It can be seen that npSolver solves more instances than bsolo within the timeout of 1800 seconds.