This is the twentieth part of the Types and Programming Languages series. For your convenience you can find other parts in the table of contents in Part 1 — Do not return in finally

Sometimes you may ask yourself how hard you work. You could count the hours of work but we all know that some things are harder and some others are easier. One hour isn’t the same effort in different activities. Similarly, it’s easier to work when you’re not supervised and there is no time pressure. With deadlines ahead of you, the same amount of work now becomes harder and more stressful. Another factor is when you can do your work. Maybe you can work 24/7 and do it when you just feel like it, or maybe you need to stick to a strict schedule.

Being that said, there are many factors that affect “how hard” the work is. I was considering that recently and this is the formula I think works in my case. Let’s call this “Work Complexity Model”:

Let’s say that at your work you need to do coding, doc writing, and mentoring. Therefore, your set of activities would have these three elements. You then need to asses the cost of context switch which is your personal coefficient. It doesn’t matter per se and do not compare it with others. You can use it to compare your effort in different months when you move between projects or tasks.

Next, you need to decide on the period, for instance a single quarter.

Next, for each activity you need to measure how many increments you have. If you need to deliver your work at the end of the sprint, then you would have six increments (two increments each month). If you need to deliver something every day, then you would have ninety increments.

You then need to measure the size of the increment. Obviously, this is very subjective and it’s up to you to define how hard a particular piece of work is. Technically, this should be the amount of energy (physical and mental) you spent on the task. Since it’s hard to measure, you can just count the number of hours dedicated to the task and then multiply that by how intense and frustrating the work was.

Finally, you need to include the length of the timeframe to do the work. If you can work asynchronously 24/7, then your timeframe would be the whole period. If you can do your work during work days 9-5, then it’s just these working hours.

Let’s say that you can do coding 24/7, same for doc writing, but the mentoring you can do only on Mondays 9-5. You need to deliver your coding artifacts every other week, your doc writing twice a week, and your mentoring every Monday. Therefore, this would be your complexity over 3 months.

See that the formula has the following features:

• It shows that context switching has some cost that scales non-linearly with the number of activities
• Number of increments affects the result much more than the size of the increments. That’s because supervision tends to slow us much more
• The length of the timeframe is also included in the formula

It’s up to you what your values for C and S are. The goal of this formula is not to give you some absolute scale. It’s much more to compare your different projects to have some numbers showing you how hard it was, as we know that our memory misleads us often.

This is the twentieth fifth part of the Availability Anywhere series. For your convenience you can find other parts in the table of contents in Part 1 – Connecting to SSH tunnel automatically in Windows

Today we’re going to make our VR experience even better. This is continuation of the previous part.

As mentioned before, there are issues with ALT+TAB and WINDOWS key. I remapped CAPS LOCK to WINDOWS with PowerToys, but today we’re doing something better.

First, I was looking for a good full-size keyboard with touchpad that I could use with VR. The best thing I found is Perixx PERIBOARD-313. Touchpad is in some weird position but I got used to that. It has this irritating Fn key, lacks Right WINDOWS, and the space is quite short, but generally the keyboard is good enough.

However, it’s a wired keyboard. You can plug that into your VR headset and it works well. The keyboard has additional USB slots, so you can plug more devices to your VR this way. Still, we’d like to make it wireless. To do that, I’m using Bluetooth Adapter for Keyboard & Mouse (BT-500). This adapter has a couple of interesting features. First, it turns your wired keyboard or mouse into a wireless one. Second, it can remap keys on the fly, add macros, or have custom settings that you can switch between easily.

I’m using the adapter to remap Left WINDOWS to CAPS LOCK, and TAB to SCROLL LOCK. This is my setup:

map add l_com caps_lock
map add tab scroll_lock
save
reboot

Next, I remap CAPS LOCK to Left WINDOWS back using PowerToys. I do the same for SCROLL LOCK and TAB.

Finally, I use another adapter to turn any wired mouse into wireless one. You could go with Bluetooth mouse instead. With these things in place, I now have a “regular” wireless keyboard that I can use with VR. Even though it’s Android behind the scenes, all is just like a regular Windows laptop.

As a side note, I tried remapping keys to F13 and similar special keys. Unfortunately, Quest 3 doesn’t handle these properly and my remote machine I connect to over vSpatial doesn’t receive the keys.

This is the one hundred and sixth part of the ILP series. For your convenience you can find other parts in the table of contents in Part 1 – Boolean algebra

Let’s solve Golden Waste (Złoty Odpad) riddle. We have a board with golden coins on it. One of the coins is a starting point and is numbered 1. We need to go along the blue lines and collect all the coins with the following rules:

• we must collect a coin when we get to it
• when collecting a coin, we can either continue straight or turn left or right; we can’t turn around (do U turn)

Let’s solve that with ILP. The idea is as follows:

• We want to number coins from one to n (number of coins); we represent this number with a bitset (to make things faster)
• each coin has two bitsets indicating which direction we entered this coin (up, right, bottom, left) and which direction we left
• for each coin, we analyze all four directions and make sure that all coins on the path in that direction have either lower number (so they were collected earlier) or we entered the first coin with higher number from the correct direction

Let’s see the code:

public class Field {
	public IVariable[] DirectionIn {get;set;}
	public IVariable[] DirectionOut {get;set;}
	public IVariable[] Number {get;set;}
}

var board = new string[]{
	" X     X",
	"    X X ",
	"   XX X1",
	"X      X",
	"  XXXX  ",
	"X  XX   ",
	"    XX  ",
	"XXXX X  "
};

var numbersCount = board.SelectMany(line => line.Select(character => character)).Count(character => character != ' ');

var fields = board.Select(line => line.Select(f => f != ' ' ? new Field{
	DirectionIn = Enumerable.Range(0, 4).Select(i => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray(),
	DirectionOut = Enumerable.Range(0, 4).Select(i => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray(),
	Number = Enumerable.Range(0, numbersCount).Select(i => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray()
} : null).ToArray()).ToArray();

for(int row=0;row<board.Length;++row){
	for(int column=0;column<board[0].Length;++column){
		if(board[row][column] != ' '){
			var thisField = fields[row][column];
			
			// If this is one, then select it
			if(board[row][column] == '1'){
				thisField.Number[0].Set<Equal>(solver.FromConstant(1));
			}
			
			// Exactly one number
			solver.Set<Equal>(solver.FromConstant(1), solver.Operation<Addition>(thisField.Number));
			
			// Cannot turn around
			for(int direction=0;direction<4;++direction){
				thisField.DirectionIn[direction].Operation<Addition>(thisField.DirectionOut[direction]).Set<LessOrEqual>(solver.FromConstant(1));
			}
			
			// Exactly one direction in
			solver.Set<Equal>(solver.FromConstant(1), solver.Operation<Addition>(thisField.DirectionIn));
			
			// Exactly one direction out
			solver.Set<Equal>(solver.FromConstant(1), solver.Operation<Addition>(thisField.DirectionOut));
			
			// Either this is last fields
			// Or there is some other field with value + 1  and input direction matching output direction
			// 0 going up, 1 going right, 2 going down, 3 going left
			var isNotLastField = thisField.Number[numbersCount-1].Operation<BinaryNegation>();
			
			Func<Field, IVariable> numberHash = f => solver.Operation<Addition>(
				Enumerable.Range(0, numbersCount).Select(p => solver.Operation<Multiplication>(f.Number[p], solver.FromConstant(p))).ToArray()
			);
			
			Func<Field, int, int, int, IVariable, IVariable> matchField = (localThis, r, c, directionIn, shouldCarryOn) => {
				if(board[r][c] != ' '){
					var thatField = fields[r][c];
					
					var isLowerNumber = solver.Operation<IsLessOrEqual>(
						numberHash(thatField),
						numberHash(localThis)
					);
					
					var isNextNumber = solver.Operation<IsEqual>(
						solver.Operation<Addition>(solver.FromConstant(1), numberHash(localThis)),
						numberHash(thatField)
					);
					
					var isDirectionInMatching = thatField.DirectionIn[directionIn];
					
					solver.Set<Equal>(
						solver.FromConstant(1),
						solver.Operation<MaterialImplication>(
							solver.Operation<Conjunction>(shouldCarryOn),
							solver.Operation<Disjunction>(
								isLowerNumber,
								solver.Operation<Conjunction>(isNextNumber, isDirectionInMatching)
							)
						)
					);
					
					return solver.Operation<Conjunction>(shouldCarryOn, isLowerNumber);
				}
				
				return shouldCarryOn;
			};
			
			IVariable shouldContinue;
			
			// Going up
			shouldContinue = thisField.DirectionOut[0].Operation<Conjunction>(isNotLastField);
			for(int row2 = row-1;row2>=0;--row2){
				shouldContinue = shouldContinue.Operation<Conjunction>(matchField(thisField, row2, column, 2, shouldContinue));
			}
			shouldContinue.Set<Equal>(solver.FromConstant(0));
			
			// Going down
			shouldContinue = thisField.DirectionOut[2].Operation<Conjunction>(isNotLastField);
			for(int row2 = row+1;row2<board.Length;++row2){
				shouldContinue = shouldContinue.Operation<Conjunction>(matchField(thisField, row2, column, 0, shouldContinue));
			}
			shouldContinue.Set<Equal>(solver.FromConstant(0));
			
			// Going left
			shouldContinue = thisField.DirectionOut[3].Operation<Conjunction>(isNotLastField);
			for(int column2=column-1;column2>=0;--column2){
				shouldContinue = shouldContinue.Operation<Conjunction>(matchField(thisField, row, column2, 1, shouldContinue));
			}
			shouldContinue.Set<Equal>(solver.FromConstant(0));
			
			// Going right
			shouldContinue = thisField.DirectionOut[1].Operation<Conjunction>(isNotLastField);
			for(int column2=column+1;column2<board[0].Length;++column2){
				shouldContinue = shouldContinue.Operation<Conjunction>(matchField(thisField, row, column2, 3, shouldContinue));
			}
			shouldContinue.Set<Equal>(solver.FromConstant(0));
		}
	}
}

// All numbers are different
for(int number=0;number<numbersCount;++number){
	solver.Operation<Addition>(fields.SelectMany(f => f).Where(f => f != null).Select(f => f.Number[number]).ToArray()).Set<Equal>(solver.FromConstant(1));
}

solver.AddGoal("goal", solver.FromConstant(0));
solver.Solve();

for(int row=0;row<board.Length;++row){
	for(int column=0;column<board.Length;++column){
		if(board[row][column] != ' '){
			var thisField = fields[row][column];
			
			for(int number=0;number<numbersCount;++number){
				if(solver.GetValue(thisField.Number[number]) > 0){
					Console.Write((number < 9 ? " " : "") + (number + 1) + " ");
				}
			}
		}else{
			Console.Write("   ");
		}
	}
	Console.WriteLine();
}

First, we define our coin class (lines 1-5). Next, we define a starting board (lines 7-16). We also count the number of coins (18) and then initialize variables (20-24).

Next, we iterate over all fields (26) and look for coins (28). We hardcode the starting point (31-34). Next, we make sure that the bitset indicating the number has exactly one value (36-37), that we can’t exit the coin to go back (to the U-turn) (39-42), and that there is exactly one input direction and output direction (44-48).

Now, we encode the main part. We first store a variable indicating whether this is the last coin to collect (53). We define a helper variable that will decode number bitset into a single integer so we can compare them easily (55-57). Finally, we encode the main function that builds the path.

The idea is: we start from some coin localThis and we check other fields along some straight line. When we spot another coin, we calculate if it has lower number (and was collected earlier) (63), or is exactly next to be collected (68-71), and that we entered from the right direction (73). We then enforce this with material implication (75-84). Finally, we return the flag indicating whether we should continue looking along this path (lines 86, 89).

We then use this function in four directions: (94-99, 101-106, 108-113, 115-120). Finally, we just make sure that all coins have different numbers (125-128) and solve the problem. Output:

Tried aggregator 3 times.
MIP Presolve eliminated 1270 rows and 609 columns.
MIP Presolve modified 33469 coefficients.
Aggregator did 895 substitutions.
Reduced MIP has 1886 rows, 1454 columns, and 32267 nonzeros.
Reduced MIP has 1454 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.06 sec. (89.01 ticks)
Probing time = 0.00 sec. (4.29 ticks)
Tried aggregator 1 time.
Reduced MIP has 1886 rows, 1454 columns, and 32267 nonzeros.
Reduced MIP has 1454 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.02 sec. (11.67 ticks)
Probing time = 0.00 sec. (4.28 ticks)
Clique table members: 2759.
MIP emphasis: balance optimality and feasibility.
MIP search method: dynamic search.
Parallel mode: deterministic, using up to 12 threads.
Root relaxation solution time = 0.05 sec. (52.10 ticks)

        Nodes                                         Cuts/
   Node  Left     Objective  IInf  Best Integer    Best Bound    ItCnt     Gap

      0     0        0.0000   508                      0.0000      874
      0     0        0.0000   481                   Cuts: 238     1192
      0     0        0.0000   580                   Cuts: 410     2048
      0     0        0.0000   532                   Cuts: 192     2580
      0     0        0.0000   660                   Cuts: 498     3396
      0     2        0.0000   263                      0.0000     3400
Elapsed time = 2.36 sec. (2430.37 ticks, tree = 0.01 MB, solutions = 0)
     25    27        0.0000   372                      0.0000     9792
    182   146        0.0000   480                      0.0000    34215
    360   218        0.0000   359                      0.0000    59248
    473   275        0.0000   382                      0.0000    86080
    630   392        0.0000   392                      0.0000   102841
    961   441    infeasible                            0.0000   127669
   1029   455    infeasible                            0.0000   146053
   1149   479        0.0000   408                      0.0000   163289
   1216   540        0.0000   440                      0.0000   176188
   1551   579    infeasible                            0.0000   232730
Elapsed time = 5.97 sec. (5824.01 ticks, tree = 0.56 MB, solutions = 0)
   1690   585    infeasible                            0.0000   289363
   1805   601        0.0000   515                      0.0000   325263
   1983   602        0.0000   477                      0.0000   373383
   2124   600        0.0000   455                      0.0000   431960
   2316   589    infeasible                            0.0000   490860
   2546   600        0.0000   570                      0.0000   544653
   2586   598        0.0000   562                      0.0000   584681
   2750   632    infeasible                            0.0000   643752
   2914   652    infeasible                            0.0000   681857
   3119   652        0.0000   679                      0.0000   725066
Elapsed time = 22.92 sec. (18464.39 ticks, tree = 1.39 MB, solutions = 0)
   3251   658        0.0000   695                      0.0000   811097
   3287   656    infeasible                            0.0000   849022
   3404   681        0.0000   528                      0.0000   907778
   3484   695    infeasible                            0.0000   930758
   3586   721        0.0000   648                      0.0000   954548
   3874   774        0.0000   588                      0.0000  1014376
   4009   807        0.0000   444                      0.0000  1049944
   4065   821        0.0000   502                      0.0000  1069917
   4327   865        0.0000   407                      0.0000  1144971
   4367   877        0.0000   521                      0.0000  1160531
Elapsed time = 39.03 sec. (29642.77 ticks, tree = 1.74 MB, solutions = 0)
   4472   910        0.0000   417                      0.0000  1190811
   4763   909    infeasible                            0.0000  1275674
   4797   921        0.0000   475                      0.0000  1295329
   4821   935        0.0000   481                      0.0000  1312840
   4857   949        0.0000   508                      0.0000  1332501
   4918   960        0.0000   520                      0.0000  1392387
   5005   997        0.0000   455                      0.0000  1432805
   5072  1020        0.0000   594                      0.0000  1448193
   5160  1040        0.0000   321                      0.0000  1479499
   5246  1048        0.0000   398                      0.0000  1504146
Elapsed time = 54.63 sec. (42147.18 ticks, tree = 2.13 MB, solutions = 0)
   5426  1124        0.0000   423                      0.0000  1544836
   5711  1181    infeasible                            0.0000  1604289
   5787  1158    infeasible                            0.0000  1631589
   5850  1169        0.0000   595                      0.0000  1655718
   5966  1183        0.0000   596                      0.0000  1695224
   6145  1204        0.0000   611                      0.0000  1770821
   6253  1242        0.0000   595                      0.0000  1814478
   6279  1244    infeasible                            0.0000  1843727
   6318  1247    infeasible                            0.0000  1878957
   6342  1249    infeasible                            0.0000  1894346
Elapsed time = 70.39 sec. (54490.95 ticks, tree = 3.57 MB, solutions = 0)
   6453  1240        0.0000   653                      0.0000  1946631
   6764  1281        0.0000   556                      0.0000  2047656
   6804  1283    infeasible                            0.0000  2063706
   6864  1299    infeasible                            0.0000  2080575
   7032  1340        0.0000   404                      0.0000  2123133
   7164  1346        0.0000   386                      0.0000  2158194
   7320  1336        0.0000   389                      0.0000  2205352
   7598  1302        0.0000   492                      0.0000  2275263
   7824  1294        0.0000   386                     -0.0000  2350430
   7831  1300        0.0000   442                     -0.0000  2352517
Elapsed time = 93.77 sec. (77852.80 ticks, tree = 58.94 MB, solutions = 0)
   7850  1311        0.0000   404                     -0.0000  2355298
   7923   969        0.0000   442                     -0.0000  2366582
   8187   689        0.0000   402                     -0.0000  2400804
   8559   412        0.0000   318                     -0.0000  2435661
   8948   389    infeasible                           -0.0000  2470993
   9576   476        0.0000   330                     -0.0000  2520604
  10159   477        0.0000   334                     -0.0000  2579870
  10555   518        0.0000   303                     -0.0000  2618541
  10930   518        0.0000   303                     -0.0000  2664466
  11282   519        0.0000   418                     -0.0000  2711235
Elapsed time = 103.23 sec. (87766.62 ticks, tree = 1.00 MB, solutions = 0)
  11651   566        0.0000   366                     -0.0000  2758926
  11693   565        0.0000   380                     -0.0000  2764222
  12058   290        0.0000   402                     -0.0000  2801170
  12633   230    infeasible                           -0.0000  2865597
  13570   230        0.0000   239                     -0.0000  2948118
  14733   263    infeasible                           -0.0000  3061474
  15820   202        0.0000   287                     -0.0000  3169807
  17003   275        0.0000   300                     -0.0000  3281567
  17989   304        0.0000   216                     -0.0000  3379704
  19041   267        0.0000   359                     -0.0000  3481728
Elapsed time = 116.88 sec. (103305.54 ticks, tree = 0.03 MB, solutions = 0)
  20430   274    infeasible                           -0.0000  3627297
  21450   423        0.0000   302                     -0.0000  3711606
  23285   375        0.0000   276                     -0.0000  3861744
  24549   281    infeasible                           -0.0000  3979235
  26136   435        0.0000   218                     -0.0000  4127636
  27561   391        0.0000   288                     -0.0000  4249779
  29100   424        0.0000   240                     -0.0000  4376829
  30874   439        0.0000   277                     -0.0000  4524167
  32176   415        0.0000   317                     -0.0000  4638570
  33981   443        0.0000   303                     -0.0000  4798347
Elapsed time = 128.17 sec. (112887.60 ticks, tree = 0.05 MB, solutions = 0)
  35594   351        0.0000   374                     -0.0000  4933169
  36777   478        0.0000   341                     -0.0000  5045144
  38466   458        0.0000   241                     -0.0000  5209098
  39471   471        0.0000   314                     -0.0000  5311307
  41132   528        0.0000   166                     -0.0000  5465492
  42639   520    infeasible                           -0.0000  5596801
  44371   393    infeasible                           -0.0000  5747683
  45828   546        0.0000   318                     -0.0000  5889722
  47025   530        0.0000   263                     -0.0000  6007087
  52571   586    infeasible                           -0.0000  6553399
Elapsed time = 142.38 sec. (125333.77 ticks, tree = 0.08 MB, solutions = 0)
  58950   670        0.0000   353                     -0.0000  7130024
  64631   643        0.0000   281                     -0.0000  7646642
  69621   603    infeasible                           -0.0000  8169867
  74350   602        0.0000   264                     -0.0000  8669095
  80366   715        0.0000   176                     -0.0000  9230184
  85904   475        0.0000   319                     -0.0000  9771470
  91692   502        0.0000   316                     -0.0000 10317244
  97439   608        0.0000   262                     -0.0000 10808574
 103409   594        0.0000   155                     -0.0000 11361920
 109112   645    infeasible                           -0.0000 11891245
Elapsed time = 186.53 sec. (163579.26 ticks, tree = 0.06 MB, solutions = 0)
 114282   994    infeasible                           -0.0000 12422478
 119356   803    infeasible                           -0.0000 12941160
 125898   915        0.0000   273                     -0.0000 13509013
 132155   881        0.0000   262                     -0.0000 14064545
 137866   886    infeasible                           -0.0000 14590510
 143707   914        0.0000   288                     -0.0000 15177172
 149235   807        0.0000   285                     -0.0000 15701530
 154911   675        0.0000   178                     -0.0000 16241618
 161882   821        0.0000   201                     -0.0000 16817652
 169771   823        0.0000   294                     -0.0000 17381212
Elapsed time = 245.55 sec. (201783.67 ticks, tree = 0.09 MB, solutions = 0)
 177104   765        0.0000   153                     -0.0000 17960080
 184942   821        0.0000   317                     -0.0000 18569902
 192554   749        0.0000   260                     -0.0000 19131939
 198295   787        0.0000   244                     -0.0000 19644341
 204161   727        0.0000   203                     -0.0000 20187350
 210163   575        0.0000   188                     -0.0000 20746953
 217540   898        0.0000   223                     -0.0000 21304646
 224070   780    infeasible                           -0.0000 21843454
 230533   820        0.0000   263                     -0.0000 22406991
 236733   779        0.0000   272                     -0.0000 22960102
Elapsed time = 300.91 sec. (240013.77 ticks, tree = 0.07 MB, solutions = 0)
 242658   745    infeasible                           -0.0000 23514500
 247652   787        0.0000   344                     -0.0000 24030942
 252764   942    infeasible                           -0.0000 24564913
 258233   961        0.0000   325                     -0.0000 25099913
 263573   874        0.0000   322                     -0.0000 25638923
 268963   864        0.0000   284                     -0.0000 26164593
 273168   887        0.0000   278                     -0.0000 26658456
 277901   886        0.0000   210                     -0.0000 27176495
 283861   956        0.0000   313                     -0.0000 27737094
 289071  1070    infeasible                           -0.0000 28251655
Elapsed time = 344.66 sec. (278234.91 ticks, tree = 0.14 MB, solutions = 0)
 293946  1036        0.0000   295                     -0.0000 28774451
 298674  1027        0.0000   270                     -0.0000 29314425
 304035   901        0.0000   291                     -0.0000 29855358
 308755  1004        0.0000   260                     -0.0000 30377899
 313952  1082        0.0000   182                     -0.0000 30884392
 319647  1011    infeasible                           -0.0000 31447232
 325025   962        0.0000   368                     -0.0000 31993586
 331144  1152    infeasible                           -0.0000 32537413
 336554  1085        0.0000   293                     -0.0000 33082843
 342745  1060        0.0000   310                     -0.0000 33644741
Elapsed time = 399.03 sec. (316477.28 ticks, tree = 0.09 MB, solutions = 0)
 348043  1070        0.0000   325                     -0.0000 34195498
 353051  1083    infeasible                           -0.0000 34733741
 357706  1092        0.0000   204                     -0.0000 35234117
 362868  1098        0.0000   396                     -0.0000 35793118
 367279  1060        0.0000   250                     -0.0000 36308791
 372233  1152        0.0000   240                     -0.0000 36828052
 377434  1040        0.0000   218                     -0.0000 37350915
 382616  1201        0.0000   283                     -0.0000 37889699
 387312  1104        0.0000   321                     -0.0000 38398280
 392225  1292        0.0000   250                     -0.0000 38920991
Elapsed time = 447.94 sec. (354693.45 ticks, tree = 0.12 MB, solutions = 0)
 397318  1139        0.0000   375                     -0.0000 39441204
 402948  1109        0.0000   301                     -0.0000 39988911
 408043  1211        0.0000   325                     -0.0000 40527949
 413033  1266    infeasible                           -0.0000 41021940
 418087  1259        0.0000   336                     -0.0000 41533403
 422935  1164        0.0000   238                     -0.0000 42063377
 427481  1148        0.0000   288                     -0.0000 42573987
 432508  1157        0.0000   310                     -0.0000 43081190
 437531  1104        0.0000   393                     -0.0000 43621012
 442498  1095    infeasible                           -0.0000 44152646
Elapsed time = 493.66 sec. (392931.47 ticks, tree = 0.11 MB, solutions = 0)
 447235  1243        0.0000   367                     -0.0000 44673781
 454167  1167        0.0000   364                     -0.0000 45252390
 459563  1358        0.0000   258                     -0.0000 45779187
 465352  1280        0.0000   276                     -0.0000 46357473
 470467  1164    infeasible                           -0.0000 46875991
 475439  1234        0.0000   351                     -0.0000 47413722
 480265  1176        0.0000   341                     -0.0000 47920454
 485190  1296        0.0000   308                     -0.0000 48445537
 489439  1203        0.0000   275                     -0.0000 48969330
 494417  1212    infeasible                           -0.0000 49473099
Elapsed time = 543.44 sec. (431141.50 ticks, tree = 0.11 MB, solutions = 0)
 499878  1134        0.0000   212                     -0.0000 50001890
 505210  1150        0.0000   348                     -0.0000 50541821
 510703  1177        0.0000   288                     -0.0000 51085904
 516296  1191        0.0000   315                     -0.0000 51627983
 522136  1340        0.0000   275                     -0.0000 52196564
 527818  1254    infeasible                           -0.0000 52747921
 533847  1184    infeasible                           -0.0000 53277168
 539496  1225        0.0000   267                     -0.0000 53838500
 545609  1258        0.0000   324                     -0.0000 54438657
 550950  1279        0.0000   239                     -0.0000 54978252
Elapsed time = 608.14 sec. (469350.48 ticks, tree = 0.11 MB, solutions = 0)
 556262  1247        0.0000   248                     -0.0000 55503690
 562223  1376        0.0000   353                     -0.0000 56086832
 567933  1384        0.0000   303                     -0.0000 56644010
 573375  1411        0.0000   201                     -0.0000 57189815
 578931  1373    infeasible                           -0.0000 57706883
 584688  1302        0.0000   337                     -0.0000 58273497
 590210  1307    infeasible                           -0.0000 58818386
 596342  1262        0.0000   400                     -0.0000 59389073
 601521  1501        0.0000   261                     -0.0000 59915960
 607666  1618        0.0000   316                     -0.0000 60463241
Elapsed time = 655.89 sec. (507553.95 ticks, tree = 0.14 MB, solutions = 0)
 613534  1464    infeasible                           -0.0000 61020365
 619827  1346    infeasible                           -0.0000 61571663
 625674  1185        0.0000   337                     -0.0000 62134994
 630902  1230    infeasible                           -0.0000 62649879
 636152  1269        0.0000   267                     -0.0000 63170593
 641404  1232    infeasible                           -0.0000 63717245
 647098  1131        0.0000   277                     -0.0000 64283791
 651991  1146        0.0000   280                     -0.0000 64792110
 657625  1102        0.0000   336                     -0.0000 65339290
 662514  1143        0.0000   288                     -0.0000 65886969
Elapsed time = 701.64 sec. (545809.44 ticks, tree = 0.10 MB, solutions = 0)
 667761   982    infeasible                           -0.0000 66435420
 672993   997    infeasible                           -0.0000 66975538
 678105   878        0.0000   333                     -0.0000 67497233
 684034   904        0.0000   243                     -0.0000 68064925
 688856  1029    infeasible                           -0.0000 68561991
 694528   996        0.0000   357                     -0.0000 69108002
 699668   949        0.0000   315                     -0.0000 69630518
 704198   991    infeasible                           -0.0000 70161775
 708775  1017        0.0000   359                     -0.0000 70646954
 713778  1124        0.0000   319                     -0.0000 71197164
Elapsed time = 753.45 sec. (584025.21 ticks, tree = 0.10 MB, solutions = 0)
 718098  1053    infeasible                           -0.0000 71697499
 722978  1157        0.0000   354                     -0.0000 72209736
 727746  1094    infeasible                           -0.0000 72707109
 732735  1208        0.0000   321                     -0.0000 73253307
 737382  1158        0.0000   262                     -0.0000 73777309
 741743  1186        0.0000   314                     -0.0000 74282073
 746089  1111        0.0000   231                     -0.0000 74770022
 750690  1071        0.0000   333                     -0.0000 75294136
 756570  1056        0.0000   183                     -0.0000 75849757
 761838   990    infeasible                           -0.0000 76384511
Elapsed time = 806.95 sec. (622255.57 ticks, tree = 0.09 MB, solutions = 0)
 766503  1047        0.0000   199                     -0.0000 76884595
 772155   973        0.0000   357                     -0.0000 77445968
 777804   905        0.0000   307                     -0.0000 78018695
 782798  1022        0.0000   255                     -0.0000 78543623
 787886   915        0.0000   354                     -0.0000 79080195
 792781   837        0.0000   207                     -0.0000 79607676
 798278   812        0.0000   288                     -0.0000 80149715
 804008   877        0.0000   352                     -0.0000 80674521
 810292   950        0.0000   221                     -0.0000 81234497
 816081  1096        0.0000   248                     -0.0000 81761078
Elapsed time = 864.78 sec. (660493.24 ticks, tree = 0.09 MB, solutions = 0)
 821608   981        0.0000   339                     -0.0000 82343536
 826874   806        0.0000   328                     -0.0000 82820634
 832016   757        0.0000   328                     -0.0000 83327447
 837482   787        0.0000   308                     -0.0000 83869680
 842139   731        0.0000   323                     -0.0000 84381411
 847060   783    infeasible                           -0.0000 84938335
 851915   664        0.0000   290                     -0.0000 85467634
 857317   674        0.0000   237                     -0.0000 85996304
 862563   625    infeasible                           -0.0000 86529643
 868267   601        0.0000   337                     -0.0000 87056256
Elapsed time = 919.34 sec. (698703.51 ticks, tree = 0.06 MB, solutions = 0)
 874538   564        0.0000   289                     -0.0000 87647117
 880183   486    infeasible                           -0.0000 88177720
 885096   474        0.0000   393                     -0.0000 88714039
 890118   478        0.0000   278                     -0.0000 89215217
 894929   452    infeasible                           -0.0000 89745753
 899775   557        0.0000   289                     -0.0000 90248578
 905044   588        0.0000   284                     -0.0000 90809349
 909687   539        0.0000   291                     -0.0000 91299572
 914621   535        0.0000   372                     -0.0000 91835448
 919578   534        0.0000   259                     -0.0000 92373542
Elapsed time = 979.02 sec. (736908.26 ticks, tree = 0.05 MB, solutions = 0)
 924284   528    infeasible                           -0.0000 92897665
 928973   614        0.0000   284                     -0.0000 93422898
 933775   525        0.0000   303                     -0.0000 93952475
 938738   533        0.0000   248                     -0.0000 94478367
 943372   431        0.0000   174                     -0.0000 94995204
 948523   447        0.0000   334                     -0.0000 95503630
 953489   585        0.0000   402                     -0.0000 96027542
 958414   528        0.0000   374                     -0.0000 96555477
 962500   423        0.0000   353                     -0.0000 97053906
 967184   482        0.0000   268                     -0.0000 97556109
Elapsed time = 1033.42 sec. (775159.19 ticks, tree = 0.05 MB, solutions = 0)
 971887   500        0.0000   316                     -0.0000 98087834
 975986   487        0.0000   300                     -0.0000 98569907
 980549   469    infeasible                           -0.0000 99091590
 985736   427    infeasible                           -0.0000 99606175
 990496   452    infeasible                           -0.0000 1.00e+008
 996024   427        0.0000   367                     -0.0000 1.01e+008
 1001487   326        0.0000   399                     -0.0000 1.01e+008
 1006410   393        0.0000   338                     -0.0000 1.02e+008
 1010756   381        0.0000   340                     -0.0000 1.02e+008
 1015858   393        0.0000   400                     -0.0000 1.03e+008
Elapsed time = 1085.41 sec. (813376.28 ticks, tree = 0.05 MB, solutions = 0)
 1021091   437        0.0000   279                     -0.0000 1.03e+008
 1027315   368        0.0000   253                     -0.0000 1.04e+008
 1032859   283        0.0000   261                     -0.0000 1.04e+008
 1037989   506        0.0000   315                     -0.0000 1.05e+008
 1043080   291        0.0000   329                     -0.0000 1.05e+008
 1048499   481        0.0000   238                     -0.0000 1.06e+008
 1054622   474    infeasible                           -0.0000 1.06e+008
 1059697   488    infeasible                           -0.0000 1.07e+008
 1065295   516        0.0000   215                     -0.0000 1.07e+008
 1070060   537        0.0000   293                     -0.0000 1.08e+008
Elapsed time = 1150.30 sec. (851586.95 ticks, tree = 0.16 MB, solutions = 0)
 1075283   516        0.0000   255                     -0.0000 1.08e+008
 1080812   392        0.0000   336                     -0.0000 1.09e+008
 1085879   298        0.0000   336                     -0.0000 1.10e+008
 1091175   558    infeasible                           -0.0000 1.10e+008
 1096144   557    infeasible                           -0.0000 1.11e+008
 1100783   505        0.0000   271                     -0.0000 1.11e+008
 1106516   471        0.0000   305                     -0.0000 1.12e+008
 1111268   484        0.0000   365                     -0.0000 1.12e+008
 1116540   569        0.0000   303                     -0.0000 1.13e+008
 1121296   601        0.0000   299                     -0.0000 1.13e+008
Elapsed time = 1210.66 sec. (889845.90 ticks, tree = 0.06 MB, solutions = 0)
 1125401   527    infeasible                           -0.0000 1.14e+008
 1129996   481        0.0000   330                     -0.0000 1.14e+008
 1133934   408        0.0000   305                     -0.0000 1.15e+008
 1138889   437    infeasible                           -0.0000 1.15e+008
 1143893   449        0.0000   220                     -0.0000 1.16e+008
 1149074   467        0.0000   364                     -0.0000 1.16e+008
 1153624   329        0.0000   352                     -0.0000 1.17e+008
 1158969   491    infeasible                           -0.0000 1.17e+008
 1163791   431    infeasible                           -0.0000 1.18e+008
 1167484   332        0.0000   318                     -0.0000 1.18e+008
Elapsed time = 1264.00 sec. (928040.04 ticks, tree = 0.26 MB, solutions = 0)
 1171268   317    infeasible                           -0.0000 1.19e+008
 1175984   329        0.0000   287                     -0.0000 1.19e+008
 1180925   323        0.0000   293                     -0.0000 1.20e+008
 1185958   242        0.0000   415                     -0.0000 1.20e+008
 1191580   223    infeasible                           -0.0000 1.21e+008
*1194993   186      integral     0        0.0000       -0.0000 1.21e+008    0.00%

Root node processing (before b&c):
  Real time             =    2.33 sec. (2407.88 ticks)
Parallel b&c, 12 threads:
  Real time             = 1294.31 sec. (947046.19 ticks)
  Sync time (average)   =  178.58 sec.
  Wait time (average)   =    0.08 sec.
                          ------------
Total (root+branch&cut) = 1296.64 sec. (949454.07 ticks)
   17                18
             4     3
          6  5     2  1
20                   19
      14  7 13 12
21        8  9
            10 11
22 16 15 23    24

This is the nineteenth part of the Types and Programming Languages series. For your convenience you can find other parts in the table of contents in Part 1 — Do not return in finally

Who is a senior software engineer? How do we become one? Does it matter at all? Let’s see some dimensions we can discuss when “assessing” someone’s skills.

Maturity

What does it mean to be mature? Many people think it’s important to point bad sides of solutions. No matter if we’re talking about the software engineering, social insurance, taxes, or whatever other thing that people like to discuss. However, that’s not the point. While it may seem that good engineers (professionals in general) can find drawbacks of solutions and identify where they fail, that’s not what we need. Let’s see some levels how people progress and what’s important.

First level – just complaining

This is easy and we do that so often. “Taxes are too high and they should be lower”. “This code is just broken and we should fix it”. Both of these statements may be 100% correct and yet they are completely non-actionable. It’s easy to “just complain” but it’s hard to explain why things are wrong and how to make them right.

When it comes to software engineering, we can give these statements literally about anything. We very often do that when criticizing some programming language, technology, library, framework, programming paradigm, particular solution, or anything else. This is just a trash talk that brings nothing.

Second level – being good at complaining

This is much harder. When someone achieves this level, they can easily point drawbacks of some particular solution and explain what they mean. What’s more, they are very often correct and make really good calls. They can for instance explain why a particular GC implementation won’t work here, why such and such library is not good enough, why some code is unreadable, or why some solution is slow. They can easily find edge cases where the solution will fail or explain why designs won’t work.

However, this is still not what we need. We need to understand that reality is never perfect. We can’t make our code (taxes, social insurance, health agency, whatever else) perfect. We can’t avoid all the problems. It’s not enough to just show where things won’t work and that they have drawbacks because everything have drawbacks. Interestingly enough, many software architects are on this level because they can always tell you “what not to do” but they can never give a good solution. Similarly, politicians are great at criticizing others but very rarely give solutions.

Another example is when software engineers can provide many options but can never decide which one to choose because all of them have some issues. Later, they typically push the decision on someone else (client, product owner, software architect) and then can complain that a wrong decision has been made.

Third level – giving solutions

Finally, people realize that the world is not perfect, and yet we need to deal with it somehow. They can give ideas (and even criticize them) and they can make decisions what to do. Even though they understand things will not be perfect, they can take the risk or even consciously pick something that they know will not work perfectly.

It’s important to understand that once one makes a choice, they will always be criticized. Always. That’s because one cannot pick a perfect solution because it doesn’t exist. Therefore, if you want to become mature enough and achieve this level, you need to accept that you will be always criticized. No matter if you’re a software engineer, software architect, or a politician. You’ll always get criticized, no matter what you do.

Seniority

Now, we can discuss what it means to be a “senior”. It’s important to understand that it’s not about skills per se. It’s about the proper attitude, skills, and experience.

There are three basic levels we can consider here.

Junior

Juniors (entry level people) cannot work independently. They aren’t experienced or skilled enough to deliver results on their own. No matter if we’re talking about software engineers, architects, politicians, or product owners. Juniors can’t work on their own and need some guidance to make progress.

Some claim that “X is not an entry-level position” where X can be whatever (scrum master, product owner, project manager, you pick one). I believe in general this is not true. No matter what our role is, we’ll need some guidance initially.

Mid

Mids (regulars) can work independently but they don’t have this something that distinguishes them from other regulars. They “just do the job”. They aren’t role models yet but they can work on their own. We can rely on them, we don’t need to supervise them, and we can expect they have good enough skills to do the job.

Senior

Seniors understand what their role is and how it interacts with other roles around. They can improve the role and not only themselves. They can grow others, can share knowledge, can teach, and they can adapt to changing conditions.

Notice that it doesn’t mean seniors have great skills. Pretty often they are not well skilled at all. However, they can use their skills efficiently and they understand how to grow up themselves and others around. They use their full potential and unblock the full potential of others around.

Senior Engineer vs Architect (vs others)

Based on previous sections, does it mean that seniors don’t need to be good at coding? Or that being an architect requires teaching others?

The answer is a little bit more complex. There are two basic things that we can recognize in software engineering: roles and skills.

Role

Software engineer is a role. Same is architect (and actually every flavor of architect like business architect, enterprise architect, solutions architect, etc.). Each role requires specific skillset and different roles may require similar skills.

Being that said, we should understand that “architect” is not “the next level after senior”. Software architect is a completely separate role. It requires different skills and generates different results. Therefore, one doesn’t need to become a senior engineer before becoming a software architect. Same with scrum masters, product owners, project managers, or people managers.

This also means that architects don’t need to be “experts” in programming. Just like there may be a junior software engineer, there may be a junior architect. It’s just another role.

Skills

Each role requires skills. Some skills may be needed for many roles, for instance dealing with numbers is required for accountants and salespeople. We can measure how good skills we have and we can typically say that we are novice, professionals, or experts. Obviously, we can recognize more levels or even assign numbers. That doesn’t change the point, it only changes the naming.

When it comes to software engineering, we can later recognize many skill dimensions.

Technology

Technology can be your favorite tech stack like C#, Spring, or LAMP. This can be a programming language, database, framework, library, paradigm, application, or whatever else.

For instance, an expert in C# will be able to explain how GC works, what is generational hypothesis, how locks are implemented, or why we can’t inherit from structures.

Area

Area is a particular part of the application. This can be backend, frontend, infrastructure, database, desktop, mobile, or whatever else.

For instance, an expert in web backend would be able to explain SNI, CORS, SOP, certificates, scaling, impersonation, caching, and other things typically used in web backends.

Domain

Domain is a particular part of the reality that we model in software. For instance, this could be payments, medical applications, high frequency trading, or logistics.

For instance, an expert in banking would explain what a credit score is, how to calculate it, what PCI is, how to deal with international transactions, what is ELIXIR, SEPA, or SORBNET.

Who am I

Based on what we said above, it’s possible that one is a senior software engineer + expert in backends + junior in C# + professional in banking. Therefore, we can see why there are software architects that seemingly don’t know how to code.

Programmer vs Software Engineer

Is there a difference between programming and software engineering? That’s a matter of naming and doesn’t matter much. If one doesn’t like to be called programmer, then let’s call them software engineers. This doesn’t matter at all.

What matters is the understanding that programming is not the only thing in “programming” (or “software engineering”). Much more important is “integrating software over time”. It’s easy to write some code. It’s hard to maintain the code over years when technologies around change, operating systems become deprecated, and network technologies disappear. Actually, writing the code is the easiest part of programming. Maintaining the code over years and keeping it alive for decades is what makes the software engineering (or programming) hard.

In short, it doesn’t matter whether we call ourselves programmers or software engineers. What matters is if we can write the code or can develop the same codebase for decades.

How do I know what to do next?

And now comes the tricky part. When someone says they look for “senior programmers”, how do I know what they mean?

The short answer is: you don’t. You won’t know until you ask them what they mean. And this is how you should look for a job: just clarify what the expectations are, what you can do, how good you are in it, and what you get in return. It doesn’t matter if they call you junior, senior, architect, principal, staff, fellow, or distinguished. That doesn’t matter at all (putting psychological aspects aside). What matters is what your role is and what you’re expected to do. That’s it.

This is the twentieth part of the Availability Anywhere series. For your convenience you can find other parts in the table of contents in Part 1 – Connecting to SSH tunnel automatically in Windows

We already know how to use full-tunnel VPN from a virtual machine on the host with TCP over File System. Today we’re going to see how to nest full-tunnel VPN inside another full-tunnel VPN.

Imagine that you take your corporate laptop and go to the office. You want to connect to your client’s network, so you use full-tunnel VPN (something like Cisco AnyConnect or Wireguard). Your client configured their firewall to allow your office’s IP address. All works.

Now, you want to work from home. You take your corporate laptop and come back home. You try connecting to your client’s network, but they didn’t allow your home’s IP address to connect. You try connecting to your office’s network with a VPN and this works well. However, you can’t connect to your client’s VPN now because you can’t have two full-tunnel VPNs enabled. How to deal with that?

I managed to get something like that to work with the following setup:

1. On the host, install Hyper-V
2. On the host, install Hyper-V guest called VM_A. I used Windows 10 x86. It’s better to use x86 VM to avoid some issues with nested virtualization.
3. On the host, enable virtualization extension for VM_A with Get-VM | where Name -eq "VM_A" | Set-VMProcessor -ExposeVirtualizationExtensions $true
4. On the host, connect to Hyper-V guest VM_A with shared drive C:
5. In Hyper-V guest VM_A, install Virtual Box 4.2.36 which works on Windows x86. Some other version of Virtual Box possibly can work.
6. In Hyper-V guest VM_A, create Virtual Box guest VM_B. I used Windows 7 x86. Again, use x86 VM version.
7. Configure VirtualBox guest VM_B networking as NAT with default interface type (something like Intel PRO/1000 MT Desktop)
8. In VirtualBox guest VM_B, install Virtual Box guest addins
9. In VirtualBox, configure shared directory \\tsclient\C with full read-write options (uncheck read only) and with automount
10. In Hyper-V guest VM_A, configure VPN to your office’s network. Let’s call this connection VPN_A.
11. In VirtualBox guest VM_B, configure VPN to your client’s network. Let’s call this connection VPN_B
12. You may need to set DNS in VirtualBox guest VM_B to something like 8.8.8.8
13. Enable VPN_A, then enable VPN_B.

All should work. Mind that in order to use VPN based on layer 3 GRE protocol (like PPTP) for VPN_A, you may need to reconfigure Hyper-V guest to use bridging. I don’t know if it’s possible to use GRE-based VPN for VPN_B in this setup (I doubt that). However, typical corporate VPN-s use HTTPS on the way to avoid issues.

I tested this setup with Wireguard as VPN_A and Windows’ SSTP as VPN_B. It worked correctly. When VPN_A was enabled and VPN_B was disabled, then VirtualBox guest VM_B was visible to the internet from the IP address of VPN_A (so the IP address of the office). When both VPN_A and VPN_B were enabled, VirtualBox guest VM_B was visible to the internet from the IP address of VPN_B (client’s IP address). Also, shared drive from host was visible in VirtualBox guest VM_B when both VPN_A and VPN_B were enabled. Therefore, you can use TCP over File System properly to route the traffic from the host through any of the VPNs.

This is the one hundred and fifth part of the ILP series. For your convenience you can find other parts in the table of contents in Part 1 – Boolean algebra

Today we are going to solve the Sudoku Cube. It’s a variation of the regular Rubik’s cube in which we have digits on the cube and each side must have exactly nine different digits from one to nine. What’s more, digits on a side must all look the same direction.

I took photos of my cube. You can see them below:

The tricky part is what to do. With the regular cube it’s rather clear where each piece should go. The hard part is figuring out how to put it into place. With Sudoku Cube it’s much harder. We don’t actually see where to put each element. The first step is to “solve the grid”. We need to understand where to put elements.

Solving the grid

First, notice that the number 1 is symmetrical. We don’t know whether it’s facing “up” or “down”. Therefore, we need to assume it can look both directions. We could actually wonder similarly for number eight (which side is “up”) or six/nine, but for them we can make some assumptions. Eight should be narrower at the top. Nine has a label on it.

Second, we don’t know which directions the sides look into. Also, it may not be obvious from the very beginning, but each center has an orientation. This is different from the regular cube. There are algorithms to do so and we’ll see them later. However, for now we need to assume that any side can look any direction. Sometimes the cube is convenient and the “middle strap” sides look upwards, but we can’t assume that.

Therefore, we need to figure out where pieces go. Once we have that, we can then solve the grid.

We start by defining the permutations in this way:

This looks cryptic, so let’s analyze step by step.

Let’s start with the corners marked with red arrows and numbers. We can see six faces of the cube. Going from left to right, top to bottom, the faces are: up, left, front, right, back, down. We have eight corners of the cube. Therefore, there are eight pieces that we can rotate and put in given places. Places are numbered from oen to eight, and permutations are numbered from zero to two. We are going to encode each piece as a list of numbers and list of rotations.

Let’s take the Picture from the above in which you can see free sides of the cube. Let’s say that the side with numbers 3, 9, 4, 6, 1, 5, 5, 7, 9 is the front side, and the side with numbers 5, 4, 6, 3, 6, 5, 8, 2, 2 is the top one. You can see that we have a corner with number 4 to the right of 9 and above 5. This is the corner that we marked as 1_0 on the diagram screen. So we can see, that we can encode this corner as having one with the following sequence of numbers: 4, 8, 4. Therefore 1_0 = 4, 1_1 = 8, 1_2 = 4.

You can see the arrow going up. This is an arbitrary indication which face I consider “upwards” of this given field. Similarly, for other fields. We want to encode the rotation of a piece based on the orientation of the digit. We have four directions: aligned with the arrow encoded as zero, rotated clockwise once by ninety degrees encoded as one, rotated twice encoded as two, rotated three times encoded as three. Therefore, the rotations of the numbers 4, 8, 4 are 3, 2, 1.

We can now take each corner and encode it properly. This should be the encoding:

var corners = new []{
	new Corner(solver, "c1") { Values = new[]{4, 8, 4}, Rotations = new[] {3, 2, 1}},
	new Corner(solver, "c2") { Values = new[]{9, 5, 1}, Rotations = new[] {3, 2, 1}},
	new Corner(solver, "c3") { Values = new[]{5, 9, 1}, Rotations = new[] {2, 2, 1}},
	new Corner(solver, "c4") { Values = new[]{3, 7, 5}, Rotations = new[] {1, 0, 3}},
	new Corner(solver, "c5") { Values = new[]{2, 6, 7}, Rotations = new[] {0, 3, 0}},
	new Corner(solver, "c6") { Values = new[]{6, 3, 7}, Rotations = new[] {2, 1, 2}},
	new Corner(solver, "c7") { Values = new[]{4, 1, 6}, Rotations = new[] {3, 0, 0}},
	new Corner(solver, "c8") { Values = new[]{8, 9, 2}, Rotations = new[] {3, 1, 0}}
};

We can do the same for edges (middles on the sides). We have twelve edges, each edge has two pieces. They are marked with green numbers and arrows. This is how we encode the cube:

var edges = new []{
	new Edge(solver, "e1") { Values = new[]{9, 3}, Rotations = new[] {0, 3}},
	new Edge(solver, "e2") { Values = new[]{5, 2}, Rotations = new[] {0, 2}},
	new Edge(solver, "e3") { Values = new[]{7, 6}, Rotations = new[] {1, 2}},
	new Edge(solver, "e4") { Values = new[]{9, 8}, Rotations = new[] {2, 0}},
	new Edge(solver, "e5") { Values = new[]{3, 2}, Rotations = new[] {0, 2}},
	new Edge(solver, "e6") { Values = new[]{6, 9}, Rotations = new[] {1, 3}},
	new Edge(solver, "e7") { Values = new[]{2, 3}, Rotations = new[] {1, 3}},
	new Edge(solver, "e8") { Values = new[]{8, 5}, Rotations = new[] {3, 3}},
	new Edge(solver, "e9") { Values = new[]{8, 8}, Rotations = new[] {1, 2}},
	new Edge(solver, "e10") { Values = new[]{4, 2}, Rotations = new[] {1, 1}},
	new Edge(solver, "e11") { Values = new[]{3, 4}, Rotations = new[] {2, 0}},
	new Edge(solver, "e12") { Values = new[]{1, 7}, Rotations = new[] {3, 0}}
};

We also have centers. We don’t care about their orientation at this point.

Formulas

We basically want to do the following:

• For each corner: assign exactly one position to a corner (position from one to eight) and one permutation (from zero to two)
• Do the same for edges (twelve positions and two permutations)
• Make sure that each face has all pieces but center oriented the same way
• Make sure that number one can be oriented upside down (as it looks the same)
• Make sure each face has digits from one to nine

Sounds easy. Let’s see the first implementation.

First implementation

Let’s start by encoding the grid. First, we’d like to encode the positions from the chart above. For corners, we take the value like 4_1 and serialize it to one number as 4 * 3 + 1 = 13. We do similarly for edges:

// 0 means empty
// Values are 1_0, 1_1, 1_2, 2_0, 2_1, ...
// Corners have 3 elements, so: 1_0 = 3 * 1 + 0 = 3
// Edges have 2 elements, so: 1_0 = 2 * 1 + 0 = 2
var diagram = new []{
	new[] {0, 0, 0, 16, 17, 26, 0, 0, 0, 0, 0, 0},
	new[] {0, 0, 0, 23, 0, 11, 0, 0, 0, 0, 0, 0},
	new[] {0, 0, 0, 14, 3, 4, 0, 0, 0, 0, 0, 0},
	new[] {17, 22, 13, 12, 2, 3, 5, 10, 25, 24, 16, 15},
	new[] {21, 0, 9, 8, 0, 4, 5, 0, 14, 15, 0, 20},
	new[] {19, 24, 11, 9, 6, 6, 7, 12, 23, 21, 18, 18},
	new[] {0, 0, 0, 10, 7, 8, 0, 0, 0, 0, 0, 0},
	new[] {0, 0, 0, 25, 0, 13, 0, 0, 0, 0, 0, 0},
	new[] {0, 0, 0, 20, 19, 22, 0, 0, 0, 0, 0, 0},
};

Now, we encode the orientation of each field (arrows). We assume -1 means empty field:

var fieldsOrientations = new []{
	new[] {-1, -1, -1, 3, 0, 0, -1, -1, -1, -1, -1, -1},
	new[] {-1, -1, -1, 3, 0, 1, -1, -1, -1, -1, -1, -1},
	new[] {-1, -1, -1, 2, 2, 1, -1, -1, -1, -1, -1, -1},
	new[] {3, 0, 0, 3, 0, 0, 3, 0, 0, 3, 0, 0},
	new[] {3, 0, 1, 3, 0, 1, 3, 0, 1, 3, 0, 1},
	new[] {2, 2, 1, 2, 2, 1, 2, 2, 1, 2, 2, 1},
	new[] {-1, -1, -1, 3, 0, 0, -1, -1, -1, -1, -1, -1},
	new[] {-1, -1, -1, 3, 0, 1, -1, -1, -1, -1, -1, -1},
	new[] {-1, -1, -1, 2, 2, 1, -1, -1, -1, -1, -1, -1}
};

Now, let’s make sure that each piece is put in a different position:

// Make corners in distinct positions
solver.Set<AllDifferent>(corners[0].FinalPosition, corners.Skip(1).Select(c => c.FinalPosition).ToArray());

// Make edges in distinct positions
solver.Set<AllDifferent>(edges[0].FinalPosition, edges.Skip(1).Select(e => e.FinalPosition).ToArray());

Let’s now start the magic. The idea is as follows: we ask the solver to assign positions and rotations to the pieces. We then iterate over all possibilities, check if a given possibility was selected by the solver, and then calculate the outcome. We then add the requirements to make the grid solved. Let’s begin with the corners.

Func<int, int, Tuple<IVariable, IVariable>> setupSingleCorner = (x, y) => {
	int number = diagram[x][y];
	int position = number / 3 - 1;
	int permutation = number % 3;
	
	IVariable piecePermutation = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(2));
	IVariable finalPermutation = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(2));
	IVariable pieceRotationValue = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(3));
	IVariable finalRotation = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(3));
	IVariable cornerValue = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(9)).Set<GreaterOrEqual>(solver.FromConstant(1));
	
	foreach(var corner in corners){
		var matchingCorner = solver.Operation<IsEqual>(corner.FinalPosition, solver.FromConstant(position));
		
		solver.Operation<MaterialImplication>(
			matchingCorner,
			solver.Operation<IsEqual>(corner.FinalPermutation, piecePermutation)
		).Set<Equal>(solver.FromConstant(1));
		
		for(int possiblePermutation=0;possiblePermutation<3;++possiblePermutation){
			var matchingPermutation = matchingCorner.Operation<Conjunction>(finalPermutation.Operation<IsEqual>(solver.FromConstant(possiblePermutation)));
		
			solver.Operation<MaterialImplication>(
				matchingPermutation,
				solver.Operation<IsEqual>(pieceRotationValue, solver.FromConstant(corner.Rotations[possiblePermutation]))
			).Set<Equal>(solver.FromConstant(1));
			
			solver.Operation<MaterialImplication>(
				matchingPermutation,
				solver.Operation<IsEqual>(cornerValue, solver.FromConstant(corner.Values[possiblePermutation]))
			).Set<Equal>(solver.FromConstant(1));
		}
	}
	
	solver.Set<Equal>(
		finalPermutation, 
		solver.Operation<Remainder>(
			solver.Operation<Addition>(solver.FromConstant(permutation), piecePermutation),
			solver.FromConstant(3)
		)
	);
	
	solver.Set<Equal>(
		finalRotation, 
		solver.Operation<Remainder>(
			solver.Operation<Addition>(solver.FromConstant(fieldsOrientations[x][y]), pieceRotationValue),
			solver.FromConstant(4)
		)
	);
	
	return Tuple.Create(cornerValue, finalRotation);
};

For each corner from the diagram, we deserialize its position and permutation (lines 2-4). Next, we need to prepare some variables (lines 6-10) and then decipher the solution.

We iterate over each possible piece (line 12) and see if the corner was assigned to the field we analyze now (line 13). If that’s the case, then we copy the value of the assigned permutation to the temporary variable (lines 15-18).

Next, we do some magic. We would like to check all possible permutations to see which one was selected. To do that, we need to calculate what we call here finalPermutation. However, this is some kind of a cyclic dependency. First, we copy the permutation assigned by the solver and called corner.FinalPermutation to the variable piecePermutation (lines 15-18). Next, we need to add the permutation of the field to that value, calculate the modulo three, and assign that to the variable finalPermutation (lines 35-41). However, we then (or technically earlier) use the variable finalPermutation in line 21 to answer whether the current permutation we analyze is the one that was selected. Once we have that, we can copy the rotation of the corner (lines 23-26) and the value of the corner (lines 28-32).

Next, we do another time travel and we calculate the final orientation of the field by adding the orientation of the corner and the orientation (direction of the arrow) of the field. That’s in lines 43-49.

Finally, we return both the value and the final orientation (line 51).

Okay, we can now iterate over all corners of a given face:

Func<int, int, Tuple<IVariable, IVariable>[]> setupCorners = (x, y) => {
	var valuesAndRotations = new []{
		setupSingleCorner(x, y),
		setupSingleCorner(x, y+2),
		setupSingleCorner(x+2, y+2),
		setupSingleCorner(x+2, y)
	};
	
	return valuesAndRotations;
};

We need to do a very similar code with the edges:

Func<int, int, Tuple<IVariable, IVariable>> setupSingleEdge = (x, y) => {
	int number = diagram[x][y];
	int position = number / 2 - 1;
	int permutation = number % 2;
	
	IVariable piecePermutation = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(1));
	IVariable finalPermutation = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(1));
	IVariable pieceRotationValue = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(3));
	IVariable finalRotation = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(3));
	IVariable edgeValue = solver.CreateAnonymous(Domain.PositiveOrZeroInteger).Set<LessOrEqual>(solver.FromConstant(9)).Set<GreaterOrEqual>(solver.FromConstant(1));
	
	calculatedRotations[x][y] = finalRotation;
	
	foreach(var edge in edges){
		var matchingEdge = solver.Operation<IsEqual>(edge.FinalPosition, solver.FromConstant(position));
		
		solver.Operation<MaterialImplication>(
			matchingEdge,
			solver.Operation<IsEqual>(edge.FinalPermutation, piecePermutation)
		).Set<Equal>(solver.FromConstant(1));
		
		for(int possiblePermutation=0;possiblePermutation<2;++possiblePermutation){
			var matchingPermutation = matchingEdge.Operation<Conjunction>(finalPermutation.Operation<IsEqual>(solver.FromConstant(possiblePermutation)));
		
			solver.Operation<MaterialImplication>(
				matchingPermutation,
				solver.Operation<IsEqual>(pieceRotationValue, solver.FromConstant(edge.Rotations[possiblePermutation]))
			).Set<Equal>(solver.FromConstant(1));
			
			solver.Operation<MaterialImplication>(
				matchingPermutation,
				solver.Operation<IsEqual>(edgeValue, solver.FromConstant(edge.Values[possiblePermutation]))
			).Set<Equal>(solver.FromConstant(1));
		}
	}
	
	solver.Set<Equal>(
		finalPermutation, 
		solver.Operation<Remainder>(
			solver.Operation<Addition>(solver.FromConstant(permutation), piecePermutation),
			solver.FromConstant(2)
		)
	);
	
	solver.Set<Equal>(
		finalRotation, 
		solver.Operation<Remainder>(
			solver.Operation<Addition>(solver.FromConstant(fieldsOrientations[x][y]), pieceRotationValue),
			solver.FromConstant(4)
		)
	);
	
	return Tuple.Create(edgeValue, finalRotation);
};

We iterate over all edges of a face:

Func<int, int, Tuple<IVariable, IVariable>[]> setupEdges = (x, y) => {
	var valuesAndRotations = new []{
		setupSingleEdge(x, y+1),
		setupSingleEdge(x+1, y),
		setupSingleEdge(x+1, y+2),
		setupSingleEdge(x+2, y+1)
	};
	
	return valuesAndRotations;
};

And we also get the value of the center:

Func<int, int, IVariable> setupCenter = (x, y) => {
	return solver.FromConstant(int.Parse("" + centers[x][y]));
};

We can now setup a single face:

Action<int, int> setupSingleFace = (x, y) => {
	var valuesAndRotations = setupCorners(x, y).Concat(setupEdges(x, y)).ToArray();
	
	var valuesAndRotationsAndOnes = valuesAndRotations.Select(t => {
		var anotherPossibleRotation = solver.Operation<Condition>(
			t.Item1.Operation<IsEqual>(solver.FromConstant(1)),
			t.Item2.Operation<Addition>(solver.FromConstant(2)).Operation<Remainder>(solver.FromConstant(4)),
			t.Item2
		);
		
		return Tuple.Create(t.Item1, t.Item2, anotherPossibleRotation);
	}).ToArray();
	
	// Make pairwise rotations equal = make pieces (but center) look the same direction
	for(int id=1; id < valuesAndRotationsAndOnes.Length; ++id){
		solver.Set<Equal>(
			solver.Operation<Disjunction>(
				solver.Operation<IsEqual>(valuesAndRotationsAndOnes[id].Item2, valuesAndRotationsAndOnes[id-1].Item2),
				solver.Operation<IsEqual>(valuesAndRotationsAndOnes[id].Item2, valuesAndRotationsAndOnes[id-1].Item3),
				solver.Operation<IsEqual>(valuesAndRotationsAndOnes[id].Item3, valuesAndRotationsAndOnes[id-1].Item2),
				solver.Operation<IsEqual>(valuesAndRotationsAndOnes[id].Item3, valuesAndRotationsAndOnes[id-1].Item3)
			),
			solver.FromConstant(1)
		);
	}
	
	var center = setupCenter(x + 1, y+1);
	
	// Make sudoku numbers
	solver.Set<AllDifferent>(center, valuesAndRotationsAndOnes.Select(t => t.Item1).ToArray());
};

We take all the values and rotations of corners and edges (line 2). We then need to take all the ones and calculate additional rotation. We check if the value is one (line 6) and if that’s the case, then we add another rotation (upside-down), otherwise we return the same rotation (lines 7-8).

Finally, we take all the sides and make sure that they all have the same rotations. So for each pair of pieces, either their rotations are equal, or their rotation and alternative rotation are equal, or their alternative rotations are equal (lines 15-25).

Finally, we add the center (line 27) and make sure that all numbers are different (line 30) which means that we have the sudoku requirement met.

We can now configure all faces:

Action setupFaces = () => {
	setupSingleFace(0, 3);
	setupSingleFace(3, 0);
	setupSingleFace(3, 3);
	setupSingleFace(3, 6);
	setupSingleFace(3, 9);
	setupSingleFace(6, 3);
};

setupFaces();

Let’s now add the goal, solve the problem, and print the result:

solver.AddGoal("goal", solver.FromConstant(0));

solver.Solve();

var template = new []{
	"     ---         ",
	"    |   |        ",
	"    |   |        ",
	"    |   |        ",
	" --- --- --- ---",
	"|   |   |   |   |",
	"|   |   |   |   |",
	"|   |   |   |   |",
	" --- --- --- --- ",
	"    |   |        ",
	"    |   |        ",
	"    |   |        ",
	"     ---         "
};

var numbersGrid = template.Select(x => x.ToArray()).ToArray();
var rotationsGrid = template.Select(x => x.ToArray()).ToArray();

Action<int, int, int, int> printSingleCorner = (x, y, destinationX, destinationY) => {
	int number = diagram[x][y];
	int position = number / 3 - 1;
	int permutation = number % 3;
	
	var matchingCorner = corners.First(c => (int)Math.Round(solver.GetValue(c.FinalPosition)) == position);
	var piecePermutation = (int)Math.Round(solver.GetValue(matchingCorner.FinalPermutation));
	
	var finalPermutation = (permutation + piecePermutation) % 3;
	numbersGrid[destinationX][destinationY] = matchingCorner.Values[finalPermutation].ToString()[0];
	
	rotationsGrid[destinationX][destinationY] = matchingCorner.Rotations[finalPermutation].ToString()[0];
};

Action<int, int, int, int> printCorners = (x, y, destinationX, destinationY) => {
	printSingleCorner(x, y, destinationX, destinationY);
	printSingleCorner(x, y+2, destinationX, destinationY + 2);
	printSingleCorner(x+2, y+2, destinationX + 2, destinationY + 2);
	printSingleCorner(x+2, y, destinationX + 2, destinationY);
};

Action<int, int, int, int> printSingleEdge = (x, y, destinationX, destinationY) => {
	int number = diagram[x][y];
	int position = number / 2 - 1;
	int permutation = number % 2;
	
	var matchingEdge = edges.First(e => (int)Math.Round(solver.GetValue(e.FinalPosition)) == position);
	var piecePermutation = (int)Math.Round(solver.GetValue(matchingEdge.FinalPermutation));
	
	var finalPermutation = (permutation + piecePermutation) % 2;
	numbersGrid[destinationX][destinationY] = matchingEdge.Values[finalPermutation].ToString()[0];
	
	rotationsGrid[destinationX][destinationY] = matchingEdge.Rotations[finalPermutation].ToString()[0];
};

Action<int, int, int, int> printEdges = (x, y, destinationX, destinationY) => {
	printSingleEdge(x, y+1, destinationX, destinationY + 1);
	printSingleEdge(x+1, y, destinationX + 1, destinationY);
	printSingleEdge(x+1, y+2, destinationX + 1, destinationY + 2);
	printSingleEdge(x+2, y+1, destinationX + 2, destinationY + 1);
};

Action<int, int, int, int> printCenters = (x, y, destinationX, destinationY) => {
	numbersGrid[destinationX+1][destinationY+1] = centers[x+1][y+1];
};

Action<int, int, int, int> printSingleFace = (x, y, destinationX, destinationY) => {
	printCorners(x, y, destinationX, destinationY);
	printEdges(x, y, destinationX, destinationY);
	printCenters(x, y, destinationX, destinationY);
};

Action printFaces = () => {
	printSingleFace(0, 3, 1, 5);
	printSingleFace(3, 0, 5, 1);
	printSingleFace(3, 3, 5, 5);
	printSingleFace(3, 6, 5, 9);
	printSingleFace(3, 9, 5, 13);
	printSingleFace(6, 3, 9, 5);
};

printFaces();

for(int row = 0; row < template.Length; ++ row){
	Console.Write(new String(numbersGrid[row]));
	Console.Write("          ");
	Console.WriteLine(new String(rotationsGrid[row]));
}

This works. In theory. I tried running that with NEOS for eight hours and it didn’t solve the problem, unfortunately. It was simply too complex.

Let’s see another solution.

Second implementation

In this solution we’ll apply many optimizations. We’ll store the positions as bitmasks instead of integers to use boolean flags (which are much faster). We won’t calculate the obtained direction of the face, but we’ll enforce which face must be selected. Finally, we won’t check the options and see if they were selected, but rather we will calculate what was selected end enforce the options. Let’s start.

First, we create a bitmask for directions of each face. We have six faces (sides) and four directions for each:

// face0_up, face0_right, face0_down, face0_left, face1_up ...
// front = 0, right = 1, back = 2, left = 3, up = 4, down = 5
var facesDirections = Enumerable.Range(0, 6 * 4).Select(d => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray();

Next, we encode a bitmask what value was assigned to each corner side. We have six faces, four corners for each face, and nine numbers to choose from:

// face0_corner_top_right_value1, face0_corner_top_right_value2, ..., face0_corner_top_right_value9, face0_corner_bottom_right_value1,
// ..., face0_corner_bottom_right_value9, face0_corner_bottom_left_value1, ..., face0_corner_top_left_value_9, face1_corner_top_right_value1...
var cornersNumbers = Enumerable.Range(0, 6*4*9).Select(n => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray();

We do the similar for edges:

// face0_top_value1, face_0_top_value2, ..., face0_top_value9, face0_right_value1
// ..., face0_right_value9, face0_bottom_value1, ..., face0_bottom_value9, face0_left_value1, ...
// face0_left_value9, face1_top_value1...
var edgeNumbers = Enumerable.Range(0, 6*4*9).Select(n => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray();

Now, we can use these bitmasks to constrain the solution. We make sure that digits on a face look all the same direction. So, for each face we take the direction flags and make sure that only one flag is selected:

// Each face has exactly one direction
for(var faceId = 0; faceId < 6; ++faceId){
	solver.Operation<Addition>(facesDirections.Skip(faceId * 4).Take(4).ToArray()).Set<Equal>(solver.FromConstant(1));
}

We then make sure each corner has exactly one number. We have six faces and four corners on each face:

// Each corner has exactly one number
for(var cornerId = 0; cornerId < 6 * 4; ++cornerId){
	solver.Operation<Addition>(cornersNumbers.Skip(cornerId * 9).Take(9).ToArray()).Set<Equal>(solver.FromConstant(1));
}

We now need to see how corners are stored. Previously, corner.FinalPosition was an integer. Now it’s a long bitmasks of positions and permutations. We have eight possible positions and three permutations:

public class Corner$id {
	public int[] Values {get;set;}
	public int[] Rotations {get;set;}
	public IVariable[] FinalPosition {get; set;}
	public string Prefix {get;set;}
	
	public Corner(IMilpManager solver, string prefix){
		// position1_permutation0, position1_permutation1, position1_permutation2, position2_permutation0, ...
		FinalPosition = Enumerable.Range(0, 8*3).Select(d => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray();
		Prefix = prefix;
	}
}

Next, we make sure that each corner piece has exactly one position and one rotation selected:

// Each corner is in one place
foreach(var corner in corners){
	solver.Operation<Addition>(corner.FinalPosition).Set<Equal>(solver.FromConstant(1));
}

Next we need to make sure that each corner of the cube has exactly one piece assigned. We have eight corners, for each corner we take bit flags of each piece, and make sure that only one was selected:

// Exactly one piece in given corner
for(var cornerId = 0; cornerId < 8; ++cornerId){
	solver.Operation<Addition>(
		corners.SelectMany(corner => corner.FinalPosition.Skip(cornerId * 3).Take(3)).ToArray()
	).Set<Equal>(solver.FromConstant(1));
}

We do the same for edges:

// Each edge has exactly one number
for(var edgeId = 0; edgeId < 6 * 4; ++edgeId){
	solver.Operation<Addition>(edgeNumbers.Skip(edgeId * 9).Take(9).ToArray()).Set<Equal>(solver.FromConstant(1));
}

// Each edge is in one place
foreach(var edge in edges){
	solver.Operation<Addition>(edge.FinalPosition).Set<Equal>(solver.FromConstant(1));
}

// Exactly one piece in given edge
for(var edgeId = 0; edgeId < 12; ++edgeId){
	solver.Operation<Addition>(
		edges.SelectMany(edge => edge.FinalPosition.Skip(edgeId * 2).Take(2)).ToArray()
	).Set<Equal>(solver.FromConstant(1));
}

Now we need to make sure that each side has sudoku numbers:

var faceToCenters = new Dictionary<int, Tuple<int, int>>{
	{0, Tuple.Create(4, 4)},
	{1, Tuple.Create(4, 7)},
	{2, Tuple.Create(4, 10)},
	{3, Tuple.Create(4, 1)},
	{4, Tuple.Create(1, 4)},
	{5, Tuple.Create(7, 4)}
};

// Sudoku numbers on each face
for(var faceId = 0; faceId < 6; ++faceId){
	var centerPosition = faceToCenters[faceId];
	var centerNumber = int.Parse("" + centers[centerPosition.Item1][centerPosition.Item2]);

	var cornerDigits = Enumerable.Range(0, 4).Select(p => cornersNumbers.Skip(faceId * 4 * 9).Skip(p * 9).Take(9).ToArray()).ToArray();
	var edgeDigits = Enumerable.Range(0, 4).Select(p => edgeNumbers.Skip(faceId * 4 * 9).Skip(p * 9).Take(9).ToArray()).ToArray();
	var centerDigit = new [] { Enumerable.Range(0, 9).Select(i => i == centerNumber - 1 ? solver.FromConstant(1) : solver.FromConstant(0)).ToArray() };
	var vectors = cornerDigits.Concat(edgeDigits).Concat(centerDigit).ToArray();
		
	for(var digit = 0; digit < 9; ++ digit){
		solver.Operation<Addition>(vectors.Select(v => v[digit]).ToArray()).Set<Equal>(solver.FromConstant(1));
	}
}

We need two additional mappings from corners and edges to faces:

var cornersToFaces = new Dictionary<Tuple<int, int>, int> {
	{Tuple.Create(0, 3), 4},
	{Tuple.Create(0, 5), 4},
	{Tuple.Create(2, 3), 4},
	{Tuple.Create(2, 5), 4},
	{Tuple.Create(3, 0), 3},
	{Tuple.Create(3, 2), 3},
	{Tuple.Create(5, 0), 3},
	{Tuple.Create(5, 2), 3},
	{Tuple.Create(3, 3), 0},
	{Tuple.Create(3, 5), 0},
	{Tuple.Create(5, 3), 0},
	{Tuple.Create(5, 5), 0},
	{Tuple.Create(3, 6), 1},
	{Tuple.Create(3, 8), 1},
	{Tuple.Create(5, 6), 1},
	{Tuple.Create(5, 8), 1},
	{Tuple.Create(3, 9), 2},
	{Tuple.Create(3, 11), 2},
	{Tuple.Create(5, 9), 2},
	{Tuple.Create(5, 11), 2},
	{Tuple.Create(6, 3), 5},
	{Tuple.Create(6, 5), 5},
	{Tuple.Create(8, 3), 5},
	{Tuple.Create(8, 5), 5},
};

var edgesToFaces = new Dictionary<Tuple<int, int>, int> {
	{Tuple.Create(0, 4), 4},
	{Tuple.Create(1, 3), 4},
	{Tuple.Create(1, 5), 4},
	{Tuple.Create(2, 4), 4},
	{Tuple.Create(3, 1), 3},
	{Tuple.Create(4, 0), 3},
	{Tuple.Create(4, 2), 3},
	{Tuple.Create(5, 1), 3},
	{Tuple.Create(3, 4), 0},
	{Tuple.Create(4, 3), 0},
	{Tuple.Create(4, 5), 0},
	{Tuple.Create(5, 4), 0},
	{Tuple.Create(3, 7), 1},
	{Tuple.Create(4, 6), 1},
	{Tuple.Create(4, 8), 1},
	{Tuple.Create(5, 7), 1},
	{Tuple.Create(3, 10), 2},
	{Tuple.Create(4, 9), 2},
	{Tuple.Create(4, 11), 2},
	{Tuple.Create(5, 10), 2},
	{Tuple.Create(6, 4), 5},
	{Tuple.Create(7, 3), 5},
	{Tuple.Create(7, 5), 5},
	{Tuple.Create(8, 4), 5},
};

We also need to know where each corner is (whether it’s right top, right bottom, left bottom, left top). Similarly for edges (top, right, bottom, left):

var cornersToDiagonalEnds = new Dictionary<Tuple<int, int>, int> {
	{Tuple.Create(0, 3), 3},
	{Tuple.Create(0, 5), 0},
	{Tuple.Create(2, 3), 2},
	{Tuple.Create(2, 5), 1},
	{Tuple.Create(3, 0), 3},
	{Tuple.Create(3, 2), 0},
	{Tuple.Create(5, 0), 2},
	{Tuple.Create(5, 2), 1},
	{Tuple.Create(3, 3), 3},
	{Tuple.Create(3, 5), 0},
	{Tuple.Create(5, 3), 2},
	{Tuple.Create(5, 5), 1},
	{Tuple.Create(3, 6), 3},
	{Tuple.Create(3, 8), 0},
	{Tuple.Create(5, 6), 2},
	{Tuple.Create(5, 8), 1},
	{Tuple.Create(3, 9), 3},
	{Tuple.Create(3, 11), 0},
	{Tuple.Create(5, 9), 2},
	{Tuple.Create(5, 11), 1},
	{Tuple.Create(6, 3), 3},
	{Tuple.Create(6, 5), 0},
	{Tuple.Create(8, 3), 2},
	{Tuple.Create(8, 5), 1},
};

var edgesToAxisEnds = new Dictionary<Tuple<int, int>, int> {
	{Tuple.Create(0, 4), 0},
	{Tuple.Create(1, 3), 3},
	{Tuple.Create(1, 5), 1},
	{Tuple.Create(2, 4), 2},
	{Tuple.Create(3, 1), 0},
	{Tuple.Create(4, 0), 3},
	{Tuple.Create(4, 2), 1},
	{Tuple.Create(5, 1), 2},
	{Tuple.Create(3, 4), 0},
	{Tuple.Create(4, 3), 3},
	{Tuple.Create(4, 5), 1},
	{Tuple.Create(5, 4), 2},
	{Tuple.Create(3, 7), 0},
	{Tuple.Create(4, 6), 3},
	{Tuple.Create(4, 8), 1},
	{Tuple.Create(5, 7), 2},
	{Tuple.Create(3, 10), 0},
	{Tuple.Create(4, 9), 3},
	{Tuple.Create(4, 11), 1},
	{Tuple.Create(5, 10), 2},
	{Tuple.Create(6, 4), 0},
	{Tuple.Create(7, 3), 3},
	{Tuple.Create(7, 5), 1},
	{Tuple.Create(8, 4), 2},
};

With all that prepared we can finally assert the corners:

Action<int, int> setupSingleCorner = (x, y) => {
	int number = diagram[x][y];
	int position = number / 3 - 1;
	int permutation = number % 3;
	var face = cornersToFaces[Tuple.Create(x, y)];
	var diagonalEnd = cornersToDiagonalEnds[Tuple.Create(x, y)];
	
	foreach(var corner in corners){
		for(var piecePermutation = 0; piecePermutation < 3; ++piecePermutation){
			var wasPicked = corner.FinalPosition.Skip(position * 3).Skip(piecePermutation).First();
			var finalPermutation = (permutation + piecePermutation) % 3;
			var finalRotation = (corner.Rotations[finalPermutation] + fieldsOrientations[x][y]) % 4;
			var value = corner.Values[finalPermutation];
			
			if(value == 1){
				solver.Operation<MaterialImplication>(
					wasPicked,
					solver.Operation<Disjunction>(
						facesDirections.Skip(face * 4).Take(4).ToArray()[finalRotation],
						facesDirections.Skip(face * 4).Take(4).ToArray()[(finalRotation + 2)%4]
					)
				).Set<Equal>(solver.FromConstant(1));
			}else{
				solver.Operation<MaterialImplication>(
					wasPicked,
					facesDirections.Skip(face * 4).Take(4).ToArray()[finalRotation]
				).Set<Equal>(solver.FromConstant(1));
			}
			
			solver.Operation<MaterialImplication>(
				wasPicked,
				cornersNumbers.Skip(face * 4 * 9).Skip(diagonalEnd * 9).Take(9).ToArray()[value - 1]
			).Set<Equal>(solver.FromConstant(1));
		}
	}
};

We take some metadata about the piece we are in (lines 2-6). Next, we iterate over all corners and permutations. However, this time instead of asking “is this corner in that permutation assigned to this field”, we simply take what was assigned and enforce the proper bitflags.

We first take the bit indicating whether a given piece was assigned to this corner and this permutation (line 10). Next, we calculate the final permutation in this field (line 11) and the final rotation including directions of the arrows (line 12). We also take the value of the piece (line 13). Notice that this time we don’t extract these values from the ILP variables. We precalculate them outside of the model which is much faster.

We can now do two simple constraints. First, if this digit is one (line 15) then we enforce this constraint: if this piece was picked (line 17), then direction of the face needs to be either the same as the direction of the piece (line 19) or the opposite (line 20). If the digit is not one, then we enforce the constraint, that if the piece was picked, than the boolean flag indicating the direction of the face must be selected (line 26).

The crucial difference is that we don’t calculate the direction within the model now. We do the causation outside of the model. We encode something like “I don’t know what piece was selected, but if the piece I’m currently looking at was selected, then this bit flag of the face direction must be selected too”.

The next constraint we add is for the numbers: if the piece was picked (line 31) then the number assigned to the corner is selected (line 32). Again, we don’t care about the actual value if it was selected or not. We just make sure that if it was selected, then some other bit flag is set.

We can now setup all corners:

Action<int, int> setupCorners = (x, y) => {
	setupSingleCorner(x, y);
	setupSingleCorner(x, y+2);
	setupSingleCorner(x+2, y+2);
	setupSingleCorner(x+2, y);
};

We do very similar stuff for edges:

Action<int, int> setupSingleEdge = (x, y) => {
	int number = diagram[x][y];
	int position = number / 2 - 1;
	int permutation = number % 2;
	var face = edgesToFaces[Tuple.Create(x, y)];
	var axisEnd = edgesToAxisEnds[Tuple.Create(x, y)];
	
	foreach(var edge in edges){
		for(var piecePermutation = 0; piecePermutation < 2; ++piecePermutation){
			var wasPicked = edge.FinalPosition.Skip(position * 2).Skip(piecePermutation).First();
			var finalPermutation = (permutation + piecePermutation) % 2;
			var finalRotation = (edge.Rotations[finalPermutation] + fieldsOrientations[x][y]) % 4;
			var value = edge.Values[finalPermutation];
			
			if(value == 1){
				solver.Operation<MaterialImplication>(
					wasPicked,
					solver.Operation<Disjunction>(
						facesDirections.Skip(face * 4).Take(4).ToArray()[finalRotation],
						facesDirections.Skip(face * 4).Take(4).ToArray()[(finalRotation + 2)%4]
					)
				).Set<Equal>(solver.FromConstant(1));
			}else{
				solver.Operation<MaterialImplication>(
					wasPicked,
					facesDirections.Skip(face * 4).Take(4).ToArray()[finalRotation]
				).Set<Equal>(solver.FromConstant(1));
			}
			
			solver.Operation<MaterialImplication>(
				wasPicked,
				edgeNumbers.Skip(face * 4 * 9).Skip(axisEnd * 9).Take(9).ToArray()[value - 1]
			).Set<Equal>(solver.FromConstant(1));
		}
	}
};

Action<int, int> setupEdges = (x, y) => {
	setupSingleEdge(x, y+1);
	setupSingleEdge(x+1, y);
	setupSingleEdge(x+1, y+2);
	setupSingleEdge(x+2, y+1);
};

Finally, we encode faces:

Action<int, int> setupSingleFace = (x, y) => {
	setupCorners(x, y);
	setupEdges(x, y);
};

Action setupFaces = () => {
	setupSingleFace(0, 3);
	setupSingleFace(3, 0);
	setupSingleFace(3, 3);
	setupSingleFace(3, 6);
	setupSingleFace(3, 9);
	setupSingleFace(6, 3);
};

setupFaces();

We run it and this is the result we get:

Tried aggregator 2 times.
MIP Presolve eliminated 7285 rows and 3504 columns.
MIP Presolve modified 1149 coefficients.
Aggregator did 3596 substitutions.
Reduced MIP has 979 rows, 844 columns, and 4885 nonzeros.
Reduced MIP has 844 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.03 sec. (15.56 ticks)
Found incumbent of value 0.000000 after 0.03 sec. (24.88 ticks)

Root node processing (before b&c):
  Real time             =    0.03 sec. (25.19 ticks)
Parallel b&c, 12 threads:
  Real time             =    0.00 sec. (0.00 ticks)
  Sync time (average)   =    0.00 sec.
  Wait time (average)   =    0.00 sec.
                          ------------
Total (root+branch&cut) =    0.03 sec. (25.19 ticks)
     ---                        ---
    |239|                      |333|
    |568|                      |3 3|
    |147|                      |333|
 --- --- --- ---           --- --- --- ---
|829|523|681|529|          |222|111|111|111|
|157|618|974|347|          |2 2|1 1|1 1|1 1|
|634|497|532|681|          |222|111|111|111|
 --- --- --- ---            --- --- --- ---
    |863|                      |111|
    |219|                      |1 1|
    |457|                      |111|
     ---                        ---

It took 30 milliseconds to find the answer. First implementation couldn’t do that in 8 hours. Not to mention that the first implementation ran on Gurobi in NEOS, and the second one was running with CPLEX on my local machine.

Reading the solution

Let’s read the solution. We can see that when we hold the cube in a way that the top side has center 6, front side has center 1, and bottom side has center 1, then the top side looks to the left, left side looks down, front and right and back and down sides look to the right. We can also see all the numbers assigned, so we know the “colors” of the pieces. We can now apply the regular algorithms for solving the cube.

The last remaining piece is how to rotate centers. There are two algorithms for that:

• Top center clockwise and front center counter-clockwise: f b’ l r’ u d’ f’ u’ d l’ r f’ b u
• Top center 180 degrees: u r l uu r’ l’ u r l uu r’ l’

We can now easily solve the cube:

Lessons learned

There are some important tricks we applied to optimize the solution:

1. We stored numbers as bitflags instead of storing them as integers. This is a common trick. If you know the range of the variables, then don’t use integers. Bitflags are much faster.
2. We precalcualted results outside of the model. Instead of creating a variable with a value of the face rotation, we calculated the rotation outside of the model, and then added a constraint (basically, an “if” condition in the ILP)
3. We didn’t compare numbers. Generally, don’t do that if it’s possible. Instead, just create a boolean flag indicating the result of comparison and use it later onw. The difference is subtle but improves the performance a lot.
4. We didn’t use “if else” conditions. They look easy, but they are really the performance killer.

With all these improvements in place, we managed to solve the cube in milliseconds.

This is the third part of the Distributed Designs series. For your convenience you can find other parts in the table of contents in Part 1 — Outbox without idempotency nor synchronous commit

Last time we saw how to use transactional outbox pattern with multiple databases and no synchronous commit. We also learned how to take the lock on the database end to make sure that we can scale out the Relay. However, what if we use Multi-version Concurrency Control (MVCC) or can’t enforce pessimistic locking in general? Can we implement the lock in that case?

Solution

We need to implement leases. The idea is:

• Create a table with leases
• Take the lease if it’s not taken yet
• Process rows
• Release the lease

The only tricky part is how to release the lease automatically in case of a crash. However, this we can do with timestamps. The idea is:

CREATE TABLE leases(name VARCHAR(MAX), lease_time DATETIME);
INSERT INTO leases(name, lease_time) VALUES ('lease_name', NULL);

Now, we want to take the lease if and only if it’s not taken yet. Let’s do this:

while(true){
   beginTransaction(REPEATABLE READ);
   lease_name, existingTimestamp = SELECT name, lease_date FROM leases WHERE lease_date < NOW() AND name = 'lease_name';
   if(lease_name IS NOT NULL) {
      UPDATE leases SET lease_date = NOW() + 1 minute WHERE name = 'lease_name';
      try{
          COMMIT; // First commit
      }catch{
          // Someone updated the lease before us. Let's try again
          // The transaction is now rolled back
          continue;
      }
      
      // beginTransaction(REPEATABLE READ); Process messages and set their status properly; COMMIT;

      beginTransaction(REPEATABLE READ);
      UPDATE leases SET lease_date = NOW() WHERE name = 'lease_name';
      COMMIT;
   }else {
      // We didn't find the lease, so it's not available
      // Let's roll back and back off
      ROLLBACK;
      sleep(5);
      continue;
   }
}

We take the lease row. If it’s missing, then it means that the lease is not available (someone else holds it). We wait and try again.

If the lease is available, then we try to take it. We try updating the row and book it for one minute. We then try to commit. If this fails, then it means that someone else modified the lease. We need to back off and try again.

However, if we succeed to take the lease, then we can get the messages from the outbox table. We don’t need to do anything special now because nobody else will fiddle with the outbox. We need to finish in one minute, and then we can release the lease.

Why does it work? What isolation level should I use?

Let’s stop for a moment and analyze why it even works and what isolation level we should use. We tried updating the lease with the following:

UPDATE leases SET lease_date = NOW() + 1 minute WHERE name = 'lease_name';

What we should in fact do is this:

UPDATE leases SET lease_date = NOW() + 1 minute WHERE name = 'lease_name' AND lease_date = existingTimestamp;

If we run this query with REPEATABLE READ, then the database engine simply can’t let the UPDATE to complete if someone else modified the row. That’s because the UPDATE needs to read the row again (to check the filtering criteria). Since we run on REPEATABLE READ, then the second read must return exactly the same data. Therefore, either nobody else modified the row, or the UPDATE fails and the transaction is rolled back.

Therefore, after the first commit we can be sure that we have the lease. I can’t really imagine a database that would claim that it meets the ACID requirements and would still let this commit to succeed just to break the data later on. Such a database would be a very interesting (not necessarily useful) case. Obviously, with distributed databases we may get some different isolation levels, some the actual optimizations may be different and break this mechanism. However, according to the SQL standard, this solution should work, as it simply implements the Compare-and-swap operation on the database level.

In short, this is your checklist:

• Use REPEATABLE READ
• If you can enforce eager locks in the database, just use them without and leases and rely on the locks maintained by the database engine
• If you can’t enforce eager locks (so the database engine uses optimistic locking), then implement the lease protocol defined above

Now you can scale your Relay to multiple instances and still get the correct results.

Summary

We implemented a generic lock for MVCC. You can use it for the transactional outbox pattern or for whatever else.

This is the second part of the Distributed Designs series. For your convenience you can find other parts in the table of contents in Part 1 — Outbox without idempotency nor synchronous commit

Last time we saw how to use transactional outbox pattern with multiple databases and no synchronous commit. We learned how to synchronize things between datacenters. The solution used delays in Relay component to get messages from the same datacenter only to avoid having the lock between databases.

Now, let’s consider another problem: can we scale out Relay? In other words, can we have multiple instances of Relay running in the same datacenter? Let’s see.

Should we scale Relay?

First, let’s be explicit: we most likely don’t need to scale the Relay. One instance is enough from the performance perspective. Obviously, there are cases when we have so many messages to propagate that we could benefit from parallelizing that, but it’s not as straightforward as it may seem. Relay needs to meet the following requirements:

• Ideally, Relay shouldn’t produce duplicates (on the happy path)
• Relay should process messages in the proper order. We don’t want to reorder the events if possible
• Relay should be fast. We should avoid locks and delays if possible

Being that said, it gets tricky to parallelize Relay. We need to send messages serially, so there is no easy way to make it faster.

However, we may need to scale out Relay because we run things in parallel by default and we can’t have just one instance. Without going into details whether it’s reasonable, we may be forced to run multiple instances of Relay. How to do it?

Naïve scaling

When people describe transactional outbox pattern, they typically focus on the idea to insert business entity and message entity in the same transaction. However, there is another important problem to solve: how to read the messages from the table to avoid duplicating messages sent to the queue? If you just scale out Relay, then you’ll effectively get duplicates.

Typically, Relay works this way:

openTransaction();
var messages = getMessagesFromTheDatabase();
foreach (var message in messages){
    sendMessageToTheQueue(message);
    markMessageAsSent(message);
}
commitTransaction();

Let’s say there are two instances of Relay. Both of them get messages from the database, both of them send them to the queue, and then both of them try to mark messages as sent and commit changes to the database. However, one instance will succeed, and the other instance will simply fail. This is not a problem per se, the message is still delivered to the queue. However, with this approach we will have duplicates on the happy path.

To solve that, we need to block the latter Relay instance from reading the rows that are being processed by the former instance. To do that, we need to make sure that locks are properly taken on the database end. Specifically, we need the following:

1. When reading a row, a lock is taken
2. The lock prevents other transactions from modifying the row until the end of the current transaction
3. The lock prevents other transaction from reading the row

Let’s examine one by one.

When reading a row, a lock is taken

This is done automatically by the database engine. Whenever we touch the row, the locks are taken appropriately.

The lock prevents other transactions from modifying the row until the end of the current transaction

This is seemingly easy. We have various database isolation levels. However, they typically focus on reading the data when they can be modified by other transaction. However, just preventing the modifications is not enough. Let’s see why.

First, let’s create the table:

CREATE TABLE dbo.t (a INT);
INSERT INTO dbo.t(a) VALUES (10);

Let’s now try running things in parallel with READ COMMITTED (the default) using MS SQL:

SET TRANSACTION ISOLATION LEVEL READ COMMITTED 
BEGIN TRANSACTION
SELECT * FROM dbo.t
                                                                             SET TRANSACTION ISOLATION LEVEL READ COMMITTED
                                                                             BEGIN TRANSACTION
                                                                             SELECT * FROM dbo.t
                                                                             UPDATE dbo.t SET a = 3
                                                                             COMMIT
UPDATE dbo.t SET a = 2
COMMIT

First transaction reads the row, takes the lock, and immediately releases it. Second transaction reads the row, updates it, and commits. First transaction updates the row and commits. There is no error here, no exception. It just works. This way, we get duplicates in the queue.

Let’s change the isolation level to REPEATABLE READ:

SET TRANSACTION ISOLATION LEVEL REPEATABLE READ
BEGIN TRANSACTION
SELECT * FROM dbo.t
                                                                             SET TRANSACTION ISOLATION LEVEL REPEATABLE READ
                                                                             BEGIN TRANSACTION
                                                                             SELECT * FROM dbo.t
                                                                             UPDATE dbo.t SET a = 3
                                                                             -- THIS HANGS
UPDATE dbo.t SET a = 2
-- Msg 1205, Level 13, State 45, Line 5
-- Transaction (Process ID 53) was deadlocked on lock 
-- resources with another process and has been chosen 
-- as the deadlock victim. Rerun the transaction.
                                                                             COMMIT

First transaction reads the row. Second transaction reads the row properly. However, when it tries to update it, the second transaction hangs. The first transaction then hangs the same way and gets killed. The second transaction finishes properly. As a result, we get the duplicate in the queue. However, we observed the error in the Relay, but we can’t help that. It’s too late. We get the same with SERIALIZABLE.

However, what if we try that with MySQL? Since MySQL with InnoDB uses snapshots for REPEATABLE READ, we get the following:

SET TRANSACTION ISOLATION LEVEL REPEATABLE READ;
START TRANSACTION;
SELECT * FROM dbo.t;

                                                                             SET TRANSACTION ISOLATION LEVEL REPEATABLE READ;
                                                                             START TRANSACTION;
                                                                             SELECT * FROM dbo.t;
                                                                             UPDATE dbo.t SET a = 3;
                                                                             COMMIT;

UPDATE dbo.t SET a = 2;
COMMIT;

This works with no issue. When we move to SERIALIZABLE, we get this:

SET TRANSACTION ISOLATION LEVEL REPEATABLE READ;
START TRANSACTION;
SELECT * FROM dbo.t;

                                                                             SET TRANSACTION ISOLATION LEVEL REPEATABLE READ;
                                                                             START TRANSACTION;
                                                                             SELECT * FROM dbo.t;
                                                                             UPDATE dbo.t SET a = 3;

UPDATE dbo.t SET a = 2;
-- ERROR 1213 (40001): Deadlock found when 
-- trying to get lock; try restarting transaction

                                                                             COMMIT;

Therefore, SERIALIZABLE makes the issue visible. Similarly, for Oracle we would get ORA-08177: can't serialize access for this transaction.

From the theoretical point of view, we need to use REPEATABLE READ isolation level. However, the problem is with the actual implementations. Typically, the database engine doesn’t try to predict the future, so the engine won’t stop the transaction from moving forward just because something wrong could happen. Instead, the engine decides to roll things back in case of issues. That’s why we get an error in the REPEATABLE READ or SERIALIZABLE examples above. This is not enough for us, though. We need to prevent others from reading the rows and not let them move forward. To see how to do that, let’s move on.

The lock prevents other transaction from reading the row

When we read about database isolation levels, they typically focus on preventing modifications to the row we want to read. However, they don’t cover how to prevent other transactions from reading the row at all. To do that, we can use the SELECT FOR UPDATE syntax. In practice, this is not a matter of the isolation level, but rather a case of taking the lock for updates and the internal database implementation. Let’s see how to do that in MS SQL:

SET TRANSACTION ISOLATION LEVEL READ COMMITTED 
BEGIN TRANSACTION
SELECT * FROM dbo.t WITH (UPDLOCK)
                                                                             SET TRANSACTION ISOLATION LEVEL READ COMMITTED
                                                                             BEGIN TRANSACTION
                                                                             SELECT * FROM dbo.t WITH (UPDLOCK)
                                                                             -- This waits
UPDATE dbo.t SET a = 2
COMMIT
                                                                             UPDATE dbo.t SET a = 3
                                                                             COMMIT

Similarly, we can do the same in MySQL or Oracle using SELECT * FROM dbo.t FOR UPDATE;.

This way we can block the row and make sure that no duplicates are sent to the queue. And notice that it works with READ COMMITTED. Read on to understand why.

What isolation level should I choose? And what about snapshots?

Let’s now consider what isolation level we should choose and why.

In theory, we need to go with REPEATABLE READ or above. That’s because READ COMMITTED guarantees that we read only the committed data. However, committed doesn’t mean latest. We can read a row that has its values updated already but these values are not committed yet. What’s worse, in theory we can read data that has been changed already and committed to the database. If we take that to the extreme, we could even always read the same empty result, because at some point that’s what was committed to the database. This is crazy, but if our transaction doesn’t modify the rows at all, then it’s perfectly valid according to the definition (and completely unreasonable and unexpected).

However, REPEATABLE READ makes it much more predictable. That’s because the UPDATE statement needs to read the rows again. Therefore, if the row was modified at some point and committed to the database, then the UPDATE would fail because it wouldn’t find the same row which is against the definition of REPEATABLE READ. Therefore, we need to go with REPEATABLE READ to make sure the result is correct at the very end.

Use REPEATABLE READ

However, we also need to prevent others from reading the rows. To guarantee that, we can either rely on the definitions or on the actual implementation. According to the definitions of the isolation levels, we must use at least REPEATABLE READ. But in order to block other readers, we need to understand whether the database uses pessimistic or optimistic locking. Typically, common SQL databases use pessimistic locking with optimizations, so they take locks as late as possible and escalate them as late as possible. We can enforce taking locks earlier by using FOR UPDATE syntax which makes the database to take the locks eagerly. The side effect of that is that the protocol we defined above works with READ COMMITTED. That’s just a coincidence, not something that we should rely on.

However, this approach won’t work for snapshot isolation and Multi-version Concurrency Control (MVCC). That’s because MVCC effectively instructs the database to take locks as late as possible. The database will either fail with FOR UPDATE syntax, or the database will simply ignore it and carry on with optimistic locking. We’ll see in the next post how to fix that.

In short: use REPEATABLE READ and take locks eagerly to avoid rollbacks. If you can’t take locks eagerly (because the database uses MVCC or forces optimistic locking), then you need a different protocol that I cover here

What about the performance?

We can see that this approach will not give us benefits. How can we process things faster and still maintain the order? The solution would be to read messages in batches, send these batches to the queue, but commit them only after. This would effectively create a transaction in the queue. It would look like this:

readFirstHundredRows();
sendThemToTheQueue();
                                                   readSecondHundredRows();
                                                   sendThemToTheQueue();
commitRows();
                                                   commitRows();

This way we can improve the performance. However, implementing this solution is hard and it requires the way to commit messages on the queue end which may not be supported.

Summary

Transactional outbox pattern requires not only the transaction for the business entity and the message, but also the careful extraction of the messages. It may be a little bit harder when we scale out Relay to run multiple instances.

This is the one hundred and fourth part of the ILP series. For your convenience you can find other parts in the table of contents in Part 1 – Boolean algebra

Today we are going to solve the 12 Stones Logic Puzzle. We have 12 stones, 11 of them are of equal weight, 1 is of unequal weight (could be lighter or heavier). We can use at most 3 weightings on a balance scale to find the odd stone and tell whether it’s lighter or heavier.

That’s gonna be a little bit tricky to understand, but let’s try it out. We want to implement an ILP model that will give us a recipe for finding the odd stone. Notice, that this problem seems to be even harder than NP class because we can’t verify the solution in polynomial time.

The idea is as follows:

• We create 24 lists. Each list contains exactly 3 integers. Each integer indicates which subset of stones to put on the left side of the scale, and which stones to put on the right side of the scale.
• Each list is supposed to determine the “designated stone”, so provide the weightings that will determine that the stone number is lighter (heavier).
• For each list, we calculate the results of weightings for every possible input (which stone is odd and how). This gives us a three dimensional list of [listId][number of weighting][which stone is odd and how].
• For each list, we make sure that we get unique weighting results for the “designated stone” of that list (so results of weightings for that list for other stones must be different).
• Each list must expect unique result of weightings.
• When two lists have the same prefix of how to put stones and what result to expect for first steps, then their -th step must be the same (to have deterministic solution).

That was quite a lot. Let’s see the code:

var stonesCount = 12;
var weightingsCount = 3;
var needToFindIfHeaverOrLigher = true;

// --------------------------------------------------------

// [listId][whichWeighting][whichStone][wasLeftLighter + wasRightLighter + wasEqual]
var weightingResultsCount = 3;
var weightingResults = Enumerable.Range(0, 2*stonesCount).Select(listId =>
	// Number of weighting
	Enumerable.Range(0, weightingsCount).Select(weighting =>
		// stone 1 lighter, stone 1 heavier, stone 2 lighter, stone 2 heavier, ...
		Enumerable.Range(0, 2 * stonesCount).Select(stoneId => 
			// wasLeftLighter, wasRightLighter, wasEqual
			Enumerable.Range(0, weightingResultsCount).Select(resultId => 
				solver.CreateAnonymous(Domain.BinaryInteger)
			).ToArray()
		).ToArray()
	).ToArray()
).ToArray();

// For each list, for each weighting, for each stone, exactly one result is possible
for(int listId = 0; listId < 2 * stonesCount; ++listId){
	for(int weighting = 0; weighting < weightingsCount; ++weighting){
		for(int stoneId = 0; stoneId < 2 * stonesCount; ++stoneId){
			solver.Operation<Addition>(weightingResults[listId][weighting][stoneId]).Set<Equal>(solver.FromConstant(1));
		}
	}
}


// [listId][whichWeighting][putOnLeft, putOnRight]		
// Stone 1 lighter, stone 1 heavier, stone 2 lighter, stone 2 heavier, stone 3 lighter...
var weightingLists = Enumerable.Range(0, 2*stonesCount).Select(listId =>
	// Number  of weighting
	Enumerable.Range(0, weightingsCount).Select(weighting =>
		// stone 1 on left, stone 2 on left, stone 3 on left, ..., stone #stonesCount on left, stone 1 on right...
		Enumerable.Range(0, 2 * stonesCount).Select(stoneId => 
			solver.CreateAnonymous(Domain.BinaryInteger)
		).ToArray()
	).ToArray()
).ToArray();

// For each list, for each weighting, make sure that we put some stone on the scale
for(int listId = 0; listId < 2 * stonesCount; ++listId){
	for(int weighting = 0; weighting < weightingsCount; ++weighting){
		solver.Operation<Addition>(weightingLists[listId][weighting]).Set<GreaterOrEqual>(solver.FromConstant(1));
	}
}

// For each list, for each weighting, make sure that each stone is either on the left, or on the right, or nowhere
for(int listId = 0; listId < 2 * stonesCount; ++listId){
	for(int weighting = 0; weighting < weightingsCount; ++weighting){
		for(int stoneId = 0; stoneId < stonesCount; ++stoneId){
			solver
				.Operation<Addition>(weightingLists[listId][weighting][stoneId], weightingLists[listId][weighting][stonesCount + stoneId])
				.Set<LessOrEqual>(solver.FromConstant(1));
		}
	}
}


// For each list, for each weighting, calculate the result based on the known input
for(int listId = 0; listId < 2 * stonesCount; ++listId){
	for(int weighting = 0; weighting < weightingsCount; ++weighting){
		for(int stoneId = 0; stoneId < 2 * stonesCount; ++stoneId){
			var stonesCountOnTheLeft = solver.Operation<Addition>(weightingLists[listId][weighting].Take(stonesCount).ToArray());
			var stonesCountOnTheRight = solver.Operation<Addition>(weightingLists[listId][weighting].Skip(stonesCount).Take(stonesCount).ToArray());
			
			var isThisListForLighterCase = stoneId % 2 == 0;
			
			var hasSpecialStoneOnLeft = weightingLists[listId][weighting][stoneId/2];
			var hasSpecialStoneOnRight = weightingLists[listId][weighting][stonesCount + stoneId/2];
			
			// Left has fewer stones (left is lighter)
			solver.Operation<MaterialImplication>(
				stonesCountOnTheLeft.Operation<IsLessThan>(stonesCountOnTheRight),
				weightingResults[listId][weighting][stoneId][0]
			).Set<Equal>(solver.FromConstant(1));
			
			// Right has fewer stones (right is lighter)
			solver.Operation<MaterialImplication>(
				stonesCountOnTheLeft.Operation<IsGreaterThan>(stonesCountOnTheRight),
				weightingResults[listId][weighting][stoneId][1]
			).Set<Equal>(solver.FromConstant(1));
			
			// Have equal stones
			if(isThisListForLighterCase){
				// Lighter stone is on the left (left is lighter)
				solver.Operation<MaterialImplication>(
					stonesCountOnTheLeft.Operation<IsEqual>(stonesCountOnTheRight)
						.Operation<Conjunction>(hasSpecialStoneOnLeft),
					weightingResults[listId][weighting][stoneId][0]
				).Set<Equal>(solver.FromConstant(1));
				
				// Lighter stone is on the right (right is lighter)
				solver.Operation<MaterialImplication>(
					stonesCountOnTheLeft.Operation<IsEqual>(stonesCountOnTheRight)
						.Operation<Conjunction>(hasSpecialStoneOnRight),
					weightingResults[listId][weighting][stoneId][1]
				).Set<Equal>(solver.FromConstant(1));
				
				// There is no lighter stone here (are equal)
				solver.Operation<MaterialImplication>(
					stonesCountOnTheLeft.Operation<IsEqual>(stonesCountOnTheRight)
						.Operation<Conjunction>(hasSpecialStoneOnLeft.Operation<BinaryNegation>(), hasSpecialStoneOnRight.Operation<BinaryNegation>()),
					weightingResults[listId][weighting][stoneId][2]
				).Set<Equal>(solver.FromConstant(1));
			}else {
				// Heavier stone is on the left (righti s lighter)
				solver.Operation<MaterialImplication>(
					stonesCountOnTheLeft.Operation<IsEqual>(stonesCountOnTheRight)
						.Operation<Conjunction>(hasSpecialStoneOnLeft),
					weightingResults[listId][weighting][stoneId][1]
				).Set<Equal>(solver.FromConstant(1));
				
				// Heavier stone is on the right (left is lighter)
				solver.Operation<MaterialImplication>(
					stonesCountOnTheLeft.Operation<IsEqual>(stonesCountOnTheRight)
						.Operation<Conjunction>(hasSpecialStoneOnRight),
					weightingResults[listId][weighting][stoneId][0]
				).Set<Equal>(solver.FromConstant(1));
				
				// There is no heavier stone here (are equal)
				solver.Operation<MaterialImplication>(
					stonesCountOnTheLeft.Operation<IsEqual>(stonesCountOnTheRight)
						.Operation<Conjunction>(hasSpecialStoneOnLeft.Operation<BinaryNegation>(), hasSpecialStoneOnRight.Operation<BinaryNegation>()),
					weightingResults[listId][weighting][stoneId][2]
				).Set<Equal>(solver.FromConstant(1));
			}
		}
	}
}


// For each list pair, for each prefix length, check if prefixes are the same and the weighting results are the same, then next step must be the same
for(int listId = 0; listId < 2 * stonesCount; ++listId){
	for(int listId2 = listId + 1; listId2 < 2 * stonesCount; ++listId2){
		var arePrefixesEqual = solver.FromConstant(1);
		for(int prefixLength = 0; prefixLength < weightingsCount; ++ prefixLength){
			for(int stoneId = 0; stoneId < 2*stonesCount; ++stoneId){
				solver
					.Operation<MaterialImplication>(
						arePrefixesEqual,
						weightingLists[listId][prefixLength][stoneId].Operation<IsEqual>(weightingLists[listId2][prefixLength][stoneId])
					).Set<Equal>(solver.FromConstant(1));
			}
			
			for(int stoneId = 0; stoneId < 2*stonesCount; ++stoneId){
				arePrefixesEqual = arePrefixesEqual.Operation<Conjunction>(
					weightingLists[listId][prefixLength][stoneId].Operation<IsEqual>(weightingLists[listId2][prefixLength][stoneId])
				);
			}
			
			for(int weightingResult = 0; weightingResult < weightingResultsCount; ++weightingResult){
				arePrefixesEqual = arePrefixesEqual.Operation<Conjunction>(
					weightingResults[listId][prefixLength][listId][weightingResult]
					.Operation<IsEqual>(weightingResults[listId2][prefixLength][listId2][weightingResult])
				);
			}
		}
	}
}

// All list pairwise must have different expected stones and results
for(int listId = 0; listId < 2 * stonesCount; ++listId){
	for(int listId2 = listId + 1; listId2 < 2 * stonesCount; ++listId2){
		if(needToFindIfHeaverOrLigher == false && listId % 2 == 0 && listId2 == listId + 1){
			continue;
		}
	
		var areBothEqual = solver.FromConstant(1);
		for(int weighting = 0; weighting < weightingsCount; ++ weighting){
			for(int stoneId = 0; stoneId < 2*stonesCount; ++stoneId){
				areBothEqual = areBothEqual.Operation<Conjunction>(
					weightingLists[listId][weighting][stoneId].Operation<IsEqual>(weightingLists[listId2][weighting][stoneId])
				);
			}
			
			for(int weightingResult = 0; weightingResult < weightingResultsCount; ++weightingResult){
				areBothEqual = areBothEqual.Operation<Conjunction>(
					weightingResults[listId][weighting][listId][weightingResult].Operation<IsEqual>(weightingResults[listId2][weighting][listId2][weightingResult])
				);
			}
		}
		
		areBothEqual.Set<Equal>(solver.FromConstant(0));
	}
}


// For each list, the designated stone must have different results than results for other stones
for(int listId = 0; listId < 2 * stonesCount; ++listId){
	for(int otherList = 0; otherList < 2 * stonesCount; ++otherList){
		if(listId == otherList){
			continue;
		}
		
		if(needToFindIfHeaverOrLigher == false && ((listId % 2 == 0 && otherList == listId + 1) || (listId % 2 == 1 && otherList == listId - 1))){
			continue;
		}
		
		var areBothEqual = solver.FromConstant(1);
		for(int weighting = 0; weighting < weightingsCount; ++ weighting){
			for(int weightingResult = 0; weightingResult < weightingResultsCount; ++weightingResult){
				areBothEqual = areBothEqual.Operation<Conjunction>(
					weightingResults[listId][weighting][listId][weightingResult].Operation<IsEqual>(weightingResults[listId][weighting][otherList][weightingResult])
				);
			}
		}
		
		areBothEqual.Set<Equal>(solver.FromConstant(0));
	}
}

solver.AddGoal("goal", solver.FromConstant(0));
solver.Solve();


for(int listId = 0; listId < 2 * stonesCount; ++listId){
	Console.Write("Stone {0} {1}: ", listId/2 + 1, listId %2 == 0 ? "lighter" : "heavier");
	for(int weighting = 0; weighting < weightingsCount; ++weighting){
		var stonesOnTheLeft = string.Join(",", Enumerable
			.Range(0, stonesCount)
			.Select(stoneId => Tuple.Create(stoneId + 1, Math.Round(solver.GetValue(weightingLists[listId][weighting][stoneId])) > 0.5))
			.Where(tuple => tuple.Item2)
			.Select(tuple => tuple.Item1));
		var stonesOnTheRight = string.Join(",", Enumerable
			.Range(0, stonesCount)
			.Select(stoneId => Tuple.Create(stoneId + 1, Math.Round(solver.GetValue(weightingLists[listId][weighting][stonesCount + stoneId])) > 0.5))
			.Where(tuple => tuple.Item2)
			.Select(tuple => tuple.Item1));
			
		var weightingResult = Math.Round(solver.GetValue(weightingResults[listId][weighting][listId][0])) > 0.5
			? ">"
			: Math.Round(solver.GetValue(weightingResults[listId][weighting][listId][1])) > 0.5
				? "<"
				: Math.Round(solver.GetValue(weightingResults[listId][weighting][listId][2])) > 0.5
					? "="
					: "Something very wrong!";
			
		Console.Write("({0} ; {1}) [{2}] ; ", stonesOnTheLeft, stonesOnTheRight, weightingResult);
	}
	Console.WriteLine();
}

We set initial conditions in lines 1-3.

Next, we create the variables for weighting results (lines 7-20). That’s the four dimensional array. First dimension indicates which list this refers to. Second dimension indicates which weighting we perform (we have exactly 3 weightings in this scenario). Third level is for indicating which stone is odd (from the input). Last dimension consists of three binaries: whether the left side was lighter (moved up), whether the right side was lighter, whether both sides were equal.

Next, we make sure that we can get only one result for each weighting. This is in lines 22-29.

Next step defines another part of the model we have (lines 32-42). We need to define variables indicating which stones to put on the scale in each step. This is three dimensional array. First dimension indicates which list we have. Second dimension indicates which weighting we consider. Third dimension consists of 24 binaries: first 12 binaries indicate whether a given stone was put on the left side. Next 12 binaries do the same for the right side of the scale.

We now need to encode correctness conditions for the scale. First, we want to make sure, that we put some stones on the scale for each weighting. This is in lines 44-49. We basically take all the variables from the third dimension and make sure they are not all zeroes.

Next, we make sure that if we put a stone on the left side of the scale, then we don’t put it on the right side (and the opposite). This is in lines 51-60.

Next comes the core of the weightings. We need to calculate the result for a given list. ILP will evaluate some subset of stones to put on the scale, and we need to calculate how the scale moves. This is in lines 63-133. We iterate over every list, over every weighting, and over every instance of the input (which stone is odd and how). We then calculate some helper variables indicating whether we put more stones on one of the sides, whether this list is for checking if the stone is lighter or heavier, and whether the special stone has been put on the scale (and on which side). We then encode if conditions to make sure that the result of the weighting is stored properly.

Once we have that, we need to make sure, that our lists can actually identify the solution. We first make sure, that the algorithm we produce is deterministic. For each pair of lists, we take their prefix of steps, and if the prefixes match (so both lists tried weighting the same stones and expected the same results), then next step in both of the lists (which stones to put on the scale) must be the same. This is in lines 136-163.

Now, we need to make sure that our lists generate unique solutions. First, let’s take some list that is supposed to confirm that the third stone is lighter. We get the subsets of stones to weigh, we get the results of the weightings. We need to make sure that the result is unique, so for every other stone from the input we would get different results in weightings. This is in lines 165-.

Finally, we need to make sure that all 24 lists generate some unique weightings. If that’s the case, then we can be sure, that we get the proper algorithm for finding the odd stone. This is in lines 192-214.

We then solve the problem, and we print the solution.

Here comes some sample output:

var stonesCount = 4;
var weightingsCount = 3;
var needToFindIfHeaverOrLigher = true;

Tried aggregator 3 times.
MIP Presolve eliminated 9067 rows and 4572 columns.
MIP Presolve modified 33516 coefficients.
Aggregator did 10560 substitutions.
Reduced MIP has 24673 rows, 12164 columns, and 91360 nonzeros.
Reduced MIP has 12164 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.14 sec. (122.11 ticks)
Probing time = 0.09 sec. (45.11 ticks)
Tried aggregator 1 time.
MIP Presolve eliminated 580 rows and 290 columns.
Reduced MIP has 24093 rows, 11874 columns, and 89620 nonzeros.
Reduced MIP has 11874 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.08 sec. (63.97 ticks)
Probing time = 0.13 sec. (41.80 ticks)
Clique table members: 56542.
MIP emphasis: balance optimality and feasibility.
MIP search method: dynamic search.
Parallel mode: deterministic, using up to 12 threads.
Root relaxation solution time = 0.25 sec. (233.38 ticks)

        Nodes                                         Cuts/
   Node  Left     Objective  IInf  Best Integer    Best Bound    ItCnt     Gap

      0     0        0.0000  3549                      0.0000     5007
      0     0        0.0000  4634                  Cuts: 3327     8757
      0     0        0.0000  4153                  Cuts: 3136    12012
      0     0        0.0000  3716                  Cuts: 4801    14696
      0     0        0.0000  4840                  Cuts: 2543    16843
      0     2        0.0000  2182                      0.0000    16843
Elapsed time = 21.00 sec. (11370.65 ticks, tree = 0.01 MB, solutions = 0)
      3     5        0.0000  2182                      0.0000    17507
      7     9        0.0000  2843                      0.0000    19561
     12    14        0.0000  3079                      0.0000    27692
     17    19        0.0000  1784                      0.0000    32431
     22    24        0.0000  3615                      0.0000    40876
     33    35        0.0000   910                      0.0000    53631
     51    53        0.0000  1607                      0.0000    64149
    262   244        0.0000   999                      0.0000    88749
    271   245        0.0000  1496                      0.0000    99688
    359   289        0.0000   614                      0.0000   134357
Elapsed time = 32.19 sec. (16729.64 ticks, tree = 2.19 MB, solutions = 0)
    665   533        0.0000   813                      0.0000   171436
   1011   771        0.0000  1127                      0.0000   198237
   1441   975    infeasible                            0.0000   254716
   1524   971        0.0000  1466                      0.0000   296856
   1726  1087    infeasible                            0.0000   366176
   1899  1183        0.0000  1400                      0.0000   406975
   2235  1384    infeasible                            0.0000   464046
   2283  1387        0.0000  1261                      0.0000   503516
   2343  1395        0.0000  1740                      0.0000   548927
   2592  1537        0.0000   906                      0.0000   600827
Elapsed time = 60.58 sec. (27170.42 ticks, tree = 27.86 MB, solutions = 0)
   2882  1712        0.0000  1367                      0.0000   646003
   2907  1699    infeasible                            0.0000   683087
   2968  1676        0.0000  1964                      0.0000   777718
   2987  1677        0.0000  2320                      0.0000   797273
   3067  1701        0.0000  1557                      0.0000   852616
   3116  1708        0.0000  1854                      0.0000   906596
   3133  1725        0.0000  2004                      0.0000   917695
   3241  1771        0.0000  2111                      0.0000   952497
   3608  1922    infeasible                            0.0000  1057357
   3647  1893    infeasible                            0.0000  1096427
Elapsed time = 97.08 sec. (39043.42 ticks, tree = 27.39 MB, solutions = 0)
   3689  1893        0.0000  1526                      0.0000  1141849
   3703  1893        0.0000  1661                      0.0000  1153728
   3820  1870        0.0000  1386                      0.0000  1268057
   3862  1868    infeasible                            0.0000  1308167
   3902  1856    infeasible                            0.0000  1352170
   3967  1863    infeasible                            0.0000  1401294
   4019  1863    infeasible                            0.0000  1444617
*  4162+ 1800                            0.0000        0.0000  1504384    0.00%

GUB cover cuts applied:  112
Clique cuts applied:  548
Cover cuts applied:  1729
Implied bound cuts applied:  5596
Mixed integer rounding cuts applied:  598
Zero-half cuts applied:  1053
Gomory fractional cuts applied:  32

Root node processing (before b&c):
  Real time             =   20.80 sec. (11242.73 ticks)
Parallel b&c, 12 threads:
  Real time             =   99.58 sec. (35940.06 ticks)
  Sync time (average)   =   13.62 sec.
  Wait time (average)   =    0.00 sec.
                          ------------
Total (root+branch&cut) =  120.38 sec. (47182.78 ticks)
Stone 1 lighter: (2 ; 4) [=] ; (3 ; 4) [=] ; (1,2 ; 3,4) [>] ;
Stone 1 heavier: (2 ; 4) [=] ; (3 ; 4) [=] ; (1,2 ; 3,4) [<] ;
Stone 2 lighter: (2 ; 4) [>] ; (1,3 ; 2,4) [<] ; (3 ; 2) [<] ;
Stone 2 heavier: (2 ; 4) [<] ; (1,3 ; 2,4) [>] ; (3,4 ; 2) [<] ;
Stone 3 lighter: (2 ; 4) [=] ; (3 ; 4) [>] ; ( ; 3,4) [>] ;
Stone 3 heavier: (2 ; 4) [=] ; (3 ; 4) [<] ; (1,4 ; 3) [<] ;
Stone 4 lighter: (2 ; 4) [<] ; (1,3 ; 2,4) [<] ; ( ; 3) [>] ;
Stone 4 heavier: (2 ; 4) [>] ; (1,3 ; 2,4) [>] ; (2 ; ) [<] ;

Let’s see how to read that. In this simpler example, we consider 4 stones, 3 weightings, we want to find whether the odd stone is heavier or lighter. Notice, that first step in all of the lists is the same. This makes sense (we actually enforced that), because we need to have a deterministic algorithm. Pick any input instance you want to verify. Let’s say, that we assume, that the odd stone is the stone number 3, and the stone is heavier.

We take the first list from the top, and we perform the first weighting. The solution tells us to weigh stones 2 (on the left) and 4 (on the right). We weight them together. Since we know that the odd stone is the stone number 3, we know the result of this weighting will be “both sides are equal”. We see that the first list expected the result to be equal (just like second, fifth, and sixth list). Since our first list is still correct, we move to the second step of the list.

This time we need to weigh stones 3 (on the left) and 4 (on the right). We know the stone number 3 is heavier, we get the result indicated as “<" (meaning that the left side is lower than the right one). We see that the first list expects a different result. So does the second list. Third, fourth, and fifth lists expected different results in the first step. So we move to the sixth list. That list matches our results, so we move to the third step. In the third step we weigh stones 1 and 4 (on the left) with the stone number 3 (on the right). Since we have two stones on the left, the left side is heavier This is exactly what this list expects. So we know that the odd stone is the stone number 3, and that the stone is heavier (as indicated by the list). We can try other inputs. Notice, that only one list will take us through all the steps properly. Let's see another example:

var stonesCount = 4;
var weightingsCount = 2;
var needToFindIfHeaverOrLigher = false;

Tried aggregator 3 times.
MIP Presolve eliminated 7691 rows and 3892 columns.
MIP Presolve modified 21184 coefficients.
Aggregator did 6560 substitutions.
Reduced MIP has 13789 rows, 6780 columns, and 53032 nonzeros.
Reduced MIP has 6780 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.09 sec. (78.93 ticks)
Probing time = 0.03 sec. (22.20 ticks)
Tried aggregator 1 time.
MIP Presolve eliminated 420 rows and 210 columns.
Reduced MIP has 13369 rows, 6570 columns, and 51772 nonzeros.
Reduced MIP has 6570 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.05 sec. (37.15 ticks)
Probing time = 0.06 sec. (19.96 ticks)
Clique table members: 32370.
MIP emphasis: balance optimality and feasibility.
MIP search method: dynamic search.
Parallel mode: deterministic, using up to 12 threads.
Root relaxation solution time = 0.16 sec. (140.05 ticks)

        Nodes                                         Cuts/
   Node  Left     Objective  IInf  Best Integer    Best Bound    ItCnt     Gap

      0     0        0.0000  2081                      0.0000     2874
*     0+    0                            0.0000        0.0000     4886    0.00%
      0     0        cutoff              0.0000        0.0000     4886    0.00%
Elapsed time = 1.92 sec. (1598.36 ticks, tree = 0.00 MB, solutions = 1)

GUB cover cuts applied:  387
Clique cuts applied:  471
Cover cuts applied:  543
Implied bound cuts applied:  673
Mixed integer rounding cuts applied:  89
Zero-half cuts applied:  262
Lift and project cuts applied:  3
Gomory fractional cuts applied:  46

Root node processing (before b&c):
  Real time             =    1.92 sec. (1598.96 ticks)
Parallel b&c, 12 threads:
  Real time             =    0.00 sec. (0.00 ticks)
  Sync time (average)   =    0.00 sec.
  Wait time (average)   =    0.00 sec.
                          ------------
Total (root+branch&cut) =    1.92 sec. (1598.96 ticks)
Stone 1 lighter: (1 ; 2) [>] ; (1 ; 3) [>] ;
Stone 1 heavier: (1 ; 2) [<] ; (4 ; 1) [>] ;
Stone 2 lighter: (1 ; 2) [<] ; (4 ; 1) [=] ;
Stone 2 heavier: (1 ; 2) [>] ; (1 ; 3) [=] ;
Stone 3 lighter: (1 ; 2) [=] ; (4 ; 2) [=] ;
Stone 3 heavier: (1 ; 2) [=] ; (4 ; 2) [=] ;
Stone 4 lighter: (1 ; 2) [=] ; (4 ; 2) [>] ;
Stone 4 heavier: (1 ; 2) [=] ; (4 ; 2) [<] ;

We have 4 stones and 2 weightings this time, but we only need to find the odd stone, without telling whether it's heavier or lighter. Let's assume once again, that our odd stone is the stone number 3, and that the stone is heavier. Let's take first step. We weigh stones 1 and 2, we get that they are equal. There are four lists that match this result. Let's take first list from the top that works for us, that is the list number 5. Second step asks us to weigh stones 4 and 2. We know these stones are equal. However, this time we have at least two lists that match this input. Those are lists 5 and 6. Both of them indicate that the odd stone is the stone number 3, but we can't tell whether the stone is lighter or heavier. Let's take another example. Again, 4 stones and 2 weightings, but this time we want to know whether the stone is heavier or lighter:

var stonesCount = 4;
var weightingsCount = 2;
var needToFindIfHeaverOrLigher = true;


Tried aggregator 3 times.
MIP Presolve eliminated 7979 rows and 4028 columns.
MIP Presolve modified 22428 coefficients.
Aggregator did 6816 substitutions.
Reduced MIP has 14617 rows, 7204 columns, and 55456 nonzeros.
Reduced MIP has 7204 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.08 sec. (81.46 ticks)
Probing time = 0.05 sec. (23.52 ticks)
Tried aggregator 1 time.
MIP Presolve eliminated 470 rows and 235 columns.
Reduced MIP has 14147 rows, 6969 columns, and 54046 nonzeros.
Reduced MIP has 6969 binaries, 0 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.05 sec. (38.83 ticks)
Probing time = 0.05 sec. (21.59 ticks)
Clique table members: 33914.
MIP emphasis: balance optimality and feasibility.
MIP search method: dynamic search.
Parallel mode: deterministic, using up to 12 threads.
Root relaxation solution time = 0.16 sec. (157.25 ticks)

        Nodes                                         Cuts/
   Node  Left     Objective  IInf  Best Integer    Best Bound    ItCnt     Gap

      0     0        0.0000  2151                      0.0000     3069
      0     0        0.0000  3063                  Cuts: 1847     5294
      0     0        0.0000  2630                  Cuts: 1606     7065
      0     0        0.0000  2707                  Cuts: 3502     8995
      0     2        0.0000  1516                      0.0000     8995
Elapsed time = 9.16 sec. (6396.65 ticks, tree = 0.01 MB, solutions = 0)
      4     6        0.0000  1515                      0.0000     9602
      8    10        0.0000   946                      0.0000    12439
      9    11        0.0000  1474                      0.0000    14376
     16    18        0.0000   880                      0.0000    24078
     17    19        0.0000  1551                      0.0000    25430
     18    20        0.0000  2182                      0.0000    28371
     22    24        0.0000  1662                      0.0000    33220
     25    27        0.0000  2197                      0.0000    37737
     29    31        0.0000   950                      0.0000    41055
     81    77    infeasible                            0.0000    82804
Elapsed time = 16.22 sec. (11603.06 ticks, tree = 0.24 MB, solutions = 0)
    141    77    infeasible                            0.0000   130504
    207    84        0.0000   573                      0.0000   171817
    220    87        0.0000  1161                      0.0000   181888
    741   338        0.0000   502                      0.0000   261716
   1838   624        0.0000   511                      0.0000   306384
   2706   799        0.0000   473                      0.0000   364713
   2963   678        0.0000   968                      0.0000   447687
   3744   828    infeasible                            0.0000   495342
   4342   769    infeasible                            0.0000   567069
   4873   700        0.0000   749                      0.0000   643508
Elapsed time = 38.22 sec. (21634.35 ticks, tree = 0.71 MB, solutions = 0)
   5550  1011        0.0000   336                      0.0000   688323
   6408  1119    infeasible                            0.0000   753821
   6540   987    infeasible                            0.0000   889211
   6796   733    infeasible                            0.0000  1027923
   6887   668    infeasible                            0.0000  1082863
   7035   566    infeasible                            0.0000  1145077
   7310   401        0.0000   927                      0.0000  1247273
   7751   491        0.0000  1013                      0.0000  1288255
   8500   656        0.0000   769                      0.0000  1339779
   9399   708    infeasible                            0.0000  1414407
Elapsed time = 61.05 sec. (31695.72 ticks, tree = 1.13 MB, solutions = 0)
   9512   619        0.0000   638                      0.0000  1450005
   9620   548        0.0000   353                      0.0000  1485033
   9951   378        0.0000  1112                      0.0000  1602006
  10659   541        0.0000   241                      0.0000  1652664
  11056   602        0.0000   920                      0.0000  1686445
  11872   693        0.0000   899                      0.0000  1743247
  12902   674    infeasible                            0.0000  1823367
  13059   541    infeasible                            0.0000  1885856
  13184   450        0.0000   599                      0.0000  1924334
  13375   311        0.0000  1101                      0.0000  1990600
Elapsed time = 85.00 sec. (42071.90 ticks, tree = 0.33 MB, solutions = 0)
  13521   350        0.0000  1249                      0.0000  2016520
  14049   423        0.0000   987                      0.0000  2064605
  14529   468        0.0000  1053                      0.0000  2104572
  15776   529    infeasible                            0.0000  2220194
  15884   423    infeasible                            0.0000  2273648
  15975   355        0.0000  2000                      0.0000  2332887
  16153   353        0.0000  1040                      0.0000  2400556
  16231   385        0.0000   896                      0.0000  2408262
  16709   630        0.0000  1306                      0.0000  2457290
  17633   875        0.0000  1893                      0.0000  2553832
Elapsed time = 110.98 sec. (53742.88 ticks, tree = 0.69 MB, solutions = 0)
  17655   887        0.0000  2059                      0.0000  2572045
  17739   925        0.0000  2061                      0.0000  2592268
  18467  1245    infeasible                            0.0000  2809240
  18490  1222    infeasible                            0.0000  2862765
  18509  1203    infeasible                            0.0000  2894288
  18538  1174    infeasible                            0.0000  2954243
  18550  1162    infeasible                            0.0000  2977278
  18603  1111    infeasible                            0.0000  3071110
  18632  1082    infeasible                            0.0000  3113050
  18657  1057    infeasible                            0.0000  3152949
Elapsed time = 139.20 sec. (65489.88 ticks, tree = 1.02 MB, solutions = 0)
  18703  1035        0.0000  1538                      0.0000  3215507
  18766   992        0.0000  1513                      0.0000  3289399
  18773   991        0.0000  1954                      0.0000  3299613
  18785   987        0.0000  1870                      0.0000  3317451
  18810   968    infeasible                            0.0000  3353816
  18937   848        0.0000  1405                      0.0000  3504999
  18945   840    infeasible                            0.0000  3513374
  19002   807        0.0000  1521                      0.0000  3552254
  19027   788        0.0000   889                      0.0000  3567473
  19074   757        0.0000  1516                      0.0000  3598113
Elapsed time = 174.28 sec. (78644.14 ticks, tree = 0.72 MB, solutions = 0)
  19209   688        0.0000  1421                      0.0000  3671212
  19576   636        0.0000  1336                      0.0000  3793448
  19876   730        0.0000  1286                      0.0000  3830126
  20633   786        0.0000  1087                      0.0000  3919803
  20698   783        0.0000  1761                     -0.0000  3938066
  20701   783        0.0000  1772                     -0.0000  3939038
  20706   784        0.0000  1737                     -0.0000  3941101
  20712   785        0.0000  1527                     -0.0000  3943797
  20723   792        0.0000  1686                     -0.0000  3948083
  20744   802        0.0000  1368                     -0.0000  3960461
Elapsed time = 214.22 sec. (104503.67 ticks, tree = 7.09 MB, solutions = 0)
  20836   823        0.0000  1726                     -0.0000  3986141
  21274   760        0.0000   802                     -0.0000  4028859
  22072   706        0.0000   555                     -0.0000  4079944
  22658   913        0.0000   587                     -0.0000  4118471
  23413  1131        0.0000   638                     -0.0000  4165697
  24085  1269        0.0000  1102                     -0.0000  4208939
  24697  1362        0.0000  1467                     -0.0000  4249456
  24707  1364        0.0000  1395                     -0.0000  4250658
  24823  1048        0.0000  1095                     -0.0000  4257228
  25065  1071    infeasible                           -0.0000  4300075
Elapsed time = 239.13 sec. (123018.58 ticks, tree = 13.01 MB, solutions = 0)
  25299  1026        0.0000  1528                     -0.0000  4346987
  25703   880        0.0000  1260                     -0.0000  4413791
  25956   726        0.0000  1484                     -0.0000  4464113
  26326   642    infeasible                           -0.0000  4531938
  26709   764        0.0000  1392                     -0.0000  4600736
  27194   830        0.0000  1504                     -0.0000  4690663
  27505   881    infeasible                           -0.0000  4754242
  27728   910        0.0000  1401                     -0.0000  4805393
  28143   972    infeasible                           -0.0000  4890255
  29468  1242        0.0000  1129                     -0.0000  5156954
Elapsed time = 268.17 sec. (135740.89 ticks, tree = 0.72 MB, solutions = 0)
  30823  1629        0.0000  1514                     -0.0000  5412126
  32350  1829    infeasible                           -0.0000  5718157
  33681  2055        0.0000  1806                     -0.0000  5982692
  35083  2390        0.0000  1073                     -0.0000  6250237
  36581  2505        0.0000  1043                     -0.0000  6529869
  37841  2625    infeasible                           -0.0000  6817490
  39098  2867    infeasible                           -0.0000  7048531
  40747  3107    infeasible                           -0.0000  7290962
  42603  3141        0.0000  1660                     -0.0000  7563118
  44182  3230    infeasible                           -0.0000  7819515
Elapsed time = 361.98 sec. (174394.28 ticks, tree = 4.79 MB, solutions = 0)
  45619  3223    infeasible                           -0.0000  8097725
  46934  3130        0.0000  1454                     -0.0000  8347398
  48243  3130    infeasible                           -0.0000  8596902
  49646  3295        0.0000  1690                     -0.0000  8877792
  51457  3485        0.0000  1713                     -0.0000  9148822
  53014  3570    infeasible                           -0.0000  9418591
  54081  3625        0.0000  1030                     -0.0000  9606215
  55525  3715        0.0000  1189                     -0.0000  9877402
  56700  3928        0.0000   855                     -0.0000 10075168
  58063  4056    infeasible                           -0.0000 10333360
Elapsed time = 456.38 sec. (212954.00 ticks, tree = 10.13 MB, solutions = 0)
  59500  4151        0.0000  1234                     -0.0000 10584348
  60939  4343    infeasible                           -0.0000 10827749
  62208  4431        0.0000   936                     -0.0000 11070122
  63869  4520    infeasible                           -0.0000 11332455
  65291  4460    infeasible                           -0.0000 11588607
  66927  4504    infeasible                           -0.0000 11858213
  67955  4528        0.0000  1910                     -0.0000 12076043
  69355  4604    infeasible                           -0.0000 12348814
  70699  4650    infeasible                           -0.0000 12610568
  71789  4734        0.0000  1329                     -0.0000 12800946
Elapsed time = 545.30 sec. (251434.93 ticks, tree = 13.54 MB, solutions = 0)
  73016  4916        0.0000  1487                     -0.0000 13037540
  74506  5023    infeasible                           -0.0000 13269173
  76094  5090    infeasible                           -0.0000 13528840
  77625  5202        0.0000  1735                     -0.0000 13792072
  78726  5106    infeasible                           -0.0000 14003840
  79889  5084    infeasible                           -0.0000 14231445
  81320  5038    infeasible                           -0.0000 14505353
  82040  4900    infeasible                           -0.0000 14661949
  83548  4972        0.0000  1589                     -0.0000 14955703
  84626  4843    infeasible                           -0.0000 15167841
Elapsed time = 632.33 sec. (290030.55 ticks, tree = 14.75 MB, solutions = 0)
  86294  5088    infeasible                           -0.0000 15387594
  87804  5225        0.0000  1359                     -0.0000 15564328
  88886  5244    infeasible                           -0.0000 15699728
  90552  5271    infeasible                           -0.0000 15948314
  91964  5264    infeasible                           -0.0000 16180305
  93433  5389    infeasible                           -0.0000 16427669
  94565  5307        0.0000  1120                     -0.0000 16621300
  95994  5212        0.0000  1455                     -0.0000 16873270
  97427  5247    infeasible                           -0.0000 17129972
  98889  5287        0.0000   983                     -0.0000 17406516
Elapsed time = 719.33 sec. (328416.41 ticks, tree = 27.38 MB, solutions = 0)
  99907  5228        0.0000  1328                     -0.0000 17575397
 101302  5330    infeasible                           -0.0000 17823322
 102799  5214        0.0000   863                     -0.0000 18099640
 103764  5170        0.0000  1129                     -0.0000 18285881
 105271  5249        0.0000  1271                     -0.0000 18554404
 106449  5160        0.0000  1543                     -0.0000 18755055
 107926  5113        0.0000  1762                     -0.0000 19016073
 108946  5142    infeasible                           -0.0000 19221112
 110335  5099        0.0000   777                     -0.0000 19481823
 111545  4980        0.0000  1704                     -0.0000 19710912
Elapsed time = 805.23 sec. (366844.78 ticks, tree = 23.88 MB, solutions = 0)
 112585  4819        0.0000  1424                     -0.0000 19941208
 113784  4892        0.0000  1509                     -0.0000 20193029
 114777  4798    infeasible                           -0.0000 20389392
 116492  4784    infeasible                           -0.0000 20686235
 117583  4572    infeasible                           -0.0000 20908289
 118640  4660        0.0000   970                     -0.0000 21116568
 119860  4641    infeasible                           -0.0000 21355030
 121382  4590        0.0000  1454                     -0.0000 21627839
 122351  4608        0.0000  1265                     -0.0000 21797169
 123588  4526        0.0000  1700                     -0.0000 22052286
Elapsed time = 893.16 sec. (405404.89 ticks, tree = 19.45 MB, solutions = 0)
 124597  4542        0.0000  1581                     -0.0000 22246731
 125830  4603        0.0000  1411                     -0.0000 22485436
 127235  4523        0.0000  1640                     -0.0000 22742415
 128168  4478        0.0000  1636                     -0.0000 22911720
 129565  4484        0.0000  1000                     -0.0000 23181009
 130743  4487        0.0000  1599                     -0.0000 23351196
 132108  4479        0.0000  1378                     -0.0000 23550263
 133548  4330    infeasible                           -0.0000 23826937
 134461  4260        0.0000  1144                     -0.0000 24037776
 135337  4300        0.0000  1185                     -0.0000 24239681
Elapsed time = 980.72 sec. (444203.37 ticks, tree = 20.49 MB, solutions = 0)
 136369  4298        0.0000  1345                     -0.0000 24438674
 137776  4279    infeasible                           -0.0000 24669845
 138913  4133        0.0000  1142                     -0.0000 24923243
 139683  4024        0.0000  1013                     -0.0000 25089334
 140779  4056        0.0000  1273                     -0.0000 25275702
 142463  4028        0.0000  1275                     -0.0000 25559396
 143596  4029        0.0000  1421                     -0.0000 25801485
 144449  4108        0.0000  1474                     -0.0000 25999187
 145595  4199        0.0000  1814                     -0.0000 26236291
 146576  4192    infeasible                           -0.0000 26430551
Elapsed time = 1068.33 sec. (482851.65 ticks, tree = 23.50 MB, solutions = 0)
 147814  4325        0.0000  1747                     -0.0000 26660597
 149075  4345        0.0000  1244                     -0.0000 26937802
 150223  4396    infeasible                           -0.0000 27146886
 151396  4372        0.0000  1272                     -0.0000 27326098
 152752  4293        0.0000  1545                     -0.0000 27564920
 153548  4127        0.0000  1268                     -0.0000 27771342
 154765  4064        0.0000  1057                     -0.0000 27981568
 155488  3955    infeasible                           -0.0000 28150713
 156418  3765    infeasible                           -0.0000 28383049
 157341  3595        0.0000  1666                     -0.0000 28576333
Elapsed time = 1152.84 sec. (521275.28 ticks, tree = 22.79 MB, solutions = 0)
 158467  3589        0.0000  1136                     -0.0000 28815572
 159532  3561        0.0000  1803                     -0.0000 29040318
 160465  3611        0.0000  1598                     -0.0000 29279594
 161411  3625    infeasible                           -0.0000 29511805
 162031  3578        0.0000   832                     -0.0000 29642435
 163258  3549        0.0000   919                     -0.0000 29941674
 163927  3560        0.0000  1921                     -0.0000 30088371
 165262  3556        0.0000  1464                     -0.0000 30381954
 166573  3540    infeasible                           -0.0000 30624650
 167811  3509        0.0000  1489                     -0.0000 30890814
Elapsed time = 1243.14 sec. (559789.31 ticks, tree = 16.68 MB, solutions = 0)
 168651  3427    infeasible                           -0.0000 31073463
 170018  3445    infeasible                           -0.0000 31286141
 170741  3286        0.0000  1484                     -0.0000 31424810
 172175  3297    infeasible                           -0.0000 31707599
 172965  3208        0.0000  1736                     -0.0000 31868977
 174150  3090    infeasible                           -0.0000 32138345
 175160  3044        0.0000  1107                     -0.0000 32355657
 175994  2990        0.0000  1593                     -0.0000 32555554
 177147  2771    infeasible                           -0.0000 32778058
 178088  2697        0.0000  1883                     -0.0000 32977587
Elapsed time = 1330.00 sec. (598388.63 ticks, tree = 5.88 MB, solutions = 0)
 178865  2623        0.0000  1670                     -0.0000 33186397
 179659  2568    infeasible                           -0.0000 33347250
 180686  2520    infeasible                           -0.0000 33607419
 181816  2384        0.0000  1800                     -0.0000 33867732
 182642  2300    infeasible                           -0.0000 34051617
 183672  2248        0.0000  1716                     -0.0000 34251822
 184628  2049        0.0000  1881                     -0.0000 34486471
 185359  1843        0.0000   917                     -0.0000 34650208
 186210  1758        0.0000  1685                     -0.0000 34883935
 186808  1625    infeasible                           -0.0000 35060248
Elapsed time = 1418.44 sec. (637045.35 ticks, tree = 2.74 MB, solutions = 0)
 187666  1390        0.0000  1656                     -0.0000 35284509
 188282  1348        0.0000  1607                     -0.0000 35454477
 188974  1294    infeasible                           -0.0000 35658533
 189819  1284        0.0000  1344                     -0.0000 35878470
 190530  1111        0.0000  1847                     -0.0000 36069288
 191306  1126        0.0000  1961                     -0.0000 36238662
 192172  1193    infeasible                           -0.0000 36457694
 192817  1169        0.0000  1389                     -0.0000 36644583
 193478  1202        0.0000   408                     -0.0000 36869749
 194158  1161        0.0000  1825                     -0.0000 37060379
Elapsed time = 1506.59 sec. (676153.52 ticks, tree = 2.70 MB, solutions = 0)
 194823  1047    infeasible                           -0.0000 37314861
 195274   902        0.0000  2100                     -0.0000 37464452
 195909   731        0.0000  1760                     -0.0000 37659892
 196478   737    infeasible                           -0.0000 37804184
 197079   644    infeasible                           -0.0000 38034960
 197760   600        0.0000  1947                     -0.0000 38279954
 198275   538        0.0000  2168                     -0.0000 38437348
 198876   476    infeasible                           -0.0000 38643813
 199376   406    infeasible                           -0.0000 38820484
 200186   333        0.0000  2000                     -0.0000 38993643
Elapsed time = 1593.83 sec. (714834.63 ticks, tree = 0.36 MB, solutions = 0)
 200819   171    infeasible                           -0.0000 39193590
 201410    67    infeasible                           -0.0000 39359622
 201695     1    infeasible                           -0.0000 39435653

Root node processing (before b&c):
  Real time             =    9.05 sec. (6330.63 ticks)
Parallel b&c, 12 threads:
  Real time             = 1610.13 sec. (720154.57 ticks)
  Sync time (average)   =  172.85 sec.
  Wait time (average)   =    0.07 sec.
                          ------------
Total (root+branch&cut) = 1619.17 sec. (726485.20 ticks)
Stone 1 lighter: ILOG.CPLEX.CpxException: CPLEX Error  1217: No solution exists.

   at ILOG.CPLEX.CplexI.CALL(Int32 status)
   at ILOG.CPLEX.CplexI.GetXcache()
   at ILOG.CPLEX.Cplex.GetValue(INumExpr expr)
   at CplexMilpManager.Implementation.CplexMilpSolver.GetValue(IVariable variable) in C:\Users\afish\Desktop\milpmanager\CplexMilpSolver\Implementation\CplexMilpSolver.cs:line 160
   at IlpPlayground.Program420502851.<>c__DisplayClass18.<Start>b__8(Int32 stoneId)
   at System.Linq.Enumerable.WhereSelectEnumerableIterator`2.MoveNext()
   at System.Linq.Enumerable.WhereSelectEnumerableIterator`2.MoveNext()
   at System.String.Join[T](String separator, IEnumerable`1 values)
   at IlpPlayground.Program420502851.Start()
   at IlpPlayground.Env420502851.Start()

CPLEX indicates there are no solutions. This makes sense, we can't tell the solution for sure with 2 weightings only. Here comes the solution for 12 stones and 3 moves:

Stone 1 lighter: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [<] ; (5 ; 6) [=] ;
Stone 1 heavier: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [>] ; (1 ; 2) [<] ;
Stone 2 lighter: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [=] ; (11 ; 2) [<] ;
Stone 2 heavier: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [>] ; (1 ; 2) [>] ;
Stone 3 lighter: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [>] ; (3 ; 4) [>] ;
Stone 3 heavier: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [=] ; (11 ; 3) [>] ;
Stone 4 lighter: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [>] ; (3 ; 4) [<] ;
Stone 4 heavier: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [<] ; (7 ; 8) [=] ;
Stone 5 lighter: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [>] ; (1 ; 2) [=] ;
Stone 5 heavier: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [<] ; (5 ; 6) [<] ;
Stone 6 lighter: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [=] ; (11 ; 3) [=] ;
Stone 6 heavier: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [<] ; (5 ; 6) [>] ;
Stone 7 lighter: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [<] ; (7 ; 8) [>] ;
Stone 7 heavier: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [=] ; (11 ; 2) [=] ;
Stone 8 lighter: (1,2,3,4 ; 5,6,7,8) [<] ; (4,5,9,10 ; 1,2,7,8) [<] ; (7 ; 8) [<] ;
Stone 8 heavier: (1,2,3,4 ; 5,6,7,8) [>] ; (3,4,5,6 ; 1,8,9,10) [>] ; (3 ; 4) [=] ;
Stone 9 lighter: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [<] ; (9 ; 10) [>] ;
Stone 9 heavier: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [>] ; (9 ; 10) [<] ;
Stone 10 lighter: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [<] ; (9 ; 10) [<] ;
Stone 10 heavier: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [>] ; (9 ; 10) [>] ;
Stone 11 lighter: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [<] ; (9 ; 10) [=] ;
Stone 11 heavier: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [>] ; (9 ; 10) [=] ;
Stone 12 lighter: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [=] ; (1 ; 12) [<] ;
Stone 12 heavier: (1,2,3,4 ; 5,6,7,8) [=] ; (1,2,3 ; 9,10,11) [=] ; (1 ; 12) [>] ;

Big thanks to Tomasz Masternak. We had lots of fun discussing the problem.

This is the first part of the Distributed Designs series. For your convenience you can find other parts using the links below:
Part 1 — Outbox without idempotency nor synchronous commit
Part 2 — Transactional outbox pattern and multiple instances of relay
Part 3 — Taking lock in MVCC for transactional outbox pattern

Transactional outbox is a common pattern in the distributed systems. It helps to avoid having either orphaned records (for which messages were not published) or messages pointing to non-existing records (for which database entities do not exist). However, the pattern assumes, that the consumer is idempotent, so the consumer can handle duplicates easily by retrying the logic. Even the linked page says that:

The Message Relay might publish a message more than once. It might, for example, crash after publishing a message but before recording the fact that it has done so. When it restarts, it will then publish the message again. As a result, a message consumer must be idempotent, perhaps by tracking the IDs of the messages that it has already processed. Fortunately, since Message Consumers usually need to be idempotent (because a message broker can deliver messages more than once) this is typically not a problem.

What can we do in case when the message consumer doesn’t support idempotency? One idea is to detect duplicates somehow, and only handle given message once. However, how can we do that in case when we lack a synchronous commit in the data storage? I recently stumbled upon such a problem and this is the solution I used.

Problem statement

Let’s say that we have n clusters of our application. We can communicate between them, but all the changes we perform are not synchronously committed but only eventually consistent. All clusters are active, they can accept incoming transactions, they can modify the state. We have some database, we have some queue, we have some synchronization mechanisms between the clusters, but we can’t build any lock nor run transaction across all of the clusters. To sum up, these are our requirements:

• We have n clusters. Each cluster runs a database, a queue, a message relay, and a message consumer
• Database is replicated across clusters, but we lack a synchronous commit. We do have an eventual consistency
• We now we have some bounded timeout for synchronization, but we don’t know what it is. We can safely assume it’s belowe some reasonable value like 10 minutes
• Message consumer is not idempotent

If we implement transactional outbox the regular way, then we’ll end up with n messages published to the queue. Since our message consumer is not idempotent, it will modify the state n times. However, we can’t easily track duplicates, as we lack a synchronous commit in the database across all clusters, so we can’t easily check if the message was already processed.

Solution

We introduce the following environment variables:

• CLUSTERS_COUNT – that indicates how many clusters are running
• CLUSTER_ID – identifier of the cluster a given component is in
• MAXIMUM_DELAY – some reasonable timeout for replication, like 10 minutes

Now, the trick is. We extend our outbox table with additional column indicating which cluster was the true source of the message. So we add additional integer column which we fill with the value of CLUSTER_ID variable. Next, we modify our message relay to extract messages in the following way:

SELECT *
FROM outbox
WHERE cluster_id = $CLUSTER_ID OR creation_time < NOW - $MAXIMUM_DELAY

This reads as: message relay gets all the messages coming from the same cluster, or all messages that are old enough. The former is the “happy path” – the message was created by the application code, shortly after the relay picks it up and puts to the queue, and also removes it from the outbox table (or marks as processed). The latter is the “unhappy path” – if the originating cluster crashed for whatever reason after putting the message to the outbox, then the message will be delayed by MAXIMUM_DELAY and then picked up by some other message relay from some other cluster. This shouldn’t happen often, but when it happens, then it’s an indicator of some “catastrophic outage”.

However, in the “happy path” we won’t get any duplicate posted to the queue. Obviously, we may still face the regular crashes or connection rests, as in the transactional outbox, but they are not because of the lack of synchronous commit.

You may also notice that when the catastrophic outage happens, then the message will be duplicated n-1 times. We may come up with some more sophisticated query to extract messages, to effectively introduce ordering between the clusters.