PBS v2.1

Incremental Pseudo-Boolean Backtrack Search SAT Solver and Optimizer

A new version of PBS is currently available. click here


  • Reads as input both:
    • CNF constraints 
    • PB constraints (e.g. -2x + 3y + . + 6z <= 7, where x, y, and z are Boolean literals.)
  • Can be used to solve decision (Yes/No) and optimization (Max/Min) problems.
  • Includes incremental features.
  • PBS options include:
    • Static/Dynamic decision heuristics
    • 1-UIP conflict diagnosis
    • Random restarts and backtracking

Download Binary

To get notified of future updates of PBS please email faloul@aus.edu your Name, Email, and Affiliation.

Also please let me know if you cite PBS in your work.

Latest Updates:

<<<<<<         January 2003: 2nd release of PBS . optimized PB engine.

<<<<<<         November 2002: 1st release of PBS.


Maintained by Fadi Aloul (faloul@aus.edu)
Last updated May 25, 2009