XOR Analysis

Author:	Wolfgang Scherer

Contents

Base Problem

Partial problem extracted from mod2-3cage-unsat-9-10.

Boolean Formula

( ¬a0 ∨ ¬a1 ∨ ¬a2 ) ∧
( ¬a0 ∨  a1 ∨  a2 ) ∧
(  a0 ∨ ¬a1 ∨  a2 ) ∧
(  a0 ∨  a1 ∨ ¬a2 ) ∧
( ¬a0 ∨ ¬b1 ∨ ¬b2 ) ∧
( ¬a0 ∨  b1 ∨  b2 ) ∧
(  a0 ∨ ¬b1 ∨  b2 ) ∧
(  a0 ∨  b1 ∨ ¬b2 ) ∧
( ¬a1 ∨ ¬c1 ∨ ¬c2 ) ∧
( ¬a1 ∨  c1 ∨  c2 ) ∧
(  a1 ∨ ¬c1 ∨  c2 ) ∧
(  a1 ∨  c1 ∨ ¬c2 ) ∧
( ¬a2 ∨ ¬d1 ∨ ¬d2 ) ∧
( ¬a2 ∨  d1 ∨  d2 ) ∧
(  a2 ∨ ¬d1 ∨  d2 ) ∧
(  a2 ∨  d1 ∨ ¬d2 ) ∧
( ¬b1 ∨ ¬e1 ∨ ¬e2 ) ∧
( ¬b1 ∨  e1 ∨  e2 ) ∧
(  b1 ∨ ¬e1 ∨  e2 ) ∧
(  b1 ∨  e1 ∨ ¬e2 ) ∧
( ¬b2 ∨ ¬f1 ∨ ¬f2 ) ∧
( ¬b2 ∨  f1 ∨  f2 ) ∧
(  b2 ∨ ¬f1 ∨  f2 ) ∧
(  b2 ∨  f1 ∨ ¬f2 )

Clause Vectors

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

Basic Mapping Without Conflict Maximization

001-3XOR-variable.v-000.png

Basic Mapping With Conflict Maximization

001-3XOR-variable.x.v-000.png

Combine 4-SAT Clauses

001-3XOR-variable.x.v-001.png

Remove Covered 3-SAT Clauses

001-3XOR-variable.x.v-002.png

Create CNF of DNF

This restores the matrix, when mapped.

The flattened clause vectors are identical to the orginal CNF problem.

[ // OR
  [ 0 1 1 _ _ _ _ _ _ _ _ _ _ ] // AND
  [ 0 0 0 _ _ _ _ _ _ _ _ _ _ ] // AND
  [ 1 1 0 _ _ _ _ _ _ _ _ _ _ ] // AND
  [ 1 0 1 _ _ _ _ _ _ _ _ _ _ ] // AND
]
[ // OR
  [ 0 _ _ 1 1 _ _ _ _ _ _ _ _ ] // AND
  [ 0 _ _ 0 0 _ _ _ _ _ _ _ _ ] // AND
  [ 1 _ _ 1 0 _ _ _ _ _ _ _ _ ] // AND
  [ 1 _ _ 0 1 _ _ _ _ _ _ _ _ ] // AND
]
[ // OR
  [ _ 0 _ _ _ 1 1 _ _ _ _ _ _ ] // AND
  [ _ 0 _ _ _ 0 0 _ _ _ _ _ _ ] // AND
  [ _ 1 _ _ _ 1 0 _ _ _ _ _ _ ] // AND
  [ _ 1 _ _ _ 0 1 _ _ _ _ _ _ ] // AND
]
[ // OR
  [ _ _ 0 _ _ _ _ 1 1 _ _ _ _ ] // AND
  [ _ _ 0 _ _ _ _ 0 0 _ _ _ _ ] // AND
  [ _ _ 1 _ _ _ _ 1 0 _ _ _ _ ] // AND
  [ _ _ 1 _ _ _ _ 0 1 _ _ _ _ ] // AND
]
[ // OR
  [ _ _ _ 0 _ _ _ _ _ 1 1 _ _ ] // AND
  [ _ _ _ 0 _ _ _ _ _ 0 0 _ _ ] // AND
  [ _ _ _ 1 _ _ _ _ _ 1 0 _ _ ] // AND
  [ _ _ _ 1 _ _ _ _ _ 0 1 _ _ ] // AND
]
[ // OR
  [ _ _ _ _ 0 _ _ _ _ _ _ 1 1 ] // AND
  [ _ _ _ _ 0 _ _ _ _ _ _ 0 0 ] // AND
  [ _ _ _ _ 1 _ _ _ _ _ _ 1 0 ] // AND
  [ _ _ _ _ 1 _ _ _ _ _ _ 0 1 ] // AND
]
    a a a b b c c d d e e f f
    0 1 2 1 2 1 2 1 2 1 2 1 2

Why Is This Non-Trivial?

When the satoku matrix is encoded in selection normal form (SNF), the structural information (XOR variables) is lost.

However, mapping of the SNF problem properly restores the original conflict situation.

Since the SNF problem is a boolean satisfiability problem in its own right, it cannot be simply dismissed as irrelevant.

Running a SAT-solver with different problem encodings shows a significant difference in running time for structured problems.

The conflict situation is invariant for the chosen problem encodings and the satoku matrix reflects this fact. Note, that there are also problem transformations, which do not result in the same satoku matrix. Whether the effective m-complexity is also affected remains to be researched.

MiniSAT and SNF

The unsatisfiable bipartite XOR problem mod2-3cage-unsat-9-10 is solved (unsatisfiability is detected) by MiniSAT in 32.082 seconds in its original encoding.

The number of decisions is between 2²³ and 2²⁴ :

==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |     232      696 |      77       0        0     nan |  0.000 % |
|       100 |     232      696 |      84     100     1823    18.2 |  0.013 % |
|       251 |     232      696 |      93     132     1925    14.6 |  0.013 % |
|       477 |     232      696 |     102      91     1132    12.4 |  0.013 % |
|       814 |     232      696 |     112     139     1844    13.3 |  0.013 % |
|      1320 |     232      696 |     124     116     1428    12.3 |  0.013 % |
|      2079 |     232      696 |     136      95     1165    12.3 |  0.013 % |
|      3218 |     232      696 |     150     149     2035    13.7 |  0.013 % |
|      4926 |     232      696 |     165     145     2098    14.5 |  0.013 % |
|      7488 |     232      696 |     181     120     1561    13.0 |  0.013 % |
|     11332 |     232      696 |     199     169     2534    15.0 |  0.013 % |
|     17099 |     232      696 |     219     155     1878    12.1 |  0.013 % |
|     25748 |     232      696 |     241     141     1708    12.1 |  0.013 % |
|     38723 |     232      696 |     265     261     3340    12.8 |  0.013 % |
|     58185 |     232      696 |     292     251     3162    12.6 |  0.013 % |
|     87377 |     232      696 |     321     305     4116    13.5 |  0.013 % |
|    131167 |     232      696 |     353     182     2295    12.6 |  0.013 % |
|    196852 |     232      696 |     389     236     2756    11.7 |  0.013 % |
|    295379 |     232      696 |     428     362     4849    13.4 |  0.013 % |
|    443168 |     232      696 |     470     305     3873    12.7 |  0.013 % |
|    664851 |     232      696 |     518     389     4560    11.7 |  0.013 % |
|    997376 |     232      696 |     569     499     6237    12.5 |  0.013 % |
|   1496165 |     232      696 |     626     314     3871    12.3 |  0.013 % |
|   2244348 |     232      696 |     689     589     8167    13.9 |  0.014 % |
|   3366623 |     233      696 |     758     665     8210    12.3 |  0.027 % |
|   5050035 |     229      684 |     834     482     5464    11.3 |  1.163 % |
==============================================================================
restarts              : 26
conflicts             : 6516168        (203110 /sec)
decisions             : 9885877        (308144 /sec)
propagations          : 92282116       (2876445 /sec)
conflict literals     : 87119249       (19.39 % deleted)
Memory used           : 2.05 MB
CPU time              : 32.082 s

UNSATISFIABLE

The SNF of mod2-3cage-unsat-9-10 with conflict maximization looses the XOR variables but contains enough conflict information, so that MiniSAT can solve it in 22761.1 seconds.

The number of decisions is almost 2²⁹ , which is the worst-case expectation of both n-comlexity and m-complexity:

==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    1730     3576 |     576       0        0     nan |  0.000 % |
|       101 |    1730     3576 |     633     101     2881    28.5 |  0.001 % |
|       252 |    1731     3576 |     696     251     6098    24.3 |  0.001 % |
|       478 |    1734     3576 |     766     474    10979    23.2 |  0.001 % |
|       816 |    1738     3576 |     843     808    19184    23.7 |  0.001 % |
|      1324 |    1740     3576 |     927     777    20474    26.4 |  0.001 % |
|      2083 |    1751     3576 |    1020    1038    25913    25.0 |  0.002 % |
|      3223 |    1754     3576 |    1122    1026    22338    21.8 |  0.001 % |
|      4931 |    1774     3576 |    1234     816    21661    26.5 |  0.001 % |
|      7493 |    1784     3576 |    1358    1285    36315    28.3 |  0.001 % |
|     11337 |    1791     3576 |    1493    1460    42005    28.8 |  0.001 % |
|     17103 |    1800     3576 |    1643    1581    50885    32.2 |  0.001 % |
|     25753 |    1807     3576 |    1807    1542    42402    27.5 |  0.001 % |
|     38730 |    1830     3576 |    1988    1060    27313    25.8 |  0.001 % |
|     58192 |    1842     3576 |    2187    1161    29061    25.0 |  0.001 % |
|     87385 |    1861     3576 |    2406    1229    31548    25.7 |  0.001 % |
|    131174 |    1879     3576 |    2646    1724    45714    26.5 |  0.001 % |
|    196858 |    1887     3576 |    2911    2024    66899    33.1 |  0.001 % |
|    295386 |    1895     3576 |    3202    1750    58822    33.6 |  0.001 % |
|    443175 |    1916     3576 |    3522    3059   104660    34.2 |  0.001 % |
|    664859 |    1933     3576 |    3875    2945   102476    34.8 |  0.001 % |
|    997385 |    1945     3576 |    4262    2460    85460    34.7 |  0.001 % |
|   1496176 |    1949     3576 |    4688    2275    80916    35.6 |  0.001 % |
|   2244358 |    1953     3576 |    5157    2566    88599    34.5 |  0.001 % |
|   3366632 |    1954     3576 |    5673    3564   120184    33.7 |  0.001 % |
|   5050045 |    1954     3576 |    6240    3859   121915    31.6 |  0.001 % |
|   7575162 |    1960     3576 |    6864    4065   152471    37.5 |  0.001 % |
|  11362839 |    1960     3576 |    7551    6923   219702    31.7 |  0.007 % |
|  17044352 |    1960     3576 |    8306    6207   177760    28.6 |  0.007 % |
|  25566625 |    1960     3576 |    9137    5991   215173    35.9 |  0.001 % |
|  38350028 |    1960     3576 |   10050    5453   187002    34.3 |  0.001 % |
|  57525135 |    1960     3576 |   11055    9157   344012    37.6 |  0.001 % |
|  86287793 |    1960     3576 |   12161    8826   301639    34.2 |  0.001 % |
| 129431781 |    1960     3576 |   13377   11976   461638    38.5 |  0.007 % |
| 194147763 |    1960     3576 |   14715    9009   339113    37.6 |  0.001 % |
| 291221737 |    1960     3576 |   16187   13619   520440    38.2 |  0.001 % |
| 436832698 |    1961     3576 |   17805   11715   422829    36.1 |  0.012 % |
==============================================================================
restarts              : 37
conflicts             : 492799432      (21651 /sec)
decisions             : 523453042      (22998 /sec)
propagations          : 32650223888    (1434474 /sec)
conflict literals     : 19118584028    (15.50 % deleted)
Memory used           : 28.08 MB
CPU time              : 22761.1 s

UNSATISFIABLE

The SNF of the unmaximized unsatisfiable XOR problem mod2-3cage-unsat-9-10 had not been solved after 9 days (when I decided to interrupt it):

==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    2320     4872 |     773       0        0     nan |  0.000 % |
|       100 |    2320     4872 |     850     100     2696    27.0 |  0.000 % |
|       250 |    2320     4872 |     935     250     7730    30.9 |  0.000 % |
|       475 |    2320     4872 |    1028     475    15025    31.6 |  0.000 % |
|       813 |    2320     4872 |    1131     813    26086    32.1 |  0.000 % |
|      1322 |    2320     4872 |    1244    1322    40334    30.5 |  0.000 % |
|      2081 |    2320     4872 |    1369     783    18378    23.5 |  0.000 % |
|      3220 |    2320     4872 |    1506    1108    31069    28.0 |  0.000 % |
|      4929 |    2320     4872 |    1656    1230    32439    26.4 |  0.000 % |
|      7492 |    2320     4872 |    1822    1874    64202    34.3 |  0.000 % |
|     11336 |    2320     4872 |    2004    1689    54535    32.3 |  0.000 % |
|     17102 |    2320     4872 |    2205    2206    92348    41.9 |  0.000 % |
|     25752 |    2320     4872 |    2426    1703    65328    38.4 |  0.000 % |
|     38727 |    2320     4872 |    2668    1945    77118    39.6 |  0.000 % |
|     58188 |    2320     4872 |    2935    1915    71077    37.1 |  0.000 % |
|     87382 |    2320     4872 |    3229    2012    76019    37.8 |  0.000 % |
|    131173 |    2320     4872 |    3551    2072    75605    36.5 |  0.000 % |
|    196858 |    2320     4872 |    3907    2105    72181    34.3 |  0.000 % |
|    295385 |    2320     4872 |    4297    3485   127768    36.7 |  0.000 % |
|    443174 |    2320     4872 |    4727    3926   177139    45.1 |  0.000 % |
|    664860 |    2320     4872 |    5200    4542   209943    46.2 |  0.000 % |
|    997387 |    2320     4872 |    5720    3700   156595    42.3 |  0.000 % |
|   1496175 |    2320     4872 |    6292    4308   191208    44.4 |  0.000 % |
|   2244358 |    2320     4872 |    6921    3566   159429    44.7 |  0.000 % |
|   3366633 |    2320     4872 |    7613    4742   234022    49.4 |  0.000 % |
|   5050044 |    2320     4872 |    8375    7289   326987    44.9 |  0.000 % |
|   7575163 |    2320     4872 |    9212    7408   339034    45.8 |  0.000 % |
|  11362840 |    2320     4872 |   10134    5888   214951    36.5 |  0.000 % |
|  17044352 |    2320     4872 |   11147    6992   321011    45.9 |  0.000 % |
|  25566622 |    2320     4872 |   12262    7620   324590    42.6 |  0.000 % |
|  38350025 |    2320     4872 |   13488    9132   447983    49.1 |  0.000 % |
|  57525131 |    2320     4872 |   14837    8502   373241    43.9 |  0.000 % |
|  86287791 |    2320     4872 |   16320   12710   621498    48.9 |  0.000 % |
| 129431780 |    2320     4872 |   17953   14970   801196    53.5 |  0.000 % |
| 194147763 |    2320     4872 |   19748   10371   514816    49.6 |  0.000 % |
| 291221738 |    2320     4872 |   21723   13446   680208    50.6 |  0.000 % |
| 436832698 |    2320     4872 |   23895   12423   624677    50.3 |  0.000 % |
| 655249138 |    2320     4872 |   26285   13921   733198    52.7 |  0.000 % |
| 982873799 |    2320     4872 |   28913   16449   748971    45.5 |  0.000 % |
| 1474310791 |    2320     4872 |   31804   19079   886125    46.4 |  0.000 % |
| -2083501017 |    2320     4872 |   34985   23194  1083272    46.7 |  0.000 % |
| -977767784 |    2320     4872 |   38483   28154  1360430    48.3 |  0.000 % |
| 680832066 |    2320     4872 |   42332   17063   858971    50.3 |  0.000 % |
*** INTERRUPTED ***
restarts              : 43
conflicts             : 10835521721    (13930 /sec)
decisions             : 12838157330    (16504 /sec)
propagations          : 1071321181196   (1377230 /sec)
conflict literals     : 571262903478   (15.21 % deleted)
Memory used           : 147.38 MB
CPU time              : 777881 s
*** INTERRUPTED ***

The number of decisions is between 2³³ and 2³⁴ :

2^33 =       8589934592
2^34 =      17179869184
decisions:  12838157330

It seems, as if the solver is about to try all 2⁵⁸ variable combinations for detecting unsatisfiability.

Construct SNF

Selection normal form (SNF)[1]:

[ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 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 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ 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 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 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 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 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 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]
[ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 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 ]

Mapping With Conflict Maximization

This recovers the conflict situation. It does not recover the XOR structure.

005-3XOR-SNF.x-000.png

Mapping Without Conflict Maximization

This also does not recover the XOR structure, but it allows for reconstruction of the XOR variables.

005-3XOR-SNF-000-reduced.png

Note: The 2-SAT clause region in the above matrix is reduced.

For what it's worth, here is the boolean formula

(  l000 ∨  l001 ∨  l002 ) ∧
(  l010 ∨  l011 ∨  l012 ) ∧
(  l020 ∨  l021 ∨  l022 ) ∧
(  l030 ∨  l031 ∨  l032 ) ∧
(  l040 ∨  l041 ∨  l042 ) ∧
(  l050 ∨  l051 ∨  l052 ) ∧
(  l060 ∨  l061 ∨  l062 ) ∧
(  l070 ∨  l071 ∨  l072 ) ∧
(  l080 ∨  l081 ∨  l082 ) ∧
(  l090 ∨  l091 ∨  l092 ) ∧
(  l100 ∨  l101 ∨  l102 ) ∧
(  l110 ∨  l111 ∨  l112 ) ∧
(  l120 ∨  l121 ∨  l122 ) ∧
(  l130 ∨  l131 ∨  l132 ) ∧
(  l140 ∨  l141 ∨  l142 ) ∧
(  l150 ∨  l151 ∨  l152 ) ∧
(  l160 ∨  l161 ∨  l162 ) ∧
(  l170 ∨  l171 ∨  l172 ) ∧
(  l180 ∨  l181 ∨  l182 ) ∧
(  l190 ∨  l191 ∨  l192 ) ∧
(  l200 ∨  l201 ∨  l202 ) ∧
(  l210 ∨  l211 ∨  l212 ) ∧
(  l220 ∨  l221 ∨  l222 ) ∧
(  l230 ∨  l231 ∨  l232 ) ∧
( ¬l000 ∨ ¬l020 ) ∧
( ¬l000 ∨ ¬l030 ) ∧
( ¬l000 ∨ ¬l060 ) ∧
( ¬l000 ∨ ¬l070 ) ∧
( ¬l001 ∨ ¬l011 ) ∧
( ¬l001 ∨ ¬l031 ) ∧
( ¬l001 ∨ ¬l100 ) ∧
( ¬l001 ∨ ¬l110 ) ∧
( ¬l002 ∨ ¬l012 ) ∧
( ¬l002 ∨ ¬l022 ) ∧
( ¬l002 ∨ ¬l140 ) ∧
( ¬l002 ∨ ¬l150 ) ∧
( ¬l010 ∨ ¬l020 ) ∧
( ¬l010 ∨ ¬l030 ) ∧
( ¬l010 ∨ ¬l060 ) ∧
( ¬l010 ∨ ¬l070 ) ∧
( ¬l011 ∨ ¬l021 ) ∧
( ¬l011 ∨ ¬l080 ) ∧
( ¬l011 ∨ ¬l090 ) ∧
( ¬l012 ∨ ¬l032 ) ∧
( ¬l012 ∨ ¬l120 ) ∧
( ¬l012 ∨ ¬l130 ) ∧
( ¬l020 ∨ ¬l040 ) ∧
( ¬l020 ∨ ¬l050 ) ∧
( ¬l021 ∨ ¬l031 ) ∧
( ¬l021 ∨ ¬l100 ) ∧
( ¬l021 ∨ ¬l110 ) ∧
( ¬l022 ∨ ¬l032 ) ∧
( ¬l022 ∨ ¬l120 ) ∧
( ¬l022 ∨ ¬l130 ) ∧
( ¬l030 ∨ ¬l040 ) ∧
( ¬l030 ∨ ¬l050 ) ∧
( ¬l031 ∨ ¬l080 ) ∧
( ¬l031 ∨ ¬l090 ) ∧
( ¬l032 ∨ ¬l140 ) ∧
( ¬l032 ∨ ¬l150 ) ∧
( ¬l040 ∨ ¬l060 ) ∧
( ¬l040 ∨ ¬l070 ) ∧
( ¬l041 ∨ ¬l051 ) ∧
( ¬l041 ∨ ¬l071 ) ∧
( ¬l041 ∨ ¬l180 ) ∧
( ¬l041 ∨ ¬l190 ) ∧
( ¬l042 ∨ ¬l052 ) ∧
( ¬l042 ∨ ¬l062 ) ∧
( ¬l042 ∨ ¬l220 ) ∧
( ¬l042 ∨ ¬l230 ) ∧
( ¬l050 ∨ ¬l060 ) ∧
( ¬l050 ∨ ¬l070 ) ∧
( ¬l051 ∨ ¬l061 ) ∧
( ¬l051 ∨ ¬l160 ) ∧
( ¬l051 ∨ ¬l170 ) ∧
( ¬l052 ∨ ¬l072 ) ∧
( ¬l052 ∨ ¬l200 ) ∧
( ¬l052 ∨ ¬l210 ) ∧
( ¬l061 ∨ ¬l071 ) ∧
( ¬l061 ∨ ¬l180 ) ∧
( ¬l061 ∨ ¬l190 ) ∧
( ¬l062 ∨ ¬l072 ) ∧
( ¬l062 ∨ ¬l200 ) ∧
( ¬l062 ∨ ¬l210 ) ∧
( ¬l071 ∨ ¬l160 ) ∧
( ¬l071 ∨ ¬l170 ) ∧
( ¬l072 ∨ ¬l220 ) ∧
( ¬l072 ∨ ¬l230 ) ∧
( ¬l080 ∨ ¬l100 ) ∧
( ¬l080 ∨ ¬l110 ) ∧
( ¬l081 ∨ ¬l091 ) ∧
( ¬l081 ∨ ¬l111 ) ∧
( ¬l082 ∨ ¬l092 ) ∧
( ¬l082 ∨ ¬l102 ) ∧
( ¬l090 ∨ ¬l100 ) ∧
( ¬l090 ∨ ¬l110 ) ∧
( ¬l091 ∨ ¬l101 ) ∧
( ¬l092 ∨ ¬l112 ) ∧
( ¬l101 ∨ ¬l111 ) ∧
( ¬l102 ∨ ¬l112 ) ∧
( ¬l120 ∨ ¬l140 ) ∧
( ¬l120 ∨ ¬l150 ) ∧
( ¬l121 ∨ ¬l131 ) ∧
( ¬l121 ∨ ¬l151 ) ∧
( ¬l122 ∨ ¬l132 ) ∧
( ¬l122 ∨ ¬l142 ) ∧
( ¬l130 ∨ ¬l140 ) ∧
( ¬l130 ∨ ¬l150 ) ∧
( ¬l131 ∨ ¬l141 ) ∧
( ¬l132 ∨ ¬l152 ) ∧
( ¬l141 ∨ ¬l151 ) ∧
( ¬l142 ∨ ¬l152 ) ∧
( ¬l160 ∨ ¬l180 ) ∧
( ¬l160 ∨ ¬l190 ) ∧
( ¬l161 ∨ ¬l171 ) ∧
( ¬l161 ∨ ¬l191 ) ∧
( ¬l162 ∨ ¬l172 ) ∧
( ¬l162 ∨ ¬l182 ) ∧
( ¬l170 ∨ ¬l180 ) ∧
( ¬l170 ∨ ¬l190 ) ∧
( ¬l171 ∨ ¬l181 ) ∧
( ¬l172 ∨ ¬l192 ) ∧
( ¬l181 ∨ ¬l191 ) ∧
( ¬l182 ∨ ¬l192 ) ∧
( ¬l200 ∨ ¬l220 ) ∧
( ¬l200 ∨ ¬l230 ) ∧
( ¬l201 ∨ ¬l211 ) ∧
( ¬l201 ∨ ¬l231 ) ∧
( ¬l202 ∨ ¬l212 ) ∧
( ¬l202 ∨ ¬l222 ) ∧
( ¬l210 ∨ ¬l220 ) ∧
( ¬l210 ∨ ¬l230 ) ∧
( ¬l211 ∨ ¬l221 ) ∧
( ¬l212 ∨ ¬l232 ) ∧
( ¬l221 ∨ ¬l231 ) ∧
( ¬l222 ∨ ¬l232 )

Copyright

XOR Analysis

Base Problem

Boolean Formula

Clause Vectors

Basic Mapping Without Conflict Maximization

Basic Mapping With Conflict Maximization

Combine 4-SAT Clauses

Remove Covered 3-SAT Clauses

Create CNF of DNF

Why Is This Non-Trivial?

MiniSAT and SNF

Construct SNF

Mapping With Conflict Maximization

Mapping Without Conflict Maximization

Reduced Matrix For XOR Recovery

XOR Targets

XOR Recovery

XOR Recovery

XOR Recovery

XOR Recovery

XOR Recovery

XOR Recovery

XOR Recovery

XOR Recovery

XOR Recovery

XOR Recovery