Problem Encoding

Author: Wolfgang Scherer

Contents

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.

000-indirect-conflict.x.v-000.png

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.

010-indirect-conflict-snf-conjunctions.r.v-000.png

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:

020-indirect-conflict-minimize-2-SAT-constraints.r.v-000.png

2-SAT constraint clauses and the variable clauses are identical

Conflict maximization is one possible variant of variable disambiguation.

020-indirect-conflict-minimize-2-SAT-constraints.c.v-000.png

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

020-indirect-conflict-minimize-2-SAT-constraints.r.v-001.png

2-SAT constraint clause reduction

2-SAT constraint clause reduction, 2nd pass

020-indirect-conflict-minimize-2-SAT-constraints.r.v-002.png

2-SAT constraint clause reduction, 2nd pass

Conflict detection for 2-SAT constraints

020-indirect-conflict-minimize-2-SAT-constraints.r.v-003.png

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

020-indirect-conflict-minimize-2-SAT-constraints.r.v-004.png

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

020-indirect-conflict-minimize-2-SAT-constraints.r.v-005.png

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:

020-indirect-conflict-minimize-2-SAT-constraints.c.v-001.png

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:

020-indirect-conflict-minimize-2-SAT-constraints.c.v-002.png

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

Superset/identity detection for variable region

020-indirect-conflict-minimize-2-SAT-constraints.c.v-003.png

Superset/identity detection for variable region

Remove redundancies

020-indirect-conflict-minimize-2-SAT-constraints.c.v-004.png

Remove redundancies

Playing along

Minimize variable encoding region

020-indirect-conflict-minimize-2-SAT-constraints.c.v-005.png

Minimize variable encoding region

Detect weak identities in minimized version

020-indirect-conflict-minimize-2-SAT-constraints.c.v-006.png

Detect weak identities in minimized version

Detect weak identities in minimized version

020-indirect-conflict-minimize-2-SAT-constraints.c.v-007.png

Detect weak identities in minimized version

Remove redundancies

020-indirect-conflict-minimize-2-SAT-constraints.c.v-008.png

Remove redundancies

Remove 4-SAT redundancies

020-indirect-conflict-minimize-2-SAT-constraints.c.v-009.png

Remove 4-SAT redundancies

Very weak identities

020-indirect-conflict-minimize-2-SAT-constraints.c.v-010.png

Very weak identities

Clean up

020-indirect-conflict-minimize-2-SAT-constraints.c.v-011.png

Clean up

Copyright

Copyright (C) 2013, Wolfgang Scherer, <Wolfgang.Scherer@gmx.de>. See the document source for conditions of use under the GNU Free Documentation License.