Team:MoWestern Davidson/project mathmodel

Lego Models

B2 Bomber

We used Wolfram Mathematica to visualize 2-SAT problems and particularly to analyze unsatisfiable problems with varying numbers of clauses.

The clauses of 2-SAT problems can be graphed as boxes on a grid, like the one below. This grid shows all of the 4-variable 2-SAT problems.

So, for example, the square completely to the bottom left corresponds to the clause a'b.

Rough and Fine Distributions

To classify SAT problems, we began looking at the rough distribution of each problem, meaning how many inputs satisfied a certain number of clauses in a problem. There are ₃C₂ ×2² = 12 clauses for 3 variables 2-SAT. There are ₁₂C₃ = 220 problems with 3 clauses. The table below gives the number of clauses satisfied by each input for a few select 2-SAT problems.

The rough distribution for the red problem is 0143. That distribution means 0 inputs satisfied 0 clauses, 1 input satisfied 1 clause, 4 inputs satisfied 2 clauses and 3 inputs satisfied all 3 clauses.

The following pie chart shows 2-SAT 3-clause problems grouped by rough distribution, with all shades of a given color representing one rough distribution.

Fine distributions look more deeply at how each clause was satisfied. If an input satisfies one or two literals in a clause, that clause is satisfied singly or doubly respectively. For example, the input abc’ satisfies the clause (a OR b’) singly because it satisfies only one literal in the clause. However, the same input abc’ satisfies the clause (b OR c’) doubly because it satisfies two literals in the clause.

The fine distribution for the red problem from the table above is 0011212100. This distribution means that 0 inputs satisfied 0 clauses, 0 inputs satisfied 1 clause singly, 1 input satisfied 1 clause doubly, 1 input satisfied 2 clauses with 2 singles, 2 inputs satisfied 2 clauses with 1 single and 1 double, 1 input satisfied 2 clauses with 2 doubles, 2 inputs satisfied 3 clauses with 3 singles, 1 input satisfied 3 clauses with 2 singles and 1 double, 0 inputs satisfied 3 clauses with 1 single and 2 doubles, and 0 inputs satisfied 3 clauses with 3 doubles.

The following pie chart shows 2-SAT, 3-clause problems grouped by fine distribution, with each shade of a given color representing one fine distribution.