Author: Wolfgang Scherer

# All Clauses Identical

Boolean problem:

```(  a0 ∨  a1 ∨  a2 ) ∧
(  b0 ∨  b1 ∨  b2 ) ∧
(  c0 ∨  c1 ∨  c2 ) ∧
(  d0 ∨  d1 ∨  d2 ) ∧
(  e0 ∨  e1 ∨  e2 ) ∧
( ¬a0 ∨ ¬e1 ) ∧
( ¬a0 ∨ ¬e2 ) ∧
( ¬a1 ∨ ¬e0 ) ∧
( ¬a1 ∨ ¬e2 ) ∧
( ¬a2 ∨ ¬e0 ) ∧
( ¬a2 ∨ ¬e1 ) ∧
( ¬b0 ∨ ¬c1 ) ∧
( ¬b0 ∨ ¬c2 ) ∧
( ¬b1 ∨ ¬c0 ) ∧
( ¬b1 ∨ ¬c2 ) ∧
( ¬b2 ∨ ¬c0 ) ∧
( ¬b2 ∨ ¬c1 ) ∧
( ¬c0 ∨ ¬d1 ) ∧
( ¬c0 ∨ ¬d2 ) ∧
( ¬c1 ∨ ¬d0 ) ∧
( ¬c1 ∨ ¬d2 ) ∧
( ¬c2 ∨ ¬d0 ) ∧
( ¬c2 ∨ ¬d1 ) ∧
( ¬d0 ∨ ¬e1 ) ∧
( ¬d0 ∨ ¬e2 ) ∧
( ¬d1 ∨ ¬e0 ) ∧
( ¬d1 ∨ ¬e2 ) ∧
( ¬d2 ∨ ¬e0 ) ∧
( ¬d2 ∨ ¬e1 )
```

Clause vectors:

```[ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ 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 ]
[ _ _ _ _ _ _ _ _ _ _ _ 0 0 _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ 0 _ 0 _ ]
a a a b b b c c c d d d e e e
0 1 2 0 1 2 0 1 2 0 1 2 0 1 2
```

Satoku matrix without requirements update

Satoku matrix without requirements update

## Row update for selection row s00

Row update for selection row s00 , 1st pass

Row update for selection row s00 , 1st pass

Row update for selection row s00 , 2nd pass

Row update for selection row s00 , 2nd pass

Row update for selection row s00 , 3rd pass

Row update for selection row s00 , 3rd pass

Row update for selection row s00 , 4th pass

Row update for selection row s00 , 4th pass

Row update for selection row s00 , 6th pass

Row update for selection row s00 , 6th pass

Row update for selection row s00 , 7th pass

Row update for selection row s00 , 7th pass

Row update for selection row s00 , 8th pass

Row update for selection row s00 , 8th pass

Row update for selection row s00 , 9th pass

Row update for selection row s00 , 9th pass

## Row updates for selection rows s01, s02

Row update for selection row s01

Row update for selection row s01

Row update for selection row s02

Row update for selection row s02

## Row updates for clause submatrix S1

Row update for selection row s10

Row update for selection row s10

Row update for s11

Row update for s11

Row update for selection row s12

Row update for selection row s12

Row update for clause sub-matrixes S2, S3, S4

Row update for clause sub-matrixes S2, S3, S4

## Satoku Statistics

### Sparse Encoding

Satoku Statistics
satisfiable True
init clauses 29
init variables 0
init rows 63
clauses 29
variables 0
rows 63
cells 3969
clauses deleted 0
row kills 0
duplicate kills 0
zero changes 600
soft changes 300
zero update passes 0
row update passes 2
superset update passes 1
row checks 72
row merges 147
message
ratio: 147 ⁄ 63 = 2.33333333333

### Full Encoding

When all redundancies are fully encoded in 2-SAT constraints.

Satoku Statistics
satisfiable True
init clauses 65
init variables 0
init rows 135
clauses 65
variables 0
rows 135
cells 18225
clauses deleted 0
row kills 0
duplicate kills 0
zero changes 1320
soft changes 660
zero update passes 0
row update passes 2
superset update passes 1
row checks 63
row merges 291
message
ratio: 291 ⁄ 135 = 2.15555555556

Full encoding of 10 3-SAT clauses.

Satoku Statistics
satisfiable True
init clauses 280
init variables 0
init rows 570
clauses 280
variables 0
rows 570
cells 324900
clauses deleted 0
row kills 0
duplicate kills 0
zero changes 11340
soft changes 5670
zero update passes 0
row update passes 2
superset update passes 1
row checks 123
row merges 1196
message
ratio: 1196 ⁄ 570 = 2.09824561404

The increase in row merges is almost linear:

rows: 570 ⁄ 135 = 4.22222222222
row checks: 123 ⁄ 63 = 1.95238095238
row merges: 1196 ⁄ 291 = 4.10996563574

# 2-SAT All Identical

10 clauses:

```// rows                        200
// zero changes              19800
// row checks                  811
// row merges                 1049
```
ratio: 1049 ⁄ 200 = 5.245

20 clauses:

```// rows                        800
// zero changes             319200
// row checks                 3221
// row merges                 4309
```
ratio: 4309 ⁄ 800 = 5.38625
rows: 800 ⁄ 200 = 4
row checks: 3221 ⁄ 811 = 3.97163995068
row merges: 4309 ⁄ 1049 = 4.10772163966

40 clauses:

```// rows                         3200
// zero changes              5116800
// row checks                  12841
// row merges                  17429
```
ratio: 17429 ⁄ 3200 = 5.4465625
rows: 3200 ⁄ 200 = 16
row checks: 12841 ⁄ 811 = 15.8335388409
row merges: 17429 ⁄ 1049 = 16.614871306

## Sparse Encoding

11 clauses:

```// rows                         76
// zero changes               2812
// row checks                  327
// row merges                  379
```
ratio: 379 ⁄ 76 = 4.98684210526
rows: 200 ⁄ 76 = 2.63157894737
row checks: 811 ⁄ 327 = 2.48012232416
row merges: 1049 ⁄ 379 = 2.76781002639

## Very Sparse Encoding

29 clauses, 11 variables:

```// rows                       58
// zero changes             1624
// row checks                243
// row merges                292
```
ratio: 292 ⁄ 58 = 5.03448275862
rows: 200 ⁄ 58 = 3.44827586207
row checks: 811 ⁄ 243 = 3.33744855967
row merges: 1049 ⁄ 292 = 3.59246575342
```a = b = c = d = !f = g = h = p = q = r
```

## Mapping With Variables

10 clauses:

```// rows                        240
// zero changes              28560
// row checks                  972
// row merges                 1358
```
ratio: 1358 ⁄ 240 = 5.65833333333

20 clauses:

```// rows                        880
// soft changes             386320
// row checks                 3542
// row merges                 5128
```
ratio: 5128 ⁄ 880 = 5.82727272727
rows: 880 ⁄ 240 = 3.66666666667
row checks: 3542 ⁄ 972 = 3.64403292181
row merges: 5128 ⁄ 1358 = 3.77614138439

40 clauses:

```// rows                         3360
// zero changes              5641440
// row checks                  13482
// row merges                  19868
```
ratio: 19868 ⁄ 3360 = 5.9130952381
rows: 3360 ⁄ 240 = 14
row checks: 13482 ⁄ 972 = 13.8703703704
row merges: 19868 ⁄ 1358 = 14.6303387334

## Running Times

```// rows                       240
//  |:TIM:|  processed      : [2013-10-29 19:48:52.164039] step: [0:00:00.041764] total: [0:00:00.214489]

// rows                       880
//  |:TIM:|  processed      : [2013-10-29 19:49:10.427168] step: [0:00:00.329501] total: [0:00:02.982316]
| rows:       880 / 240 = 3.66666666667
| time:       2.982316 / 0.214489 = 13.9042841358

// rows                       3360
//  |:TIM:|  processed      : [2013-10-29 19:50:12.472748] step: [0:00:05.101761] total: [0:00:46.632018]
| rows:       3360 / 880 = 3.81818181818
| time:       46.632018 / 2.982316 = 15.6361760457

Input factor | Time factor
-------------+------------
3.6          | 13 = n^2
3.8          | 15 = n^2
```