Distributed Conjunctive Single-Selection (4-SAT)

Author: Wolfgang Scherer

Contents

Base Problem

Boolean Formula

(( ¬a0 ∧ ¬a1 ) ∨ ( ¬b0 ∧ ¬b1 ) ∨ ( ¬c0 ∧ ¬c1 ) ∨ ( ¬d0 ∧ ¬d1 )) ∧
(( ¬a0 ∧  a1 ) ∨ ( ¬b0 ∧  b1 ) ∨ ( ¬d0 ∧  d1 ) ∨ ( ¬e0 ∧ ¬e1 )) ∧
((  a0 ∧ ¬a1 ) ∨ (  d0 ∧ ¬d1 ) ∨ ( ¬e0 ∧  e1 ) ∨ ( ¬f0 ∧ ¬f1 )) ∧
((  a0 ∧  a1 ) ∨ ( ¬c0 ∧  c1 ) ∨ ( ¬g0 ∧ ¬g1 ) ∨ ( ¬h0 ∧ ¬h1 )) ∧
((  b0 ∧ ¬b1 ) ∨ (  c0 ∧ ¬c1 ) ∨ ( ¬g0 ∧  g1 ) ∨ ( ¬i0 ∧ ¬i1 )) ∧
((  b0 ∧  b1 ) ∨ ( ¬f0 ∧  f1 ) ∨ ( ¬j0 ∧ ¬j1 ) ∨ ( ¬k0 ∧ ¬k1 )) ∧
((  c0 ∧  c1 ) ∨ ( ¬h0 ∧  h1 ) ∨ ( ¬i0 ∧  i1 ) ∨ ( ¬k0 ∧  k1 )) ∧
((  d0 ∧  d1 ) ∨ (  e0 ∧ ¬e1 ) ∨ (  f0 ∧  f1 ) ∨ (  i0 ∧ ¬i1 )) ∧
((  e0 ∧  e1 ) ∨ (  h0 ∧ ¬h1 ) ∨ ( ¬j0 ∧  j1 ) ∨ (  k0 ∧ ¬k1 )) ∧
((  f0 ∧ ¬f1 ) ∨ (  g0 ∧ ¬g1 ) ∨ (  j0 ∧ ¬j1 ) ∨ (  k0 ∧  k1 )) ∧
((  g0 ∧  g1 ) ∨ (  h0 ∧  h1 ) ∨ (  i0 ∧  i1 ) ∨ (  j0 ∧  j1 ))

Clause Vectors

[
  [ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
]
[
  [ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ ]
]
[
  [ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ ]
]
[
  [ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 0 _ _ _ _ _ _ ]
]
[
  [ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ 0 1 _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 0 _ _ _ _ ]
]
[
  [ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 0 _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 0 ]
]
[
  [ _ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 1 _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 1 _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 1 ]
]
[
  [ _ _ _ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ ]
]
[
  [ _ _ _ _ _ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 1 _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 ]
]
[
  [ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 ]
]
[
  [ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 _ _ _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 _ _ _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 _ _ _ _ ]
  [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 _ _ ]
]
    a a b b c c d d e e f f g g h h i i j j k k
    0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1

Complexities

n-complexity: O(222) = 4194304
m-complexity: O(⌈4 ⁄ 2⌉11) = O(211) = 2048

Plain Mapping

000-construct.v-000.png

Fast Conjunctive Conflict Maximization

000-construct.f.v-000.png

Find solution by combining S[11] and S[12], specifically s[11, 14] with s[12, 0], s[12, 1], s[12, 8].

Then combine the result of s[11, 14] X s[12, 8] (s[44, 2]) with s[21, 1], s[21, 8], s[21, 10].

The combination s[44, 2], s[21, 8] (s[45, 1]) is detected as contradiction.

The combination s[44, 2], s[21, 10] (s[45, 2]) is detected as solution (all variables are assigned). Additionally, all clauses of the core problem are bound to a single selection.

Note, that there is some redundancy for selections of the fast conflict clauses.

000-construct.f.v-003-01.png

Full Conjunctive Conflict Maximization

000-construct.m.v-002-color.png

Copyright

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