Galena

The package consists of the solver and several utilities:

galena
The solver, which solves both decision and optimization problems.
preprocess
This utility performs preprocessing to detect variable equivalences (modulo complementation) using a probing approach (also known as recursive learning), which may otherwise hinder a solver from effectively learning new constraints. In addition, it extracts pseudo-Boolean constraints when possible. For example:
(x or y)(y or z)(z or x) becomes x+y+z >=2
convert2mps
This reads in a set of files (using the same formats as galena) and outputs an MPS file to be read by a standard ILP solver.
mps2opb
This is a Python script which converts a problem in the MPS format used by most LP and ILP solvers to one in the OPB format used by galena and opbdp.

File format

The three programs galena, preprocess, and convert2mps use the same frontend and read the same types of files:

DIMACS format
The prevailing standard for specifying CNF clauses. Comment lines are prefixed with a c. The first non-comment line is p cnf <numvars> <numclauses>. Each clause is specified as a whitespace separated list of positive or negative numbers denoting positive or negative literals. The number 0 denotes the end of a clause's literals.
.CNF.PB format
This is used by Satire and PBS.
.OPB format
This is similar to that used by the OPBDP solver.

There's also some code which translates a fragment of the CPLEX LP format into something that Galena might understand. Compiled correctly against Boost 1.33.

OPB format

This is the preferred format. Any line beginning witih an asterisk '*' is a comment line. Each nonempty noncomment line is interpreted as a constraint or objective. Here is the EBNF grammar:

Nonterminals:
constraint ::= (op coef? lit)+ relation bound
objective  ::= label (op coef? lit)+ 

Terminals:
label      ::= (min|max):
op         ::= 	(+|-)
coef	   ::= 	-?[0-9]+
lit        ::= ~?x[0-9_]+
relation   ::= ("<="|">="|"=")
bound      ::= [0-9]+

Variable names start with x1. Terminals are seperated by whitespace, and contain no whitespace (strtok is used for tokenizing). Thus, ~x1 is short for (1-x1), while ~ x1 is an error. An objective with label "min:" is used for minimization. An objective with label "max:" is used for maximization.

In OPBDP, arbitrary identifiers can be used as variable names. However, to give the user some influence over the decision heuristic, variables are restricted to the xi format and numbered internally the same way as in the input.

Usage

For most normal usage, "galena <file>" is sufficient ("-" for stdin). Filetype is determined by the file extension: ".opb" for OPB, ".cnf.pb" for CNF+PB as used by PBS, all other extensions default to DIMACS CNF. As an exception, input read via stdin is assumed to be in OPB format.

All optimization problems are represented internally as maximization problems, and solved as a linear series of increasingly difficult decision problems. When a new solution is found, two numbers are shown, representing objective values assuming a maximization or minimization problems. UNSAT means that optimality is proven. Thus, bm23 has a minimum of 34, and 3blocks has a maximum of 63.

~/galena$ ./galena benchmarks/bm23.opb
benchmarks/bm23.opb has 20 constraints
CNF/CARD/LPB:   0       0       21
.|current optimum: 87 37
current optimum: 89 35
current optimum: 90 34
UNSAT
CNF/CARD/LPB:   2068    8       21
Decisions:      2964
Implications:   15085
RUNTIME:        0.173973s
58/2148/41
~/galena$ ./galena benchmarks/3blocks.opb
benchmarks/3blocks.opb has 8781 constraints
CNF/CARD/LPB:   7529    1253    0
.|current optimum: 61 -61
current optimum: 63 -63
UNSAT
CNF/CARD/LPB:   9302    1259    0
Decisions:      1880
Implications:   94562
RUNTIME:        0.796878s
189/1605/0

Releases

The code is rather buggy; use is at own risk.

Linux x86 binaries

References