PBS v2.1

Incremental Pseudo-Boolean Backtrack Search SAT Solver and Optimizer

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@eecs.umich.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, "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@eecs.umich.edu)
Last updated May 25, 2004