Author: | Wolfgang Scherer |
---|

Contents

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

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.

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.

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:

Conflict maximization is one possible variant of variable disambiguation.

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, 2nd pass

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

Conflict detection for 2-SAT constraints

As without conflict maximization, 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:

Superset/identity detection for variable region

Remove redundancies

Minimize variable encoding region

Detect weak identities in minimized version

Detect weak identities in minimized version

Remove redundancies

Remove 4-SAT redundancies

Very weak identities

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.