PBSugar: A SAT-based Pseudo-Boolean Solver

PBSugar is a SAT-based Pseudo-Boolean (PB for short) solver. Given PB instance is encoded to a SAT instance, and solved by a SAT solver. Currently, PBSugar can solve problems of the DEC-SMALLINT-LIN (decision problems, small integers, linear constraints) category.

• pbsugar-v1-1-2.zip (version 1.1.2, released 2013-03-17 Sun)
• pbsugar-v1-1-1.zip (version 1.1.1, released 2013-02-14 Thu)
• pbsugar-v1-0-3.zip (version 1.0.3, released 2013-01-29 Tue)

• SAT solver (Glucose, GlueMiniSat, MiniSat, clasp, PrecoSAT, etc.)
• Java version 1.6 or higher
• Perl 5 or higher

1. Unzip the pbsugar-v1-1-2.zip file
2. Install with the following commands

   $ cd pbsugar-v1-1-2/bin
   $ make install
   

   • The pbsugar-v1-1-2.jar file will be installed to /usr/local/lib/pbsugar directory.
   • The pbsugar script file will be installed to /usr/local/bin directory.

• Exprimental Results for 669 instances of DEC-SMALLINT-LIN category of the 2011 PB Competition

$ pbsugar -solver glucose file.opb

• Please specify the command name of the SAT solver with -solver option.

pbsugar [ options ] opb_file
pbsugar [ options ] -n -sat file opb_file
pbsugar [ options ] -verify file opb_file

opb_file is the file name of a PB instance. It can be a gzipped (.gz) or bzipped (.bz2) file. The first line shows the usage of encoding and solving a PB instance. The second line is the usage of generating a CNF file from a PB instance. The third line is the usage of verifying the solution stored in the specified file for a PB instance.

• -h, -help : shows the help message
• -version : shows the version of PBSugar
• -v, -verbose : specifies verbose output mode
• -vv, -veryverbose : specifies very verbose output mode
• -solver command : specifies the command name of the SAT solver to be used (default glucose21_simp)
• -verify file : specifies the name of PBSugar's output file to be verified
• -o options, -option options : specifies the encoding options (multiple options should be connected with comma)
  • sort=n : do not sort terms
  • sort=l : sort terms by literal names
  • sort=a : sort terms with the ascending order of coefficients
  • sort=d : sort terms with the descending order of coefficients (this is the default)
  • no_clause : do not extract clause part from PB constraint
  • cnf=n : translate directly to CNF by order encoding for the PB constraints containing at most n literals (default cnf=3)
  • decomp=n : try decomposition of PB constraints for the base up to n (default decomp=100)
  • dense : use dense counter matrix
  • no_axioms : do not generate axiom clauses
  • no_cache : do not use "reusing cache" of counter matrices
  • share=n : try to share counter matrices when the length is greater than or equal to n (0 means no sharing, default share=4)
• -java command : specifiles the command name of Java (default java)
• -jar file : specifies the name of jar file (default /usr/local/lib/pbsugar/pbsugar-v1-1-2.jar)
• -jopt1 opt : specifies the Java option for encoding and verification (default -Xmx2000M)
• -jopt2 opt : specifies the Java option for decoding (default -Xmx2000M)
• -n, -no_solve : specifies to perform only the encoding process
• -sat file : specifies the name of the output CNF file
• -map file : specifies the name of the mapping file
• -out file : specifies the name of the output file of the SAT solver
• -tmp path : specifies the path and prefix name of temporary files (default /tmp/pbsugar$$)
• -keep : specifies not to remove temporary created files
• -prof file : specifies the name of java profiling output
• -debug level : specifies the number of debugging level

This software is distributed under the BSD License.

• PB Solvers
  • borg
  • bsolo
  • clasp
  • MiniSat+
  • Sat4j
  • wbo
• Pseudo-Boolean Competitions
  • PB Competition 2012
  • PB Competition 2011
  • PB Competition 2010
  • PB Competition 2009
  • PB Competition 2007
  • PB Competition 2006
  • PB Competition 2005
• SAT Solvers
  • clasp
  • Glucose
  • GlueMiniSat
  • Lingeling
  • MiniSat
  • PrecoSAT
• Sugar : a SAT-based Constraint Solver