# Distributed Conjunctive Single-Selection (3-SAT)

Author: Wolfgang Scherer

# Base Problem

## Boolean Formula

```(( ¬a0 ∧ ¬a1 ∧ ¬a2 ) ∨ ( ¬b0 ∧ ¬b1 ) ∨ ( ¬c0 ∧ ¬c1 )) ∧
(( ¬a0 ∧ ¬a1 ∧  a2 ) ∨ ( ¬b0 ∧  b1 ) ∨ ( ¬d0 ∧ ¬d1 )) ∧
(( ¬a0 ∧  a1 ∧ ¬a2 ) ∨ ( ¬d0 ∧  d1 ) ∨ ( ¬e0 ∧ ¬e1 )) ∧
(( ¬a0 ∧  a1 ∧  a2 ) ∨ ( ¬e0 ∧  e1 ) ∨ ( ¬f0 ∧ ¬f1 )) ∧
((  a0 ∧ ¬a1 ∧ ¬a2 ) ∨ ( ¬f0 ∧  f1 ) ∨ ( ¬g0 ∧ ¬g1 )) ∧
((  b0 ∧ ¬b1 )       ∨ ( ¬c0 ∧  c1 ) ∨ (  d0 ∧ ¬d1 )) ∧
((  b0 ∧  b1 )       ∨ (  f0 ∧ ¬f1 ) ∨ ( ¬g0 ∧  g1 )) ∧
((  c0 ∧ ¬c1 )       ∨ (  e0 ∧ ¬e1 ) ∨ (  g0 ∧ ¬g1 ))
```

## Clause Vectors

```[
[ 0 0 0 _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ ]
]
[
[ 0 0 1 _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ 0 0 _ _ _ _ _ _ ]
]
[
[ 0 1 0 _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ 0 1 _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ 0 0 _ _ _ _ ]
]
[
[ 0 1 1 _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ 0 1 _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ 0 0 _ _ ]
]
[
[ 1 0 0 _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ 0 1 _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 0 ]
]
[
[ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ 0 1 _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ ]
]
[
[ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 1 ]
]
[
[ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 ]
]
a a a b b c c d d e e f f g g
0 1 2 0 1 0 1 0 1 0 1 0 1 0 1
```

## Complexities

n-complexity: O(215) = 32768
m-complexity: O(⌈3 ⁄ 2⌉8) = O(28) = 256

# Plain Mapping

Plain mapping does not detect unsatisfiability

# Fast Conjunctive Conflict Maximization

Fast conjunctive conflict maximization detects unsatisfiability immediately (s[2, 2]).

n-complexity: O(215) = 32768
m-complexity: O(⌈3 ⁄ 2⌉8) = O(28) = 256

m-complexity: O(⌈10 ⁄ 2⌉5)*O(⌈7 ⁄ 2⌉3) = O(55)*O(43) = 3125*64 = 200000