npSolver - a SAT based solver for optimization problems. The pseudo-Boolean (PB) solver npSolver encodes PB into SAT and solves the optimization instances by calling a SAT solver iteratively. The system supports MaxSAT, PB and WBO. Optimization instances are tackled by a greedy lower bound mechanism first. The solver can translate PB to SAT based on a portfolio of different encodings, based on the number of clauses. As back end of the system any SAT solver can be used, even incremental solvers for the optimization function. By using glucose as back end and the SAT simplifier Coprocessor, npSolver shows an outstanding performance on decision instances and can compete on optimization instances.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Philipp, Tobias; Steinke, Peter: PBLib -- a library for encoding pseudo-Boolean constraints into CNF (2015)