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. 1st-UIP conflict clause learning
  6. Linear/Binary search for optimization instances


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




Bashar Al-Rawi  (Junior Undergraduate Student)
Department of Computer Engineering
American University in Dubai
Dubai, United Arab Emirates (UAE)

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


Last updated September 1, 2005.