ILP Part 73 — Matchstick puzzle

This is the seventieth third 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’re going to solve a matchstick puzzle. Move one stick to make the equality hold:

 --        --     --
|      |     |   |  |
 --   ---  --  =  --
|  |   |  |         |
 --        --     --

-- -- --

| | | | |

-- --- -- = --

| | | | |

-- -- --

which is 6 + 2 = 9.

Solution is rather trivial but let’s encode it in ILP:

var initial = new int[]{0, 2, 3, 4, 5, 6, 7, 8, 10, 11, 13, 14,15, 16, 17, 19, 20};
var toMove = 1;
var digits = 3;

// All segments
var matches = Enumerable.Range(0, digits * 7).Select(i => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray();

// Variables representing particular digits
var digitVars = Enumerable.Range(0, digits).Select(i => solver.CreateAnonymous(Domain.PositiveOrZeroInteger)).ToArray();

// Make sure digits are less than 10
foreach(var v in digitVars){
	v.Set<LessOrEqual>(solver.FromConstant(9));
}

solver.Operation<Addition>(initial.Select(i => matches[i]).ToArray()).Set<Equal>(solver.FromConstant(initial.Length - toMove));
solver.Operation<Addition>(matches.ToArray()).Set<Equal>(solver.FromConstant(initial.Length));

for(int i=0;i<digits;++i){
	var digitMatches = matches.Skip(i * 7).Take(7).ToArray();
	
	var digitFlags = new Dictionary<int, int[]>(){
		{0, new int []{0, 1, 2, 3, 4, 5}},
		{1, new int []{1, 2}},
		{2, new int []{0, 1, 3, 4, 6}},
		{3, new int []{0, 1, 2, 3, 6}},
		{4, new int []{1, 2, 5, 6}},
		{5, new int []{0, 2, 3, 5, 6}},
		{6, new int []{0, 2, 3, 4, 5, 6}},
		{7, new int []{0, 1, 2}},
		{8, new int []{0, 1, 2, 3, 4, 5, 6}},
		{9, new int []{0, 1, 2, 3, 5, 6}}
	};
	
	foreach(var key in digitFlags.Keys){
		var isSet = solver.FromConstant(1);
		for(int segment = 0; segment < 7; ++ segment){
			if(digitFlags[key].Contains(segment)){
				isSet = isSet.Operation<Conjunction>(digitMatches[segment]);
			}else{
				isSet = isSet.Operation<Conjunction>(digitMatches[segment].Operation<BinaryNegation>());
			}
		}
		
		if(key == 0){
			isSet = isSet.Operation<Disjunction>(solver.Operation<Addition>(digitMatches).Operation<IsEqual>(solver.FromConstant(0)));
		}
		
		solver.Operation<MaterialImplication>(isSet, digitVars[i].Operation<IsEqual>(solver.FromConstant(key))).Set<Equal>(solver.FromConstant(1));
		solver.Operation<MaterialImplication>(isSet.Operation<BinaryNegation>(), digitVars[i].Operation<IsNotEqual>(solver.FromConstant(key))).Set<Equal>(solver.FromConstant(1));
	}
}

digitVars[0].Operation<Addition>(digitVars[1]).Set<Equal>(digitVars[2]);

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

foreach(var v in digitVars){
	Console.Write(solver.GetValue(v));
}
Console.WriteLine();
Console.WriteLine("-----");
foreach(var v in matches){
	Console.Write(solver.GetValue(v));
}

var initial = new int[]{0, 2, 3, 4, 5, 6, 7, 8, 10, 11, 13, 14,15, 16, 17, 19, 20};

var toMove = 1;

var digits = 3;

// All segments

var matches = Enumerable.Range(0, digits * 7).Select(i => solver.CreateAnonymous(Domain.BinaryInteger)).ToArray();

// Variables representing particular digits

var digitVars = Enumerable.Range(0, digits).Select(i => solver.CreateAnonymous(Domain.PositiveOrZeroInteger)).ToArray();

// Make sure digits are less than 10

foreach(var v in digitVars){

v.Set<LessOrEqual>(solver.FromConstant(9));

}

solver.Operation<Addition>(initial.Select(i => matches[i]).ToArray()).Set<Equal>(solver.FromConstant(initial.Length - toMove));

solver.Operation<Addition>(matches.ToArray()).Set<Equal>(solver.FromConstant(initial.Length));

for(int i=0;i<digits;++i){

var digitMatches = matches.Skip(i * 7).Take(7).ToArray();

var digitFlags = new Dictionary<int, int[]>(){

{0, new int []{0, 1, 2, 3, 4, 5}},

{1, new int []{1, 2}},

{2, new int []{0, 1, 3, 4, 6}},

{3, new int []{0, 1, 2, 3, 6}},

{4, new int []{1, 2, 5, 6}},

{5, new int []{0, 2, 3, 5, 6}},

{6, new int []{0, 2, 3, 4, 5, 6}},

{7, new int []{0, 1, 2}},

{8, new int []{0, 1, 2, 3, 4, 5, 6}},

{9, new int []{0, 1, 2, 3, 5, 6}}

};

foreach(var key in digitFlags.Keys){

var isSet = solver.FromConstant(1);

for(int segment = 0; segment < 7; ++ segment){

if(digitFlags[key].Contains(segment)){

isSet = isSet.Operation<Conjunction>(digitMatches[segment]);

}else{

isSet = isSet.Operation<Conjunction>(digitMatches[segment].Operation<BinaryNegation>());

}

if(key == 0){

isSet = isSet.Operation<Disjunction>(solver.Operation<Addition>(digitMatches).Operation<IsEqual>(solver.FromConstant(0)));

}

solver.Operation<MaterialImplication>(isSet, digitVars[i].Operation<IsEqual>(solver.FromConstant(key))).Set<Equal>(solver.FromConstant(1));

solver.Operation<MaterialImplication>(isSet.Operation<BinaryNegation>(), digitVars[i].Operation<IsNotEqual>(solver.FromConstant(key))).Set<Equal>(solver.FromConstant(1));

}

digitVars[0].Operation<Addition>(digitVars[1]).Set<Equal>(digitVars[2]);

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

solver.Solve();

foreach(var v in digitVars){

Console.Write(solver.GetValue(v));

}

Console.WriteLine();

Console.WriteLine("-----");

foreach(var v in matches){

Console.Write(solver.GetValue(v));

}

We use 7 segment displays with elements in this order:

5 1

4 2

so it is top, top-right, bottom-right, bottom, bottom-left, top-left, middle.

In line 1 we specify initial state. In lines 2-3 we define how many moves to make and how many digits in total we have.
Next, in line 6 we define matches, and in line 9 we define variables for digits.

In lines 12-14 we specify that digits must be less than ten. Next, in lines 16-17 we specify that at most one match of the initial state can be moved.

Next, in lines 19-52 we translate 7 segment displays to digits. We define patters in lines 22-33. Next, in liens 35-51 we iterate over patterns, take respective segments, and make sure that if segments are set then digit is formed accordingly.

Finally, in line 54 we define the equation.

Output:

Tried aggregator 2 times.
MIP Presolve eliminated 253 rows and 99 columns.
MIP Presolve modified 855 coefficients.
Aggregator did 411 substitutions.
Reduced MIP has 698 rows, 348 columns, and 1826 nonzeros.
Reduced MIP has 345 binaries, 3 generals, 0 SOSs, and 0 indicators.
Presolve time = 0.02 sec. (7.27 ticks)
Probing fixed 345 vars, tightened 23 bounds.
Probing time = 0.00 sec. (0.60 ticks)
Tried aggregator 1 time.
MIP Presolve eliminated 698 rows and 348 columns.
All rows and columns eliminated.
Presolve time = 0.00 sec. (0.29 ticks)

Root node processing (before b&c):
  Real time             =    0.02 sec. (11.93 ticks)
Parallel b&c, 8 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.02 sec. (11.93 ticks)
639
-----
101111111110011111011

Tried aggregator 2 times.

MIP Presolve eliminated 253 rows and 99 columns.

MIP Presolve modified 855 coefficients.

Aggregator did 411 substitutions.

Reduced MIP has 698 rows, 348 columns, and 1826 nonzeros.

Reduced MIP has 345 binaries, 3 generals, 0 SOSs, and 0 indicators.

Presolve time = 0.02 sec. (7.27 ticks)

Probing fixed 345 vars, tightened 23 bounds.

Probing time = 0.00 sec. (0.60 ticks)

Tried aggregator 1 time.

MIP Presolve eliminated 698 rows and 348 columns.

All rows and columns eliminated.

Presolve time = 0.00 sec. (0.29 ticks)

Root node processing (before b&c):

Real time = 0.02 sec. (11.93 ticks)

Parallel b&c, 8 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.02 sec. (11.93 ticks)

639

-----

101111111110011111011

It worked in 0.02 second.