UAI 2016 Inference Evaluation

Organizers: Vibhav Gogate, Tahrima Rahman, Somdeb Sarkhel, David Smith, and Deepak Venugopal

Binary Model Format

We use the .buai suffix to specify binary format.

The binary format is based on the DIMACS format, with a specific interpretation. The interpretation is chosen among a number of available choices because it allows us to specify hard as well as soft constraints without recourse to infinity.

Following is an example file:

c
c comments: an example binary UAI file
c
p buai 3 4
10.1 1 -2 0
3.2 -1 2 -3 0
0.0 -3 2 0
5.7 1 3 0

The file is divided into three sections:

Comments: Lines beginning with a ‘c’ are comments, used to specify things like source of the problem, solution if available, etc.
Number of variables and clauses specification: Lines beginning with a 'p’ give problem specification. For example, the line 'p buai 3 4’ specifies that the problem has 3 Boolean variables, say , and 4 clauses. Variables are numbered consecutively beginning with 1. Note that variables start with 0 for UAI model and sparse model formats.
Clauses: Each clause begins with a non-negative real-number, namely a number , that gives the weight of the clause. Then the clause is defined by listing the index of each positive literal, and the negative index of each negative literal. The definition of a clause is terminated by a “0”. Hard clauses have zero weight (more on this in the interpretation described below). For example, the line “10.1 1 -2 0” specifies the clause with weight .

Note that the sections must appear in order. For example, comments cannot appear after (or in between) clauses.

We use the .buai suffix for files in this format.

Interpretation and Distribution

We assume that the network defined in a “buai” file represents the following probability distribution:

$Pr(x) = frac{1}{Z} prod_{i=1}^{n} w_i^{{f_i(x)}}$

where is a truth-assignment to all Boolean variables, w_i is the weight attached to the -th clause, and f_i(x) is if evaluates the -th clause to false and otherwise (the clauses are indexed from to ). In other words, if the truth assignment evaluates a clause to false, then the clause contributes its weight to the product. Otherwise it contributes a , and thus has no effect on the product. We assume that 0^0=1 . Notice that if the weight of a clause is and the truth assignment evaluates it to false, then the probability of the assignment is and therefore clauses with zero weight are hard clauses.

is the normalization constant or the partition function given by:

$Z=sum_{x} prod_{i=1}^{n} w_i^{{f_i(x)}}$

For instance, the probability of the assignment (x_1=F,x_2=T,x_3=F) for our example network:

$P(x_1=F,x_2=T,x_3=F)= frac{1}{Z} (10.1^{1} times 3.2^0 times 0^0 times 5.7^1)=frac{1}{Z} (10.1times 5.7)=frac{57.57}{Z}$

The reader can verify that the partition function is equal to 76.37 .

Weighted Partial MAX-SAT solvers

We encourage submissions of weighted partial MAX-SAT solvers. Please email Vibhav Gogate if you have a solver that can handle the weighted partial MAX-SAT format used in the 2016 MAX-SAT evaluation, given here.