Refactor Day10 to enhance button and joltage handling, implement Z3 solver for Part 2 logic, and update tests accordingly

This commit is contained in:
Sebastian Lindemeier 2025-12-11 12:05:45 +01:00
parent 3d305d80bf
commit 3af6cc3233
3 changed files with 55 additions and 15 deletions

View File

@ -30,18 +30,18 @@ public class Day10Test
}
[Fact]
public void Part02_Test_equals_24()
public void Part02_Test_equals_33()
{
var actual = _sut.SolvePart2(TestInputPath);
Assert.Equal(24, actual);
Assert.Equal(33, actual);
}
[Fact]
public void Part02_Prod_equals_1568849600()
public void Part02_Prod_equals_19763()
{
var actual = _sut.SolvePart2(ProdInputPath);
Assert.Equal(1568849600, actual);
Assert.Equal(19763, actual);
}
}

View File

@ -10,4 +10,8 @@
<ProjectReference Include="..\AdvenOfCode.Contracts\AdvenOfCode.Contracts.csproj" />
</ItemGroup>
<ItemGroup>
<PackageReference Include="Microsoft.Z3" Version="4.12.2" />
</ItemGroup>
</Project>

View File

@ -5,13 +5,13 @@ using System.Data.Common;
using System.IO;
using System.Linq;
using AdvenOfCode.Contracts;
using Microsoft.Z3;
namespace AoC_2025;
public class Day10 : IPuzzleSolver<long>
{
private static int done = 0;
private (uint lamps, uint[] buttons, int[] joltages)[] ParsePuzzleInput(string path)
private (uint lamps, (int[] buttons, uint buttonsMap)[] buttons, int[] joltages)[] ParsePuzzleInput(string path)
{
var puzzleInput = File.ReadAllLines(path)
.Where(line => !string.IsNullOrWhiteSpace(line))
@ -35,7 +35,8 @@ public class Day10 : IPuzzleSolver<long>
.Select(button => button[1..^1]
.Split(',', StringSplitOptions.RemoveEmptyEntries)
.Select(lampIndex => int.Parse(lampIndex))
.Aggregate((uint)0L, (acc, lampIndex) => acc | ((uint)1 << lampIndex)))
.ToArray())
.Select(lampIndexes => (lampIndexes, lampIndexes.Aggregate((uint)0L, (acc, lampIndex) => acc | ((uint)1 << lampIndex))))
.ToArray())
.ToArray();
var joltages = puzzleInput
@ -55,19 +56,23 @@ public class Day10 : IPuzzleSolver<long>
public long SolvePart1(string pathToPuzzleInput)
{
var instructions = ParsePuzzleInput(pathToPuzzleInput);
Console.WriteLine($"total: {instructions.Length}");
var minCounts = instructions
.Select(ins => GetMinCountButtonPressesForLamps(ins.lamps, ins.buttons))
.Select(ins => GetMinCountButtonPressesForLamps(ins.lamps, [..ins.buttons.Select(b => b.buttonsMap)]))
.ToArray();
return minCounts.Sum();
}
public long SolvePart2(string pathToPuzzleInput)
{
return 0;
var instructions = ParsePuzzleInput(pathToPuzzleInput);
var minCounts = instructions
.Select(ins => GetMinCountButtonPressesForJoltages(ins.joltages, [..ins.buttons.Select(b => b.buttons)]))
.ToArray();
var sum = minCounts.Sum();
return sum;
}
private static long GetMinCountButtonPressesForLamps(uint lamps, uint[] buttons)
private long GetMinCountButtonPressesForLamps(uint lamps, uint[] buttons)
{
var presses = 0L;
HashSet<uint> lampStates = [lamps];
@ -80,17 +85,48 @@ public class Day10 : IPuzzleSolver<long>
presses++;
}
var amount = Interlocked.Increment(ref done);
Console.WriteLine($"done: {amount}, presses: {presses}");
return presses;
}
private static uint[] GetLampStates(uint lampState, uint[] buttons)
private uint[] GetLampStates(uint lampState, uint[] buttons)
{
var states = buttons
.Where(button => (lampState & button) > 0)
.Select(button => lampState ^ button);
return [..states];
}
private long GetMinCountButtonPressesForJoltages(int[] joltages, int[][] buttons)
{
using var context = new Context();
var optimize = context.MkOptimize();
var variables = Enumerable.Range(0, buttons.Length)
.Select(ix => context.MkIntConst($"n{ix}"))
.ToArray();
foreach (var variable in variables)
{
optimize.Add(variable >= 0);
}
var zero = context.MkInt(0);
foreach (var (i, joltage) in joltages.Index())
{
var equation = zero + zero;
foreach (var (b, button) in buttons.Index())
{
if(button.Contains(i))
equation += variables[b];
}
optimize.Add(context.MkEq(equation, context.MkInt(joltage)));
}
var sumVariables = variables.Aggregate(zero + zero, (current, variable) => current + variable);
optimize.MkMinimize(sumVariables);
optimize.Check();
var answerExpression = optimize.Model.Eval(sumVariables);
var answer = answerExpression is IntNum number ? number.Int64 : 0;
return answer;
}
}