PBSugar: A SAT-based Pseudo-Boolean Solver

Table of Contents

Overview

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.

What's New

  • 2013-04-17 Wed Exprimental Results comparing PBSugar with Sat4j, clasp, bsolo, wbo, and MiniSat+
  • 2013-02-14 Thu Release of version 1.1.1

Download

Requirements

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

Installation

  1. Unzip the pbsugar-v1-1-1.zip file
  2. Install with the following commands
    $ cd pbsugar-v1-1-1/bin
    $ make install
    
    • The pbsugar-v1-1-1.jar file will be installed to /usr/local/lib/pbsugar directory.
    • The pbsugar script file will be installed to /usr/local/bin directory.

Documents

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

Example Usage

$ pbsugar -solver glucose file.opb
  • Please specify the command name of the SAT solver with -solver option.

Command Line Usage

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-1.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

License

This software is distributed under the BSD License. See LICENSE.txt for more details.

Links

Date: 2013-04-17 20:21:16 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0