# Distributed Conjunctive Single-Selection (4-SAT)

Author: Wolfgang Scherer

# 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

# Fast Conjunctive Conflict Maximization

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.