News
September 1, 2005 - First public version of PBS4 is now released. 

October 1, 2005 - PBS4 was among the fastest solvers in the PB'05 evaluation held during the SAT'05 conference.  

 

What's PBS4?

Pseudo-Boolean Solver v4.0 (PBS4) is one of the state-of-the art pseudo-Boolean SAT solvers. It is based on the zChaff 2004 solver and the original PBS solver.

PBS4 can solve decision and optimization problems and can read the following input formats: CNF, pseudo-Boolean (PB), and OPB.

PBS4 implements several advanced SAT algorithms including:

1. Watched-literals
2. Random restarts
3. Clause deletion
4. VSIDS decision heuristic
5. 1^st-UIP conflict clause learning
6. Linear/Binary search for optimization instances
   
   

In-progress

1. Rewriting the main data-structures in a more sophisticated fashion for efficiency purposes
2. Pseudo-Boolean clause learning
3. Pseudo-Boolean watched literals
   
   

and much more to come...

Downloads

• Linux or Solaris executable of PBS4 (Email faloul@aus.edu for a copy of PBS4)
  
  
  

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), 450-457, 2002.
  
  

Developers

Bashar Al-Rawi  (Junior Undergraduate Student) Department of Computer Engineering American University in Dubai Dubai, United Arab Emirates (UAE) Bashar.Alrawi@mymail.aud.edu

Prof. Fadi Aloul Department of Computer Engineering American University of Sharjah Sharjah, United Arab Emirates (UAE) faloul@aus.edu

 

Last updated September 1, 2005.