PBS v2.1

Incremental Pseudo-Boolean Backtrack Search SAT Solver and Optimizer

A new version of PBS is currently available. click here

Introduction

• 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

• Linux executable: PBSv2.1_Linux.tar.gz
• Solaris executable: PBSv2.1_Solaris.tar.gz
• Windows executable: PBSv2.1_Win.tar.gz

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: 2^nd release of PBS . optimized PB engine.

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

References

• F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "Solution and Optimization of Systems of Pseudo-Boolean Constraints" IEEE Transactions on Computers (TC), 56(10), 1415-1424, October 2007.
• F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "Generic ILP versus Specialized 0-1 ILP: an Update" International Conference on Computer Aided Design (ICCAD), 2002.
• F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "PBS: A Backtrack Search Pseudo-Boolean Solver" Symposium on the Theory and Applications of Satisfiability Testing (SAT), 2002.
  
  

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