Problem Encoding

Author: Wolfgang Scherer

Reduced Encoding of SNF instances

The following example is used to illustrate reduction of problem encodings.

Boolean formula:

```(  a0 ∨  a1 ∨  a2 ∨  a3 ) ∧
(  b0 ∨  b1 ∨  b2 ∨  b3 ) ∧
(  c0 ∨  c1 ∨  c2 ∨  c3 ) ∧
( ¬a0 ∨ ¬c2 ) ∧
( ¬a0 ∨ ¬c3 ) ∧
( ¬a1 ∨ ¬c2 ) ∧
( ¬a1 ∨ ¬c3 ) ∧
( ¬a2 ∨ ¬c0 ) ∧
( ¬a2 ∨ ¬c1 ) ∧
( ¬a3 ∨ ¬c0 ) ∧
( ¬a3 ∨ ¬c1 ) ∧
( ¬b0 ∨ ¬c0 ) ∧
( ¬b0 ∨ ¬c1 ) ∧
( ¬b1 ∨ ¬c0 ) ∧
( ¬b1 ∨ ¬c1 ) ∧
( ¬b2 ∨ ¬c2 ) ∧
( ¬b2 ∨ ¬c3 ) ∧
( ¬b3 ∨ ¬c2 ) ∧
( ¬b3 ∨ ¬c3 )
```

Clause vectors:

```[ 1 1 1 1 _ _ _ _ _ _ _ _ ]
[ _ _ _ _ 1 1 1 1 _ _ _ _ ]
[ _ _ _ _ _ _ _ _ 1 1 1 1 ]
[ 0 _ _ _ _ _ _ _ _ _ 0 _ ]
[ 0 _ _ _ _ _ _ _ _ _ _ 0 ]
[ _ 0 _ _ _ _ _ _ _ _ 0 _ ]
[ _ 0 _ _ _ _ _ _ _ _ _ 0 ]
[ _ _ 0 _ _ _ _ _ 0 _ _ _ ]
[ _ _ 0 _ _ _ _ _ _ 0 _ _ ]
[ _ _ _ 0 _ _ _ _ 0 _ _ _ ]
[ _ _ _ 0 _ _ _ _ _ 0 _ _ ]
[ _ _ _ _ 0 _ _ _ 0 _ _ _ ]
[ _ _ _ _ 0 _ _ _ _ 0 _ _ ]
[ _ _ _ _ _ 0 _ _ 0 _ _ _ ]
[ _ _ _ _ _ 0 _ _ _ 0 _ _ ]
[ _ _ _ _ _ _ 0 _ _ _ 0 _ ]
[ _ _ _ _ _ _ 0 _ _ _ _ 0 ]
[ _ _ _ _ _ _ _ 0 _ _ 0 _ ]
[ _ _ _ _ _ _ _ 0 _ _ _ 0 ]
a a a a b b b b c c c c
0 1 2 3 0 1 2 3 0 1 2 3
```

Satoku Matrix

Conflict maximization shows, that 8 variables are sufficient to encode the problem.

Remember, that the variable region of a satoku matrix is entirely optional.

The clause sub-matrixes in the 2-SAT region of the source problem become equivalent to a subset of the variables.

Conflict maximization shows reduced encoding

Reduced Encoding

Here is the reduced encoding of the source problem:

```[ 0 0 0 0 _ _ _ _ ]
[ _ _ _ _ 0 0 0 0 ]
[
[ _ _ 1 1 1 1 _ _ ]
[ _ _ 1 1 1 1 _ _ ]
[ 1 1 _ _ _ _ 1 1 ]
[ 1 1 _ _ _ _ 1 1 ]
a a a a b b b b
0 1 2 3 0 1 2 3
]
a a a a b b b b
0 1 2 3 0 1 2 3
```

Boolean formula:

```( ¬a0 ∨ ¬a1 ∨ ¬a2 ∨ ¬a3 ) ∧
( ¬b0 ∨ ¬b1 ∨ ¬b2 ∨ ¬b3 ) ∧
(
(  a2 ∧  a3 ∧  b0 ∧  b1 ) ∨
(  a2 ∧  a3 ∧  b0 ∧  b1 ) ∨
(  a0 ∧  a1 ∧  b2 ∧  b3 ) ∨
(  a0 ∧  a1 ∧  b2 ∧  b3 )
)
```

Mapping the reduced problem to a satoku matrix shows, that the conflict situation is equivalent to the original problem.

Problem encoded with 8 variables

Distributive Expansion of SNF 2-SAT Constraints

CNF Clauses, that have a common literal can be expanded to a single CNF with the literal as one alternative and the conjunction of all other literals as second alternative:

```(p v q0) & (p v q1) & ... & (p v qn) = p v (q0 & q1 & ... & qn)
```

This allows for transforming the example above to:

```(  a0 ∨  a1 ∨  a2 ∨  a3 ) ∧
(  b0 ∨  b1 ∨  b2 ∨  b3 ) ∧
(  c0 ∨  c1 ∨  c2 ∨  c3 ) ∧
(( ¬a0 ) ∨ ( ¬c2 ∧ ¬c3 ))
(( ¬a1 ) ∨ ( ¬c2 ∧ ¬c3 ))
(( ¬a2 ) ∨ ( ¬c0 ∧ ¬c1 ))
(( ¬a3 ) ∨ ( ¬c0 ∧ ¬c1 ))
(( ¬b0 ) ∨ ( ¬c0 ∧ ¬c1 ))
(( ¬b1 ) ∨ ( ¬c0 ∧ ¬c1 ))
(( ¬b2 ) ∨ ( ¬c2 ∧ ¬c3 ))
(( ¬b3 ) ∨ ( ¬c2 ∧ ¬c3 ))
(( ¬c0 ) ∨ ( ¬a2 ∧ ¬a3 ∧ ¬b0 ∧ ¬b1 ))
(( ¬c1 ) ∨ ( ¬a2 ∧ ¬a3 ∧ ¬b0 ∧ ¬b1 ))
(( ¬c2 ) ∨ ( ¬a0 ∧ ¬a1 ∧ ¬b2 ∧ ¬b3 ))
(( ¬c3 ) ∨ ( ¬a0 ∧ ¬a1 ∧ ¬b2 ∧ ¬b3 ))
```

Clause Vectors:

```[ 1 1 1 1 _ _ _ _ _ _ _ _ ]
[ _ _ _ _ 1 1 1 1 _ _ _ _ ]
[ _ _ _ _ _ _ _ _ 1 1 1 1 ]
[
[ 0 _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ 0 0 ]
]
[
[ _ 0 _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ 0 0 ]
]
[
[ _ _ 0 _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ 0 0 _ _ ]
]
[
[ _ _ _ 0 _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ 0 0 _ _ ]
]
[
[ _ _ _ _ 0 _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ 0 0 _ _ ]
]
[
[ _ _ _ _ _ 0 _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ 0 0 _ _ ]
]
[
[ _ _ _ _ _ _ 0 _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ 0 0 ]
]
[
[ _ _ _ _ _ _ _ 0 _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ 0 0 ]
]
[
[ _ _ _ _ _ _ _ _ 0 _ _ _ ]
[ _ _ 0 0 0 0 _ _ _ _ _ _ ]
]
[
[ _ _ _ _ _ _ _ _ _ 0 _ _ ]
[ _ _ 0 0 0 0 _ _ _ _ _ _ ]
]
[
[ _ _ _ _ _ _ _ _ _ _ 0 _ ]
[ 0 0 _ _ _ _ 0 0 _ _ _ _ ]
]
[
[ _ _ _ _ _ _ _ _ _ _ _ 0 ]
[ 0 0 _ _ _ _ 0 0 _ _ _ _ ]
]
```

Mapping to a satoku matrix without conflict maximization shows, that the 2-SAT constraint clauses and variable clauses are identical:

2-SAT constraint clauses and the variable clauses are identical

Conflict maximization is one possible variant of variable disambiguation.

Conflict maximization is one possible variant of variable disambiguation

Reduction Without Maximization

The 2-SAT constraints can still be made identical to the variables, but they can also be reduced independently:

2-SAT constraint clause reduction

2-SAT constraint clause reduction

2-SAT constraint clause reduction, 2nd pass

2-SAT constraint clause reduction, 2nd pass

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

Reduction With Maximization

As without conflict maximization, identity detection for 2-SAT constraints has no influence on the variable region:

Identity detection for 2-SAT constraints has no influence on the variable region

Conflict detection for 2-SAT constraints also adjusts the otherwise independent variable region:

Conflict detection for 2-SAT constraints also adjusts the otherwise independent variable region

Superset/identity detection for variable region

Superset/identity detection for variable region

Remove redundancies

Remove redundancies

Playing along

Minimize variable encoding region

Minimize variable encoding region

Detect weak identities in minimized version

Detect weak identities in minimized version

Detect weak identities in minimized version

Detect weak identities in minimized version

Remove redundancies

Remove redundancies

Remove 4-SAT redundancies

Remove 4-SAT redundancies

Very weak identities

Very weak identities

Clean up

Clean up