Row Updates

Author: Wolfgang Scherer

Contents

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

010-all-clauses-identical.n-000.png

Satoku matrix without requirements update

Row update for selection row s00

Row update for selection row s00 , 1st pass

010-all-clauses-identical.n-001.png

Row update for selection row s00 , 1st pass

Row update for selection row s00 , 2nd pass

010-all-clauses-identical.n-002.png

Row update for selection row s00 , 2nd pass

Row update for selection row s00 , 3rd pass

010-all-clauses-identical.n-003.png

Row update for selection row s00 , 3rd pass

Row update for selection row s00 , 4th pass

010-all-clauses-identical.n-004.png

Row update for selection row s00 , 4th pass

Row update for selection row s00 , 6th pass

010-all-clauses-identical.n-005.png

Row update for selection row s00 , 6th pass

Row update for selection row s00 , 7th pass

010-all-clauses-identical.n-006.png

Row update for selection row s00 , 7th pass

Row update for selection row s00 , 8th pass

010-all-clauses-identical.n-007.png

Row update for selection row s00 , 8th pass

Row update for selection row s00 , 9th pass

010-all-clauses-identical.n-008.png

Row update for selection row s00 , 9th pass

Row updates for selection rows s01, s02

Row update for selection row s01

010-all-clauses-identical.n-009.png

Row update for selection row s01

Row update for selection row s02

010-all-clauses-identical.n-010.png

Row update for selection row s02

Row updates for clause submatrix S1

Row update for selection row s10

010-all-clauses-identical.n-011.png

Row update for selection row s10

Row update for s11

010-all-clauses-identical.n-012.png

Row update for s11

Row update for selection row s12

010-all-clauses-identical.n-013.png

Row update for selection row s12

Finish row updates

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

010-all-clauses-identical.n-014.png

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
zero updates 0
row updates 30
superset updates 63
max zero updates 0
max row updates 15
max superset updates 63
pending zero updates 0
pending row updates 0
pending superset updates 0
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
zero updates 0
row updates 30
superset updates 135
max zero updates 0
max row updates 15
max superset updates 135
pending zero updates 0
pending row updates 0
pending superset updates 0
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
zero updates 0
row updates 60
superset updates 570
max zero updates 0
max row updates 30
max superset updates 570
pending zero updates 0
pending row updates 0
pending superset updates 0
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 updates                 400
// superset updates            189
// row checks                  811
// row merges                 1049
ratio: 1049 ⁄ 200 = 5.245

20 clauses:

// rows                        800
// zero changes             319200
// row updates                1600
// superset updates            779
// 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 updates                  6400
// superset updates             3159
// 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 updates                 152
// superset updates             73
// 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 updates               116
// superset updates           52
// 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 updates                 480
// superset updates            231
// row checks                  972
// row merges                 1358
ratio: 1358 ⁄ 240 = 5.65833333333

20 clauses:

// rows                        880
// soft changes             386320
// row updates                1760
// superset updates            861
// 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 updates                  6720
// superset updates             3321
// 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

Copyright

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