Coding – Random IT Utensils https://blog.adamfurmanek.pl IT, operating systems, maths, and more. Fri, 22 Mar 2024 20:15:55 +0000 en-US hourly 1 https://wordpress.org/?v=6.5.2 Availability Anywhere Part 25 — Supercharge your VR experience https://blog.adamfurmanek.pl/2024/03/22/availability-anywhere-part-25/ https://blog.adamfurmanek.pl/2024/03/22/availability-anywhere-part-25/#respond Fri, 22 Mar 2024 20:15:30 +0000 https://blog.adamfurmanek.pl/?p=4988 Continue reading Availability Anywhere Part 25 — Supercharge your VR experience]]>

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.

]]>
https://blog.adamfurmanek.pl/2024/03/22/availability-anywhere-part-25/feed/ 0
Availability Anywhere Part 24 — Make RDP retain position of windows and stop moving them around https://blog.adamfurmanek.pl/2024/03/09/availability-anywhere-part-24/ https://blog.adamfurmanek.pl/2024/03/09/availability-anywhere-part-24/#respond Sat, 09 Mar 2024 08:53:42 +0000 https://blog.adamfurmanek.pl/?p=4969 Continue reading Availability Anywhere Part 24 — Make RDP retain position of windows and stop moving them around]]>

This is the twentieth fourth 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 solve a problem of RDP session moving your windows around when you connect from multiple machines. Let’s see how it works.

Problem statement

First, a couple of assumptions what I’m trying to solve:

  • I’m using mstsc.exe to connect to the RDP server. mstsc.exe is the regular Windows RDP client (so called the “blue” client). I’m using the regular application, not the UWP one
  • I have two machines that I use to connect to the RDP server. These machines are Client1 and Client2. Both Clients have three screens attached. While I’m using physical screens, you’re free to use IddSampleDriver or vSpatial virtual screens. I think the same should apply to other solutions like spacedesk and similar. The same should apply to screens created by BetterDisplay (when you RDP from Mac to your Client1).
  • Screen1 is “at front”, Screen2 is “on the right”, Screen3 is “on the left”. The actual ordering doesn’t matter but I’ll refer to this later in this post
  • I use Client1 to connect to the RDP server and I open maximized Browser on Screen1 and maximized Notepad on Screen2. I then disconnect and connect to the RDP server from Client2. At this point, I want Browser to still be on Screen1 (“at front”) and Notepad on Screen2 (“on the right”).
  • Screen1 is my “main display” and it has the taskbar. I want the same in the RDP server (so taskbar should be on Screen1)

I’m going to use screenshots to explain my setup. They are a little trickier to let’s walk one by one.

My setup

First, my Client1 has five physical screens in total. However, I use Screen4 to duplicate my Screen1, and I use Screen5 to keep things outside of RDP. Therefore, I only want to use Screen1, Screen2, and Screen3 in the RDP session (and obviously Screen4 which is implicitly showing Screen1). I also have 5 additional virtual screens created with IddSampleDriver and 2 more virtual screens created with vSpatial. I don’t use these virtual screens (they are turned off).

This is what “Display” shows me which from now on I’ll call “Display Setup”:

So this is the mapping:

  • Screen1 (“at front”) is Display Setup Screen 1
  • Screen2 (“on the right”) is Display Setup Screen 12
  • Screen3 (“on the left”) is Display Setup Screen 11
  • Screen4 (duplicating Screen1) is Display Setup Screen 9
  • Screen5 (kept outside of RDP) is Display Setup Screen 10
  • Display Setup Screen 2-6 are IddSampleDriver virtual screens
  • Display Setup Screen 7-8 are vSpatial virtual screens

Now I want to use screens Screen1 + Screen2 + Screen3 in RDP session only. Scott Hanselman explains how to do it. We first need to list the screens with mstsc /l and this is what I get (which from now I’ll call “MSTSC Setup”):

So here comes the mapping:

  • Screen1 (“at front”) is MSTSC Setup Screen 44
  • Screen2 (“on the right”) is MSTSC Setup Screen 46
  • Screen3 (“on the left”) is MSTSC Setup Screen 47
  • Screen4 (duplicating Screen1) is MSTSC Setup Screen 44 (the same as Screen1)
  • Screen5 (kept outside of RDP) is MSTSC Setup Screen 45

It’s important to notice that numbers do not match between Display Setup and MSTSC Setup. This is very important and makes the whole trouble. Let’s now solve the problems.

Using only a subset of displays in the RDP session

This is actually easy. When you see Scott Hanselman’s blog, it mentions the parameter called selectedmonitors. You use it to specify the comma-separated-list of monitors that you want to use for the RDP session.

In my case, I need to use MSTSC Setup Screen 44, MSTSC Setup Screen 46, and MSTSC Setup Screen 47. So the parameter in my case is:

selectedmonitors:s:44,46,47

After connecting to RDP, this is what “Display” shows (which I’ll refer to as Display RDP Setup):

In textual form each line is screenId: width x height; (xBegin, yBegin, xEnd, yEnd):

44: 1920 x 1080; (0, 0, 1919, 1079)
45: 1080 x 1920; (363, 1080, 1442, 2999)
46: 2560 x 1440; (1920, 0, 4479, 1439)
47: 2560 x 1440; (-2560, 0, -1, 1439)

So, here is the mapping:

  • Screen1 (“at front”) is Display RDP Setup Screen 1
  • Screen2 (“on the right”) is Display RDP Setup Screen 2
  • Screen3 (“on the left”) is Display RDP Setup Screen 3

You can see that there are only 3 screens in the RDP session. Exactly as I wanted.

Controlling the main display in RDP

selectedmonitors parameter controls this. The main display is the first monitor from this list. So, if you have selectedmonitors:s:x,y,z, then the screen x is going to be the main display in RDP. This doesn’t need to match your main display on the host. In my case, my parameter is set to selectedmonitors:s:44,46,47, so the main display in RDP is going to be MSTSC Setup Screen 44.

Making RDP not move windows

This is the trickiest part. Remember that I open maximized Browser on Screen1 and maximized Notepad on Screen2. Based on our mappings above, the Browser is on Screen1 = Display Setup Screen 1 = Display RDP Setup Screen 1 = MSTSC Setup Screen 44. Similarly, Notepad is on Screen2 = Display Setup Screen 12 = Display RDP Setup Screen 2 = MSTSC Setup Screen 46.

Now, these are the things that I believe are correct. I found them empirically and they work for me across 4 different laptops, but your mileage my vary.

  • The order of screens in selectedmonitors parameter doesn’t matter (apart from choosing the “main display” explained in the previous section)
  • The numbers from Display Setup do not matter! The numbers from MSTSC Setup do not matter! The only thing that matters is the order of screens from MSTSC Setup
  • The resolutions of the screens do not matter! Windows remembers maximized windows positions not based on the geometry (like “the window’s top left corner is in pixel 0,0) but rather as “the window is maximized on Display RDP Setup Screen 1
  • You can’t control numbers from MSTSC Setup programmatically. You can only control them by physically moving your screens to different ports/connectors/docking stations/USB adapters, etc.
  • To get the windows not move, you need to have screen “passed to RDP” in the same order between Client1 and Client2 (between different clients)

That’s it. It may be a little bit cryptic, so let’s delve into how I think it works.

mstsc.exe uses some API to enumerate displays and then applies logic to merge windows or reorder them. Notice, that in my case Display Setup shows 12 screens while MSTSC Setup shows only 4. That’s because 7 virtual screens are turned off, and Screen4 duplicates Screen1.

Now, it seems that mstsc.exe enumerates the screens, and then for each screen checks if it was selected in selectedmonitors. If yes, then it registers the screen in the RDP session. So the code looks conceptually like:

foreach(screen in enumerateScreens()):
    if(screen.id in selectedmonitors) then
        registerScreenInRdpSession(screen)
    end
end

This explains why the order of screens in selectedmonitors doesn’t matter. Assuming that, this is what we need to get:

  • We want the Browser to still be presented on the Screen1 (“at front”). This screen was registered first in the loop above when connecting from Client1. Therefore, when Client2 enumerates the screens in mstsc.exe, Screen1 must be the first one that matches the if condition. In other words, Screen1 can be in whatever position according to MSTSC Setup and can have any number, but there must be no other selectedmonitors screen earlier in the list of mstsc.exe /l
  • We don’t care about resolutions. Screen1 on Client1 can have different resolution than Screen1 on Client2. The Browser will still be “maximized on the Display RDP Setup Screen 1
  • We want the Notepad to still be presented on the Screen2 (“on the right”). Same logic applies: mstsc.exe continues enumerating the screens and the second screen that gets picked must be the screen on the right

Now, how do we control the order of screens enumerated by mstsc.exe /l? The short answer is: we can’t do that programmatically. We need to physically change cables! What’s worse, this order breaks when you change settings like Duplicate screen or Extend desktop to this screen.

How to change cables physically? There are solutions:

  • Just plug cable to some other slot in your laptop/PC
  • Use docking station and change the order of cables (or move some monitors to your laptop and some through your docking station)
  • Use another docking station! Yes, you can have many of them (I actually have 2, that’s a long story)
  • Use USB adapters like i-tec USB Type C to DisplayPort Adapter, 4K Video, Supports 2 External Displays. I have two of them and they are great. Your mileage may vary, obviously
  • Try hacking mstsc.exe with things like API Monitor (I haven’t tried that but that seems plausible)

I tested this setup across four different laptops – one with physical screens, two with virtual screens by IddSampleDriver, one with virtual screens by vSpatial. In my case, windows are not moved anymore. I can literally switch from one computer to another with different screen resolutions but all the windows stay where they were. And yes, I had to switch my cables like crazy. In my case it was even worse, because Screen1 was attached directly (and so was enumerated first by Display Setup) but Screen4 was attached by an adapter (and was taking precedence in mstsc.exe /l). It works, though.

]]>
https://blog.adamfurmanek.pl/2024/03/09/availability-anywhere-part-24/feed/ 0
Availability Anywhere Part 23 — RDP over VR goggles with no PCVR https://blog.adamfurmanek.pl/2024/02/21/availability-anywhere-part-23/ https://blog.adamfurmanek.pl/2024/02/21/availability-anywhere-part-23/#respond Wed, 21 Feb 2024 21:10:54 +0000 https://blog.adamfurmanek.pl/?p=4961 Continue reading Availability Anywhere Part 23 — RDP over VR goggles with no PCVR]]>

This is the twentieth third 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

In this part we’re going to see how we can work remotely from VR goggles with no PCVR around. Effectively, we can work remotely with goggles and a bluetooth keyboard, nothing else.

My workstation

My home workstation is quite powerful. I have 5 physical screens which I use to display 4 different screens. I also use VirtuaWin to have many desktops. I also work remotely from a dedicated machine to which I connect using MS RDP (mstsc.exe).

My typical setup works like this:

  • My main physical screen is 24” with FullHD resolution. I duplicate this physical screen to another physical screen which is 10” and has touch capabilities. I use the touch to draw diagrams.
  • My two additional side screens are 32” with 4K resolution
  • My fifth screen is 10” big and I use it to display all the instant messengers I need (slacks, discords, meets etc). That’s basically a browser window that I configure to be visible on all of the desktops.
  • I have 11 desktops configured in VirtuaWin.
  • To connect remotely to my machine, I move to some other VirtuaWin desktop and use four physical screens (FullHD + 2x4K + touch-enabled screen) to open mstsc.exe.
  • When I need to connect to some other machine, I basically do CTRL+ALT+HOME to unfocus the current RDP, then I switch to another VirtuaWin desktop, and there I connect to the server. This way I can quickly switch between multiple machines I have

This setup works great for me. I can work remotely from any place around the planet. When I’m not at home, I can use my road runner laptop with two physical screens or my mobile phone to connect over RDP to the remote server. I do various things over RDP – I code, I write/read documents, I postprocess videos, I record videos (yes, I record them over RDP!), I browse the Internet. Typical office work.

I wanted to replicate this setup as much as possible with VR goggles. I managed to do that with Meta Quest 3 and vSpatial. Let’s see how I did that.

What we need

First, you need the goggles. I used Meta Quest 3 and they were quite good. I can’t complain on the image quality and I definitely can do all the stuff I need. The battery lasts for around 90-120 minutes which is okayish.

Next, you need to have a machine with many physical displays. That’s the most tricky part if you want to configure it entirely over RDP and use free version of vSpatial. I use two dedicated machines: one is Windows Server and the other is Mac. I first connect to Windows Server from my mobile phone over the regular RDP and log in as User1. At this point, I have a session in Windows Server that has just one display. Next, I use NoMachine to connect from Windows Server to my Mac. In my Mac, I create multiple physical screens using Better Display. Next, I connect from my Mac to my Windows Server and log in as User2 using the regular RDP application. At this point, I have a session in Windows Server that has multiple physical screens. All of that done entirely from my mobile phone, so I can do that when I’m travelling. While it works and allows for any setup of monitors, it’s probably good enough to just use 4 screens from paid vSpatial. Up to you.

Next, we need the vSpatial server. I install it in Windows Server for User2. I then log in to Windows Server using vSpatial application in Meta Quest 3 goggles. The vSpatial client correctly recognizes all 4 displays and now I have access to a regular Windows machine. I can install VirtuaWin and configure desktops the regular way. It all works just like on the screenshot below:

You can see one screen at the top and three screens in the middle. This is nearly the same setup as I have at home.

Finally, I just pair my bluetooth keyboard with touchpad and that’s it. CTRL+ALT+HOME works, so I can work the same way as at home.

Now, sky is the limit. Since I managed to RDP into a regular Windows machine, I can RDP anywhere I need, I can install any application I need, and I can do all of that using my goggles and the bluetooth keyboard only. I want to stress that there is no PCVR here. The Windows Machine with vSpatial server is completely virtualized and has no dedicated graphics card. Also, I don’t use powerful Internet connection. I just connect over regular WiFi. This works from mobile hotspot as well as it’s just RDP.

When it comes to online meetings, I can take them from my mobile phone. If I want to share the screen, I can just join the same meeting from my mobile phone and from my remote machine, and I can share the screen from Windows Server. However, you can also start browser on VR and join meeting like in Google Meet. The meeting will work even after you switch to vSpatial.

Quirks

There are quirks, obviously.

First, Meta Quest 3 seems to be based on Android. Bluetooth keyboards don’t work 100% properly with Android when you RDP to Windows. One issue is that the WIN key doesn’t work. Another, some shortcuts (like ALT+TAB) are captured by the host (goggles in this case).

To solve the lack of WIN key, I use PowerToys. I just remap CAPS LOCK to LEFT WIN on my Windows Server. You can also use AutoHotkey with the following script:

*CapsLock::
    Send {Blind}{LWin Down}
Return

*CapsLock up::
    Send {Blind}{LWin Up}
Return

The script rebinds CAPS LOCK to LEFT WIN. No matter which method you use, you can just use CAPS LOCK in all the shortcuts (like maximizing the window with LEFT WIN+ARROW UP which becomes CAPS LOCK+ARROW UP). While it’s a bit painful, it works. You need to install AutoHotkey in all the remote machines you connect to.

I didn’t solve the ALT+TAB issue with AutoHotkey. I solved it with PowerToys by remapping SCROLL LOCK to TAB. I think you could use AutoHotkey to remap it as well.

Second, vSpatial has a concept of active (focused) desktop. If you worked on one screen and want to click on another one, the mouse click changes the focus. You need to click again to do the actual click you want. This is not a big deal and I got used to it very fast.

Third, I think vSpatial is slightly slower than the regular RDP. I don’t find this as a problem, though, as it’s fast enough for me.

Fourth, the goggles don’t last for long (up to two hours). On the other hand, maybe it’s better for your eyes. You can also buy an additional strap with built-it powerbank.

Summary

It took me quite a while to figure out how to configure this setup. However, now I can truly work using goggles and no laptop around. That sounds like a great approach when traveling – imagine sitting at the airport and having multiple screens, just like at home. Now, the only issue is around the goggles. I hope one day they will be smaller, lighter, and will have stronger batteries. You can always plug them into powerbank if needed, though.

]]>
https://blog.adamfurmanek.pl/2024/02/21/availability-anywhere-part-23/feed/ 0
Availability Anywhere Part 22 — Customer Experience Improvement Program restarts https://blog.adamfurmanek.pl/2024/02/11/availability-anywhere-part-22/ https://blog.adamfurmanek.pl/2024/02/11/availability-anywhere-part-22/#respond Sun, 11 Feb 2024 10:10:10 +0000 https://blog.adamfurmanek.pl/?p=4943 Continue reading Availability Anywhere Part 22 — Customer Experience Improvement Program restarts]]>

This is the twentieth second 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

I was recently investigating a case of a computer restarting every Sunday at 3AM UTC. I couldn’t figure out what was going on and I suspected Customer Experience Improvement Program as I found the following event in event viewer:

User Logoff Notification for Customer Experience Improvement Program

- <Event xmlns="http://schemas.microsoft.com/win/2004/08/events/event">
- <System>
		<Provider Name="User32" Guid="{b0aa8734-56f7-41cc-b2f4-de228e98b946}" EventSourceName="User32" /> 
		<EventID Qualifiers="32768">1074</EventID> 
		<Version>0</Version> 
		<Level>4</Level> 
		<Task>0</Task> 
		<Opcode>0</Opcode> 
		<Keywords>0x8080000000000000</Keywords> 
		<TimeCreated SystemTime="2024-02-04T03:00:01.2906001Z" /> 
		<EventRecordID>404828</EventRecordID> 
		<Correlation /> 
		<Execution ProcessID="896" ThreadID="804" /> 
		<Channel>System</Channel> 
		<Computer>computerName</Computer> 
		<Security UserID="S-1-5-18" /> 
	</System>
- <EventData>
		<Data Name="param1">C:\Windows\system32\shutdown.EXE (computerName)</Data> 
		<Data Name="param2">computerName</Data> 
		<Data Name="param3">No title for this reason could be found</Data> 
		<Data Name="param4">0x800000ff</Data> 
		<Data Name="param5">restart</Data> 
		<Data Name="param6">System is scheduled to reboot in 10 minutes. Please save your work.</Data> 
		<Data Name="param7">NT AUTHORITY\SYSTEM</Data> 
	</EventData>
</Event>

I checked many solutions on the Internet and none of them helped. However, later I realized it was not due to Customer Experience Improvement Program. After carefully checking the event viewer, I found the following:

The process C:\Windows\system32\shutdown.EXE (computerName) has initiated the restart of computer computerName on behalf of user NT AUTHORITY\SYSTEM for the following reason: No title for this reason could be found
Reason Code: 0x800000ff
Shutdown Type: restart
Comment: System is scheduled to reboot in 10 minutes. Please save your work.

- <Event xmlns="http://schemas.microsoft.com/win/2004/08/events/event">
- <System>
		<Provider Name="Microsoft-Windows-Winlogon" Guid="{dbe9b383-7cf3-4331-91cc-a3cb16a3b538}" /> 
		<EventID>7002</EventID> 
		<Version>0</Version> 
		<Level>4</Level> 
		<Task>1102</Task> 
		<Opcode>0</Opcode> 
		<Keywords>0x2000200000000000</Keywords> 
		<TimeCreated SystemTime="2024-02-04T03:10:41.0539456Z" /> 
		<EventRecordID>404868</EventRecordID> 
		<Correlation /> 
		<Execution ProcessID="6028" ThreadID="6892" /> 
		<Channel>System</Channel> 
		<Computer>computerName</Computer> 
		<Security UserID="S-1-5-18" /> 
	</System>
- <EventData>
		<Data Name="TSId">2</Data> 
		<Data Name="UserSid">S-1-5-21-1801674531-515967899-839522115-19733726</Data> 
	</EventData>
</Event>

So it seems that something triggered the restart. I wasn’t sure what that was and I just solved it by cancelling the restart. Just run this batch script to cancel any shutdowns every 30 seconds:

:start
shutdown /a
timeout 30
goto start

It worked good enough.

]]>
https://blog.adamfurmanek.pl/2024/02/11/availability-anywhere-part-22/feed/ 0
ILP Part 106 — Golden waste https://blog.adamfurmanek.pl/2023/12/16/ilp-part-106/ https://blog.adamfurmanek.pl/2023/12/16/ilp-part-106/#respond Sat, 16 Dec 2023 07:51:05 +0000 https://blog.adamfurmanek.pl/?p=4927 Continue reading ILP Part 106 — Golden waste]]>

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

]]>
https://blog.adamfurmanek.pl/2023/12/16/ilp-part-106/feed/ 0
ILP Part 105 — Sudoku Cube https://blog.adamfurmanek.pl/2023/02/10/ilp-part-105/ https://blog.adamfurmanek.pl/2023/02/10/ilp-part-105/#respond Fri, 10 Feb 2023 09:00:18 +0000 https://blog.adamfurmanek.pl/?p=4872 Continue reading ILP Part 105 — Sudoku Cube]]>

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.

]]>
https://blog.adamfurmanek.pl/2023/02/10/ilp-part-105/feed/ 0
Distributed Designs Part 3 — Taking lock in MVCC for transactional outbox pattern https://blog.adamfurmanek.pl/2023/02/03/distributed-designs-part-3/ https://blog.adamfurmanek.pl/2023/02/03/distributed-designs-part-3/#respond Fri, 03 Feb 2023 09:00:30 +0000 https://blog.adamfurmanek.pl/?p=4858 Continue reading Distributed Designs Part 3 — Taking lock in MVCC for transactional outbox pattern]]>

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.

]]>
https://blog.adamfurmanek.pl/2023/02/03/distributed-designs-part-3/feed/ 0
Distributed Designs Part 2 — Transactional outbox pattern and multiple instances of relay https://blog.adamfurmanek.pl/2023/01/27/distributed-designs-part-2/ https://blog.adamfurmanek.pl/2023/01/27/distributed-designs-part-2/#respond Fri, 27 Jan 2023 09:00:26 +0000 https://blog.adamfurmanek.pl/?p=4853 Continue reading Distributed Designs Part 2 — Transactional outbox pattern and multiple instances of relay]]>

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.

]]>
https://blog.adamfurmanek.pl/2023/01/27/distributed-designs-part-2/feed/ 0
.NET Inside Out Part 30 – Conditional types in C# https://blog.adamfurmanek.pl/2023/01/20/net-inside-out-part-30-conditional-types-in-c/ https://blog.adamfurmanek.pl/2023/01/20/net-inside-out-part-30-conditional-types-in-c/#respond Fri, 20 Jan 2023 09:00:35 +0000 https://blog.adamfurmanek.pl/?p=4829 Continue reading .NET Inside Out Part 30 – Conditional types in C#]]>

This is the thirtieth part of the .NET Inside Out series. For your convenience you can find other parts in the table of contents in Part 1 – Virtual and non-virtual calls in C#

TypeScript has a very nice feature called conditional types. Can we mimic something like this in C#? Let’s say that we have one API endpoint that should return different output depending on the type of the input.

We can start with the following code:

using System;
					
public class Program
{
	public static void Main()
	{
		Console.WriteLine(GetForInput(new ScenarioAInput()).GetType());
		Console.WriteLine(GetForInput(new ScenarioBInput()).GetType());
	}
	
	public static Output<T> GetForInput<T>(Input<T> input) where T: Scenario{
		if(typeof(Input<ScenarioA>).IsAssignableFrom(input.GetType())){
			return (Output<T>)(object)GetForInputA((ScenarioAInput)(object)input);
		}
		if(typeof(Input<ScenarioB>).IsAssignableFrom(input.GetType())){
			return (Output<T>)(object)GetForInputB((ScenarioBInput)(object)input);
		}
		
		throw new Exception("Bang!");
	}
	
	public static ScenarioAOutput GetForInputA(ScenarioAInput input){
		return new ScenarioAOutput();
	}
	
	public static ScenarioBOutput GetForInputB(ScenarioBInput input){
		return new ScenarioBOutput();
	}
}

public abstract class Scenario {
}

public class ScenarioA : Scenario{
}

public class ScenarioB: Scenario{
}

public abstract class Input<T> where T: Scenario{
}

public class ScenarioAInput : Input<ScenarioA> {
}

public class ScenarioBInput : Input<ScenarioB> {
}

public abstract class Output<T> where T: Scenario{
}

public class ScenarioAOutput: Output<ScenarioA> {
}

public class ScenarioBOutput: Output<ScenarioB>{
}

This works but is a little bit cumbersome. When we need to add new implementation, we need to add another if condition. Can we do better? Well, a little:

using System;
using System.Linq;
using System.Collections.Generic;
					
public class Program
{
	public static void Main()
	{
		Console.WriteLine(GetForInput(new ScenarioAInput()).GetType());
		Console.WriteLine(GetForInput(new ScenarioBInput()).GetType());
	}
	
	public static Output<T> GetForInput<T>(Input<T> input) where T: Scenario<T> {
		List<Scenario> implementations = new List<Scenario>(){
			new ScenarioA(),
			new ScenarioB()
		};
		
		foreach(var implementation in implementations){
			if(implementation.GetType().GetInterfaces().First().GetGenericArguments().First() == typeof(T)){
				return ((Scenario<T>)implementation).Calculate(input);
			}
		}
		
		throw new Exception("Didn't work");
	}
}

public interface Scenario{
}

public interface Scenario<T> : Scenario where T: Scenario<T> {
	Output<T> Calculate(Input<T> input);
}

public class ScenarioA : Scenario<ScenarioA> {
	public Output<ScenarioA> Calculate(Input<ScenarioA> input){
		return new ScenarioAOutput();
	}
}

public class ScenarioB: Scenario<ScenarioB> {
	public Output<ScenarioB> Calculate(Input<ScenarioB> input){
		return new ScenarioBOutput();
	}
}

public abstract class Input<T> where T: Scenario<T> {
}

public class ScenarioAInput : Input<ScenarioA> {
}

public class ScenarioBInput : Input<ScenarioB> {
}

public abstract class Output<T> where T: Scenario<T> {
}

public class ScenarioAOutput: Output<ScenarioA> {
}

public class ScenarioBOutput: Output<ScenarioB> {
}

Now adding new type requires adding new instance to the collection. However, this time we can scan all the types and crate them on the fly as needed with DI or whatever other mechanism.

]]>
https://blog.adamfurmanek.pl/2023/01/20/net-inside-out-part-30-conditional-types-in-c/feed/ 0
Availability Anywhere Part 19 — Banning RDP and SSH attacks https://blog.adamfurmanek.pl/2023/01/13/availability-anywhere-part-19/ https://blog.adamfurmanek.pl/2023/01/13/availability-anywhere-part-19/#respond Fri, 13 Jan 2023 09:00:05 +0000 https://blog.adamfurmanek.pl/?p=4821 Continue reading Availability Anywhere Part 19 — Banning RDP and SSH attacks]]>

This is the nineteenth 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

If you expose RDP or OpenSSH to the wide Internet, you’ll most likely get automated attacks. There is a way to block these attacks with firewall, but I didn’t find a nice solution to do so, so I created my own.

The idea is as follows: we periodically scan event log to get failed authentication attempts. We extract the IP address, and then ban it if it happened too often.

Event for RDP is in Security with ID 4625:

- <Event xmlns="http://schemas.microsoft.com/win/2004/08/events/event">
- <System>
  <Provider Name="Microsoft-Windows-Security-Auditing" Guid="{54849625-5478-4994-A5BA-3E3B0328C30D}" /> 
  <EventID>4625</EventID> 
  <Version>0</Version> 
  <Level>0</Level> 
  <Task>12544</Task> 
  <Opcode>0</Opcode> 
  <Keywords>0x8010000000000000</Keywords> 
  <TimeCreated SystemTime="2023-07-15T08:12:14.780596300Z" /> 
  <EventRecordID>27785286</EventRecordID> 
  <Correlation /> 
  <Execution ProcessID="992" ThreadID="41708" /> 
  <Channel>Security</Channel> 
  <Computer>COMPUTER</Computer> 
  <Security /> 
  </System>
- <EventData>
  <Data Name="SubjectUserSid">S-1-0-0</Data> 
  <Data Name="SubjectUserName">-</Data> 
  <Data Name="SubjectDomainName">-</Data> 
  <Data Name="SubjectLogonId">0x0</Data> 
  <Data Name="TargetUserSid">S-1-0-0</Data> 
  <Data Name="TargetUserName">administrator</Data> 
  <Data Name="TargetDomainName">domainname</Data> 
  <Data Name="Status">0xc000006d</Data> 
  <Data Name="FailureReason">%%2313</Data> 
  <Data Name="SubStatus">0xc000006a</Data> 
  <Data Name="LogonType">3</Data> 
  <Data Name="LogonProcessName">NtLmSsp</Data> 
  <Data Name="AuthenticationPackageName">NTLM</Data> 
  <Data Name="WorkstationName">LOCALPCNAME</Data> 
  <Data Name="TransmittedServices">-</Data> 
  <Data Name="LmPackageName">-</Data> 
  <Data Name="KeyLength">0</Data> 
  <Data Name="ProcessId">0x0</Data> 
  <Data Name="ProcessName">-</Data> 
  <Data Name="IpAddress">ADDRESS</Data> 
  <Data Name="IpPort">PORT</Data> 
  </EventData>
  </Event>

For OpenSSH we extract these two events: Applications and Services -> OpenSSH -> Admin for IDs 1 and 2:

- <Event xmlns="http://schemas.microsoft.com/win/2004/08/events/event">
- <System>
  <Provider Name="OpenSSH" Guid="{C4B57D35-0636-4BC3-A262-370F249F9802}" /> 
  <EventID>1</EventID> 
  <Version>0</Version> 
  <Level>1</Level> 
  <Task>0</Task> 
  <Opcode>0</Opcode> 
  <Keywords>0x8000000000000000</Keywords> 
  <TimeCreated SystemTime="2023-07-14T17:28:51.261109200Z" /> 
  <EventRecordID>46166</EventRecordID> 
  <Correlation /> 
  <Execution ProcessID="32716" ThreadID="32356" /> 
  <Channel>OpenSSH/Admin</Channel> 
  <Computer>COMPUTER</Computer> 
  <Security UserID="S-1-5-18" /> 
  </System>
- <EventData>
  <Data Name="process">sshd</Data> 
  <Data Name="payload">fatal: Timeout before authentication for ADDRESS port PORT</Data> 
  </EventData>
  </Event>

and

- <Event xmlns="http://schemas.microsoft.com/win/2004/08/events/event">
- <System>
  <Provider Name="OpenSSH" Guid="{C4B57D35-0636-4BC3-A262-370F249F9802}" /> 
  <EventID>2</EventID> 
  <Version>0</Version> 
  <Level>2</Level> 
  <Task>0</Task> 
  <Opcode>0</Opcode> 
  <Keywords>0x8000000000000000</Keywords> 
  <TimeCreated SystemTime="2023-07-13T07:17:18.615649100Z" /> 
  <EventRecordID>45523</EventRecordID> 
  <Correlation /> 
  <Execution ProcessID="12388" ThreadID="24004" /> 
  <Channel>OpenSSH/Admin</Channel> 
  <Computer>COMPUTER</Computer> 
  <Security UserID="S-1-5-18" /> 
  </System>
- <EventData>
  <Data Name="process">sshd</Data> 
  <Data Name="payload">error: maximum authentication attempts exceeded for invalid user root from ADDRESS port PORT ssh2 [preauth]</Data> 
  </EventData>
  </Event>

We ban them with the following:

while($True){	
	write-host (Get-Date)
	$timeFrame = (Get-Date).AddMinutes(-15)
	$attackThreshold = 20
	$maxEvents = 10000

	$logsWithPatterns = @(
		@("Security", 4625, @("Source Network Address")),
		@("OpenSSH/Admin", 2, @("maximum authentication attempts")),
		@("OpenSSH/Admin", 1, @("Timeout before authentication"))
	)

	$newIpAddressesToBan = $logsWithPatterns | %{
		$log = $_[0]
		$id = $_[1]
		$patterns = $_[2]
		write-host $log, " ", $id, " ", $patterns
		
		Get-WinEvent $log -maxevents $maxEvents | ? {$_.id -eq $id } | ?{$_.TimeCreated -ge $timeFrame } | %{ $_.message} | select-string  $patterns | %{ [regex]::match($_,'(\d{1,4}[.]\d{1,4}[.]\d{1,4}[.]\d{1,4})') } | ?{ $_.Success} | %{$_.Groups[0].Value} | group-object | ?{$_.Count -ge $attackThreshold} | %{$_.Name}
	}

	$newIpAddressesToBan = @(($newIpAddressesToBan | %{ $_.Substring(0, $_.lastIndexOf(".")) + ".0/255.255.255.0"}) | sort | get-unique)

	$existingBannedIpAddresses = @((get-netfirewallrule -displayname "Rule for banning" | Get-NetFirewallAddressFilter).RemoteAddress | sort | get-unique)

	$allIpAddresses = (($newIpAddressesToBan + $existingBannedIpAddresses) | sort | get-unique)

	netsh advfirewall firewall set rule name="Rule for banning" new remoteip=([string]::Join(",", $allIpAddresses))
	
	sleep -s 60
}

I get at most 10000 events from the last 15 minutes, and I look for at least 20 attempts from a given IP. I extract IPv4 addresses with a regexp. I also replace them with a network subnet with mask of 24 bits.

Just run this script in the background with Administrator privileges and it will automatically add new IP addresses to the firewall. You need to create the rule Rule for banning manually beforehand as you need. If you need some other patterns or event logs, just add them to the collection at the beginning.

]]>
https://blog.adamfurmanek.pl/2023/01/13/availability-anywhere-part-19/feed/ 0