PBLIB - The Pseudo-Boolean Library --- DRAFT VERSION!!

The URL for this page is http://www.cirl.uoregon.edu/PBLIB

My intention is to build an equivalent of the "SATLIB - The Satisfiability Library" page, but for systems where the constraints are linear pseudo-Boolean inequalities.

Just collecting information/links for the moment. Hope to get a chance to improve the format sometime soon!

I am happen to receive links/suggestions: email parkes 'at' cirl.uoregon.edu.

What is "(Linear) Pseudo-Boolean" (PB)

All variables take values of either 0 (false) or 1 (true). Hence the use of "Boolean"

Constraints are linear inequalities with integer coefficients, for example

2x + y + z >= 2

Coefficients do not need to be positive, however it is somewhat more convenient to always make them positive by using the negated variables:

~x = 1-x

(~x should perhaps be x with a bar over the top, but HTML is a pain for math) then, for example,

-2x + y + z >= 0

becomes

-2(1-~x) + y + z >= 0

2 ~x + y + z >= 2

The special case when all the coefficients on the left are one, is called a "cardinality constraint"

The important thing to note is that PB constraints are much more compact than propositional clauses

Another form of quick explanation depends on your background:

For operations research (OR) people it is just "pure 0-1 programming", standard integer programming with linear constraints but specialized to the case that all variables are 0 or 1. See Section II.6.2 (page 456) of "Integer and Combinatorial Optimization" by Nemhauser and Wolsey.
Satisfiability
Think of clauses as constraints in which all coefficients are one.
x or y or z
becomes
x+y+z >= 1
Then it is natural to allow the coefficients to change from one. For work on satisfiability start from SATLIB

Generally, it seems that the term "Pseudo-Boolean" is used when the intended solution algorithm uses purely boolean methods, that is, without any linear relaxations involved. If a standard LP-based OR method (such as branch-and-bound or branch-and-cut) is used then the term "0-1 programming" seems more likely to be used.

Key Links

General

SATLIB have links to many algorithms for satisfiability problems.

Solvers

OPBDP Barth's "Optimizing Pseudo-Boolean Davis-Putnam" solver
Integer Local Search: WSAT(OIP). "WSAT(OIP) subsumes WSAT(PB), a code for pseudo-Boolean constraints."
SATIRE from the University of Michigan
(not yet released, as of 2002-09-27) PBS also from the University of Michigan
Steven Prestwich's CLS, search for "Randomised Backtracking for Linear Pseudo-Boolean Constraint Problems" somewhere on Cork Constraint Computation Centre
Satzoo "A Chaff-like SAT-solver based on watched literals and clause recording. It was developed mainly to be able to experiment with new model checking techniques which requires a tighter integration with the SAT-solver. ..."
BSOLO "a solver for restricted forms of 0-1 Integer Linear Programs (ILPs), being targeted at solving instances of the Unate and Binate Covering Problems (UCP/BCP) ...". Here are some references for the covering work.

People

Papers

Linear 0-1 Inequalities and Extended Clauses (1994). Peter Barth
Heidi E. Dixon and Matthew L. Ginsberg 2000. Combining Satisfiability techniques from AI and OR. The Knowledge Engineering Review 15(1).
Heidi E. Dixon and Matthew L. Ginsberg 2002. Inference methods for a pseudo-Boolean satisfiability solver Accepted for publication in The Eighteenth National Conference on Artificial Intelligence (AAAI-2002).
Steven Prestwich's CLS, search for "Randomised Backtracking for Linear Pseudo-Boolean Constraint Problems" somewhere on Cork Constraint Computation Centre (currently can be found at cpaior02.ps)
Fadi A. Aloul, Electrical Engineering and Computer Science, University of Michigan, USA (with Arathi Ramani, Igor Markov, and Karem Sakallah), PBS: a backtrack-search psuedo-boolean solver and optimizer To appear in SAT 2002

File Formats

".opb" is used by Barth's solver. Example:

/* MPS name: P0033 */

/* objective function: */
min: + 318 C189 + 159 C188 + 228 C187 + 114 C186 + 318 C185 + 159 C184 + 318 C183 + 159 C182 + 318 C181 + 159 C180 + 318 C179 + 159 C178 + 500 C1
77 + 250 C176 + 500 C175 + 250 C174 + 517 C173 + 258 C172 + 183 C171 + 49 C170 + 183 C169 + 183 C168 + 183 C167 + 183 C166 + 69 C165 + 69 C164 + 
163 C163 + 162 C162 + 163 C161 + 171 C160 + 171 C159 + 171 C158 + 171 C157 ;

/* constraints */
R128 : + -400 C189 + -200 C188 + -285 C163 <= -270;
R127 : + -400 C177 + -200 C176 + -400 C175 + -200 C174 + -300 C158 <= -500;
R126 : + -400 C175 + -200 C174 + -300 C158 <= -5;
R125 : + -400 C181 + -200 C180 + -400 C179 + -200 C178 + -230 C168 + -230 C167 + -265 C164 + -285 C161 <= -1026;
R124 : + -400 C179 + -200 C178 + -230 C167 + -265 C164 + -285 C161 <= -335;
R123 : + -400 C185 + -200 C184 + -400 C183 + -200 C182 + -190 C170 + -230 C169 + -265 C165 + -285 C162 + -300 C159 + -300 C157 <= -1656;
R122 : + -400 C183 + -200 C182 + -190 C170 + -265 C165 + -285 C162 + -300 C157 <= -900;
R121 : + -400 C187 + -200 C186 + -300 C160 <= -100;
R120 : + -400 C187 + -200 C186 + -400 C185 + -200 C184 + -400 C183 + -200 C182 + -400 C181 + -200 C180 + -400 C179 + -200 C178 + -190 C170 + -230
 C169 + -230 C168 + -265 C165 + -265 C164 + -285 C162 + -285 C161 + -300 C160 + -300 C159 <= -2600;
R119 : + 400 C187 + 200 C186 + 400 C185 + 200 C184 + 400 C183 + 200 C182 + 400 C181 + 200 C180 + 400 C179 + 200 C178 + 190 C170 + 230 C169 + 230 
C168 + 265 C165 + 265 C164 + 285 C162 + 285 C161 + 300 C160 + 300 C159 <= 2700;
R118 : + -400 C173 + -200 C172 + -230 C166 <= -5;
R117 : + 1 C171 + 1 C169 + 1 C168 + 1 C167 + 1 C166 <= 1;
R116 : + 1 C165 + 1 C164 <= 1;
R115 : + 1 C163 + 1 C162 + 1 C161 <= 1;
R114 : + 1 C160 + 1 C159 + 1 C158 + 1 C157 <= 1;

".oip" is used by Walser's WSAT(OIP) solver

AMPL is also taken by Walser's solver.