Finally able to remove Z3 from Day 10 thanks tenthmascot

This commit is contained in:
Sebastian Lindemeier 2025-12-12 11:39:03 +01:00
parent ab7af90af9
commit ea4ccd11a5
2 changed files with 250 additions and 13 deletions

View File

@ -23,6 +23,22 @@ public class Day10Test
[Fact] [Fact]
public void Part01_Prod_equals_500() public void Part01_Prod_equals_500()
{
var actual = (_sut as Day10).SolvePart1Unoptimized(ProdInputPath);
Assert.Equal(500, actual);
}
[Fact]
public void Part01Unop_Test_equals_7()
{
var actual = (_sut as Day10).SolvePart1Unoptimized(TestInputPath);
Assert.Equal(7, actual);
}
[Fact]
public void Part01Unop_Prod_equals_500()
{ {
var actual = _sut.SolvePart1(ProdInputPath); var actual = _sut.SolvePart1(ProdInputPath);
@ -37,6 +53,14 @@ public class Day10Test
Assert.Equal(33, actual); Assert.Equal(33, actual);
} }
[Fact]
public void Part02Z3_Test_equals_33()
{
var actual = (_sut as Day10)?.SolvePart2Z3(TestInputPath);
Assert.Equal(33, actual);
}
[Fact] [Fact]
public void Part02_Prod_equals_19763() public void Part02_Prod_equals_19763()
{ {
@ -44,4 +68,12 @@ public class Day10Test
Assert.Equal(19763, actual); Assert.Equal(19763, actual);
} }
[Fact]
public void Part02Z3_Prod_equals_19763()
{
var actual = (_sut as Day10)?.SolvePart2Z3(ProdInputPath);
Assert.Equal(19763, actual);
}
} }

View File

@ -1,4 +1,5 @@
using System; using System;
using System.Collections;
using System.Collections.Generic; using System.Collections.Generic;
using System.Data; using System.Data;
using System.Data.Common; using System.Data.Common;
@ -11,7 +12,7 @@ namespace AoC_2025;
public class Day10 : IPuzzleSolver<long> public class Day10 : IPuzzleSolver<long>
{ {
private (uint lamps, (int[] buttons, uint buttonsMap)[] buttons, int[] joltages)[] ParsePuzzleInput(string path) private (uint lamps, uint[] buttons, int[] joltages)[] ParsePuzzleInput(string path)
{ {
var puzzleInput = File.ReadAllLines(path) var puzzleInput = File.ReadAllLines(path)
.Where(line => !string.IsNullOrWhiteSpace(line)) .Where(line => !string.IsNullOrWhiteSpace(line))
@ -36,7 +37,48 @@ public class Day10 : IPuzzleSolver<long>
.Split(',', StringSplitOptions.RemoveEmptyEntries) .Split(',', StringSplitOptions.RemoveEmptyEntries)
.Select(lampIndex => int.Parse(lampIndex)) .Select(lampIndex => int.Parse(lampIndex))
.ToArray()) .ToArray())
.Select(lampIndexes => (lampIndexes, lampIndexes.Aggregate((uint)0L, (acc, lampIndex) => acc | ((uint)1 << lampIndex)))) .Select(lampIndexes => lampIndexes.Aggregate((uint)0L, (acc, lampIndex) => acc | ((uint)1 << lampIndex)))
.ToArray())
.ToArray();
var joltages = puzzleInput
.Select(input => input.joltages)
.Select(joltage => joltage
.Split(',', StringSplitOptions.RemoveEmptyEntries)
.Select(jolt => int.Parse(jolt))
.ToArray())
.ToArray();
var res = lamps
.Zip(buttons, (lamp, button) => (lamp, button))
.Zip(joltages, (bl, joltage) => (bl.lamp, bl.button, joltage))
.ToArray();
return res;
}
private (bool[] lamps, int[][] buttons, int[] joltages)[] ParsePuzzleInputUnoptimized(string path)
{
var puzzleInput = File.ReadAllLines(path)
.Where(line => !string.IsNullOrWhiteSpace(line))
.Select(line => line.Split(' ', StringSplitOptions.RemoveEmptyEntries))
.Select(instruction => instruction switch
{
[var lamps, ..var buttons, var joltages] => (lamps: lamps[1..^1], buttons, joltages: joltages[1..^1]),
_ => throw new DataException("Misaligned data")
})
.OrderBy(inst => inst.lamps.Length)
.ToArray();
var lamps = puzzleInput
.Select(input => input.lamps)
.Select(lamps => lamps.Index())
.Select(ixlamps =>
ixlamps.Select(ixlamp => ixlamp.Item == '#').ToArray())
.ToArray();
var buttons = puzzleInput
.Select(input => input.buttons)
.Select(buttons => buttons
.Select(button => button[1..^1]
.Split(',', StringSplitOptions.RemoveEmptyEntries)
.Select(lampIndex => int.Parse(lampIndex))
.ToArray())
.ToArray()) .ToArray())
.ToArray(); .ToArray();
var joltages = puzzleInput var joltages = puzzleInput
@ -57,19 +99,39 @@ public class Day10 : IPuzzleSolver<long>
{ {
var instructions = ParsePuzzleInput(pathToPuzzleInput); var instructions = ParsePuzzleInput(pathToPuzzleInput);
var minCounts = instructions var minCounts = instructions
.Select(ins => GetMinCountButtonPressesForLamps(ins.lamps, [..ins.buttons.Select(b => b.buttonsMap)])) .Select(ins => GetMinCountButtonPressesForLamps(ins.lamps, ins.buttons))
.ToArray();
return minCounts.Sum();
}
public long SolvePart1Unoptimized(string pathToPuzzleInput)
{
var instructions = ParsePuzzleInputUnoptimized(pathToPuzzleInput);
var minCounts = instructions
.Select(ins =>
GetButtonPatternCostsForLamps(ins.lamps, ins.buttons)
.Order()
.First())
.ToArray(); .ToArray();
return minCounts.Sum(); return minCounts.Sum();
} }
public long SolvePart2(string pathToPuzzleInput) public long SolvePart2(string pathToPuzzleInput)
{ {
var instructions = ParsePuzzleInput(pathToPuzzleInput); var instructions = ParsePuzzleInputUnoptimized(pathToPuzzleInput);
var minCounts = instructions var minCounts = instructions
.Select(ins => GetMinCountButtonPressesForJoltages(ins.joltages, [..ins.buttons.Select(b => b.buttons)])) .Select(instruction => GetMinCountButtonPressesForJoltageLevels(instruction.joltages, instruction.buttons));
return minCounts.Sum();
}
// not proud of you
public long SolvePart2Z3(string pathToPuzzleInput)
{
var instructions = ParsePuzzleInputUnoptimized(pathToPuzzleInput);
var minCounts = instructions
.Select(ins => GetMinCountButtonPressesForJoltagesZ3(ins.joltages, ins.buttons))
.ToArray(); .ToArray();
var sum = minCounts.Sum(); return minCounts.Sum();
return sum;
} }
private long GetMinCountButtonPressesForLamps(uint lamps, uint[] buttons) private long GetMinCountButtonPressesForLamps(uint lamps, uint[] buttons)
@ -86,17 +148,93 @@ public class Day10 : IPuzzleSolver<long>
} }
return presses; return presses;
}
private uint[] GetLampStates(uint lampState, uint[] buttons) static uint[] GetLampStates(uint lampState, uint[] buttons)
{ {
var states = buttons var states = buttons
.Where(button => (lampState & button) > 0) .Where(button => (lampState & button) > 0)
.Select(button => lampState ^ button); .Select(button => lampState ^ button);
return [..states]; return [..states];
} }
}
private long GetMinCountButtonPressesForJoltages(int[] joltages, int[][] buttons) private IEnumerable<int> GetButtonPatternCostsForLamps(bool[] lampState, int[][] buttons)
{
if (lampState.All(x => !x))
{
yield return 0;
yield break;
}
foreach (var (pattern, cost) in GetPatternCosts(lampState.Length, buttons))
{
if (pattern.Zip(lampState, (pat, lam) => (pat % 2 == 1) == lam).All(x => x))
{
yield return cost;
}
}
}
private long GetMinCountButtonPressesForJoltageLevels(int[] joltages, int[][] buttons)
{
var patternCosts = GetPatternCosts(joltages.Length, buttons).ToArray();
var res = GetMinCountInternal(joltages, patternCosts, new Dictionary<int[], long>(new IntArrayEqualityComparer()));
return res;
static long GetMinCountInternal(int[] joltages, (int[] joltages, int cots)[] patternCosts, Dictionary<int[], long> memory)
{
if (joltages.All(j => j == 0)) return 0;
if (memory.TryGetValue(joltages, out var knownResult)) return knownResult;
var minCount = 1_000_000_000L;
var joltageLevels = patternCosts
.Where(pc => pc.joltages.Zip(joltages, (pJolt, jJolt) => (pJolt % 2) == (jJolt % 2)).All(isEqual => isEqual))
.ToArray();
foreach (var (joltageLevel, buttonPresses) in joltageLevels)
{
var nextPattern = joltages.Zip(joltageLevel, (jolts, level) => (jolts - level) / 2).ToArray();
var resultNext = 2 * GetMinCountInternal(nextPattern, patternCosts, memory) + buttonPresses;
if (resultNext < minCount)
{
minCount = resultNext;
}
}
memory[joltages] = minCount;
return minCount;
}
}
private IEnumerable<(int[], int)> GetPatternCosts(int patternLength, int[][] buttons)
{
yield return ([..Enumerable.Repeat(0, patternLength)], 0);
for (var i = 1; i <= buttons.Length; i++)
{
foreach (var buttonPattern in Combinations(buttons, i))
{
var joltageLevels = GetJoltageLevelsForButtonPattern(patternLength, buttonPattern);
yield return (joltageLevels, buttonPattern.Length);
}
}
yield break;
static int[] GetJoltageLevelsForButtonPattern(int countLamps, int[][] buttonPattern)
{
var innerState = Enumerable.Repeat(0, countLamps).ToArray();
foreach (var button in buttonPattern)
{
foreach (var index in button)
{
innerState[index]++;
}
}
return innerState;
}
}
private long GetMinCountButtonPressesForJoltagesZ3(int[] joltages, int[][] buttons)
{ {
using var context = new Context(); using var context = new Context();
var optimize = context.MkOptimize(); var optimize = context.MkOptimize();
@ -129,4 +267,71 @@ public class Day10 : IPuzzleSolver<long>
var answer = answerExpression is IntNum number ? number.Int64 : 0; var answer = answerExpression is IntNum number ? number.Int64 : 0;
return answer; return answer;
} }
private IEnumerable<TValue[]> Combinations<TValue>(IEnumerable<TValue> values, int count)
{
var pool = values.ToArray();
var poolLength = pool.Length;
if (count > poolLength)
yield break;
var indices = Range(0, count).ToArray();
yield return GetCombination(indices, pool);
while (true)
{
var validIndex = false;
var currentIndex = 0;
foreach (var i in Range(0, count).Reverse())
{
currentIndex = i;
if (indices[i] != i + poolLength - count)
{
validIndex = true;
break;
}
}
if(!validIndex)
yield break;
indices[currentIndex] += 1;
foreach (var j in Range(currentIndex + 1, count))
{
Index ix = j - 1;
indices[j] = indices[ix] + 1;
}
yield return GetCombination(indices, pool);
}
static TValue[] GetCombination(int[] innerIndices, TValue[] innerPool) =>
innerIndices.Select(i => innerPool[i]).ToArray();
static IEnumerable<int> Range(int start, int end)
{
for (var i = start; i < end; i++)
yield return i;
}
}
}
public class IntArrayEqualityComparer : IEqualityComparer<int[]>
{
public bool Equals(int[]? x, int[]? y)
{
if (x is null || y is null || x.Length != y.Length) return false;
return !x.Where((t, i) => t != y[i]).Any();
}
public int GetHashCode(int[] obj)
{
var result = 17;
foreach (var t in obj)
{
unchecked
{
result = result * 23 + t;
}
}
return result;
}
} }