DRAFT VERSION!!

OPARIS. Optimizing Pseudo-boolean RelSat

What is OPARIS?

OPARIS solves optimization problems with a linear objective function over linear pseudo-boolean constraints. See PBLIB. for a descrition of Psuedo-Boolean (PB) problems.

OPARIS uses an algorithm based on that of SAT-solvers such as zchaff. It combines

Davis-Putnam-Lovemann-Logeland DPLL search
Fast unit propagation via "watched literals"
Constraint learning
SAT-inspired branching heuristics based on VSIDS or similar methods.

Most notably it does NOT rely on linear relaxations; and so should prove complementary to such Operations Research methods.

Download

Once get licensing etc set up, then should be able to download an executable from here.

For the moment, to obtain a copy, please just email us: oparis00 'at' cirl.uoregon.edu

Relevant Papers

These papers discuss an earlier version "PARIS" that does not do the optimization, just just solves decision problems. However, they do describe the basic ideas of the search methods.

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

Input Format

Basically, OPARIS reads the ".opb" format used by Barth's opbdp solver. Example:

/* MPS name: P0033 */

/* objective function: */
min: + 318 C189 + 159 C188 + 228 C187 + 114 C186 + 318 C185 + 159 C184 + 318 C183 ;

/* 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;

© CIRL
URL for this page: http://www.cirl.uoregon.edu/OPARIS
Author: Andrew J. Parkes, http://www.cirl.uoregon.edu/parkes/
Feel free to email me with links/suggestions.
Last update: 2003-10-09