NaPS (Nagoya Psudo-Boolean Solver)

NaPS and SCIP-NaPS are solvers for pseudo-Boolean constraints: linear constraints with Boolean variable.
NaPS has a maxsat mode (by option: -max-sat ), a model count mode (by option: -A), and a projected-count mode (by option: -AI)

Download

• NaPS and SCIP-NaPS: Source stable
• Version 1.02b (won at PB'16 competition in several categories: OPT-BIGINT-LIN, OPT-SMALLINT-LIN, PARTIAL-SMALLINT-LIN, and SOFT-SMALLINT-LIN)
  • Source codes on gitlab
  • Linux static linked 64bit binary   Windows binary (Cygwin 64bit)
• Version 1.01 (bug fixed version of 1.00)
  • Source codes on gitlab
  • Linux static linked 64bit binary
• Version 1.00 (submitted to PB evaluation 2015)
  • Source codes on gitlab
  • Linux static linked 64bit binary

Contributers

• Masahiko Sakai (Nagoya Univ.)
• Hidetomo Nabeshima (Univ. of Yamanashi)
• Naoki Nagatsuka (was in Nagoya Univ.)
• Harald Zankl (was in Univ. of Innsbruck)

Publications

• Masahiko Sakai and Hidetomo Nabeshima,
  Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers,
  IEICE Transaction on Information and Systems, Vol. E98-D, No. 6, pp. 1121-1127, Jun 2015.
  pdf file Copyright(C) 2015 IEICE, on line transaction