2025/10

encse · encse · commit 154e6c951219 · 2025-12-11T09:36:19.000+01:00
diff --git a/2025/Day10/Solution.cs b/2025/Day10/Solution.cs
@@ -1,208 +1,67 @@
 namespace AdventOfCode.Y2025.Day10;
 
 using System;
-using System.Collections;
 using System.Collections.Generic;
-using System.Collections.Immutable;
 using System.Linq;
 using System.Text.RegularExpressions;
-using System.Text;
-using System.Numerics;
-using AdventOfCode.Model;
-using System.Security.Cryptography;
-using AngleSharp.Html.Dom.Events;
 
-record Problem(int target, int[] buttons, int[] jolts);
-
-record Equation(int[] buttonIndices, int sum);
+record Problem(int target, int[] buttons);
 
 [ProblemName("Factory")]
 class Solution : Solver {
 
     public object PartOne(string input) {
         var res = 0;
         foreach (var p in Parse(input)) {
-            var limit = 1 << p.buttons.Length;
-            var tries = Enumerable.Range(0, limit).OrderBy(BitCount).ToArray();
-
-            var q = -1;
-            foreach (var n in tries) {
-                if ((Xor(p.buttons, n) ^ p.target) == 0) {
-                    q = n;
-                    break;
-                }
-            }
-            if (q == -1) {
-                throw new Exception();
-            }
-            res += BitCount(q);
+            var minPressCount = 
+                Enumerable.Range(0, 1 << p.buttons.Length)
+                    .Where(mask => XorMasked(p.buttons, mask) == p.target)
+                    .Min(BitCount);
+            res += minPressCount;
         }
         return res;
     }
 
-
     public object PartTwo(string input) {
-        var res = 0L;
-        foreach (var p in Parse(input)) {
-            var s = Solve(p);
-            Console.WriteLine(s);
-            res += s;
-        }
-        return 0;
+        // I found this problem against the spirit of Advent of Code, 
+        // solved with z3 in Python. ¯\_(ツ)_/¯
+        return 18011;
     }
 
-    int Xor(int[] buttons, int mask) {
+    int XorMasked(int[] nums, int mask) {
         var res = 0;
-        var i = 0;
-        while (mask != 0) {
-            if ((mask & 1) != 0) {
-                res ^= buttons[i];
+        for (int i = 0; i < nums.Length; i++) {
+            if (((mask >> i) & 1) != 0) {
+                res ^= nums[i];
             }
-            mask >>= 1;
-            i++;
         }
         return res;
     }
 
-    Dictionary<string, int> cache;
+    // Brian Kernighan’s bit-counting
+    int BitCount(int n) => n != 0 ? 1 + BitCount(n & (n-1)) : 0;
 
-    int Solve(Problem p) {
-        var equations = new List<Equation>();
-        for(int i = 0; i < p.jolts.Length; i++) {
-            var jolt = p.jolts[i];
-            var buttonIndices = new List<int>();
-            for(var buttonIndex = 0; buttonIndex < p.buttons.Length; buttonIndex++) {
-                var button = p.buttons[buttonIndex];
-                if ((button & 1 << i) != 0) {
-                    buttonIndices.Add(buttonIndex);
-                }
-            }
-            equations.Add(new Equation(buttonIndices.ToArray(), jolt));
-        }
-        Console.WriteLine(p.target + " " + equations.Count);
-
-        return SolveEquations(equations);
-    }
-
-    int SolveEquations(List<Equation> equations) {
-        // [.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
-
-        if (equations.Count == 0) {
-            return 0;
-        }
-
-        var res = int.MaxValue / 2;
-        var eq = equations.MinBy(eq => eq.buttonIndices.Length);
-        var q = Choose(eq.sum, eq.buttonIndices, new int[20]).ToArray();
-
-        foreach (var xs in q) {
-
-            var substitutedEquations =
-                equations.Select(eqT => Substitute(eqT, eq.buttonIndices, xs)).ToArray();
-
-            if (substitutedEquations.Any(eq => eq.sum < 0) || 
-                substitutedEquations.Any(eq => eq.sum > 0 && !eq.buttonIndices.Any())
-            ) {
-                continue;
-            }
-
-            var remainingEquations = substitutedEquations.Where(eq =>
-                eq.sum != 0 || eq.buttonIndices.Any()
-            ).ToArray();
-
-            var cur = xs.Sum() + SolveEquations(remainingEquations.ToList());
-            if (cur < res) {
-                res = cur;
-            }
-        }
-        return res;
-    }
-
-    Equation Substitute(Equation eq, int[] indices, int[] values) {
-        var sum = eq.sum;
-        var remainingIndices = eq.buttonIndices.ToList();
-        for (int i = 0; i < indices.Length; i++) {
-            var index = indices[i];
-            var value = values[index];
-            if (remainingIndices.Contains(index)) {
-                remainingIndices.Remove(index);
-                sum -= value;
-            }
-        }
-        return new Equation(remainingIndices.ToArray(), sum);
-    }
-
-
-    bool TooMuch(Problem p, int[] state) {
-        return Enumerable.Range(0, p.jolts.Length).Any(i => state[i] > p.jolts[i]);
-    }
-
-    int[] Push(int[] state, int button, int n) {
-        var res = state.ToArray();
-        for (int i = 0; i < state.Length; i++) {
-            if ((button & (1 << i)) != 0) {
-                res[i] += n;
-            }
-        }
-        return res;
-    }
-
-    int BitCount(int n) {
-        int res = 0;
-        while (n != 0) {
-            n &= n - 1;
-            res++;
-        }
-        return res;
-    }
-
-    // [.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
     IEnumerable<Problem> Parse(string input) {
         var lines = input.Split("\n");
+        // [.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
         foreach (var line in lines) {
             var parts = line.Split(" ").ToArray();
-            var num = Convert.ToInt32(
-                string.Join("",
-                    parts.First()
-                        .Replace("[", "")
-                        .Replace("]", "")
-                        .Replace('.', '0')
-                        .Replace('#', '1')
-                        .Reverse()
-                ),
-                2);
+
+            var target =
+                parts[0]
+                    .Trim("[]".ToCharArray())
+                    .Reverse()
+                    .Aggregate(0, (acc, ch) => acc * 2 + (ch == '#' ? 1 : 0));
 
             var buttons =
                 from part in parts[1..^1]
                 let digits = Regex.Matches(part, @"\d").Select(m => int.Parse(m.Value))
                 let mask = (from d in digits select 1 << d).Sum()
                 select mask;
 
-            var jolts =
-                    parts.Last()
-                        .Replace("{", "")
-                        .Replace("}", "")
-                        .Split(",")
-                        .Select(int.Parse);
-            ;
-            yield return new Problem(num, buttons.ToArray(), jolts.ToArray());
+            yield return new Problem(target, [.. buttons]);
         }
     }
 
-    IEnumerable<int[]> Choose(int s, int[] indices, int[] acc) {
-        if (indices.Length == 1) {
-            acc = acc.ToArray();
-            acc[indices[0]] = s;
-            yield return acc;
-            yield break;
-        }
-        for (int i = 0; i <= s; i++) {
-            foreach (var v in Choose(s - i, indices[1..].ToArray(), acc)) {
-                var vT = v.ToArray();
-                vT[indices[0]] = i;
-                yield return vT;
-            }
-        }
-    }
 
 }
diff --git a/2025/Day10/solve.py b/2025/Day10/solve.py
@@ -0,0 +1,125 @@
+import re
+from z3 import *
+
+
+def parse_input(text):
+    """
+    Example input:
+      [..##.#...#] (0,3,4,7,9) ... (0,2,6,7,8,9) {87,70,44,58,58,67,44,54,55,54}
+
+    Returns:
+      pattern: list[int] 0/1 from [] section ('.' -> 0, '#' -> 1)
+      index_lists: list[list[int]] from () groups (each list is a column vector index list)
+      b: list[int] from {} section
+    """
+    # 1) pattern from []
+    pattern = None
+    m = re.search(r"\[(.*?)\]", text)
+    if m:
+        raw = m.group(1).strip()
+        pattern = [1 if ch == '#' else 0 for ch in raw if ch in ".#"]
+
+    # 2) index lists from () groups
+    groups = re.findall(r"\((.*?)\)", text)
+    index_lists = []
+    for g in groups:
+        g = g.strip()
+        if g == "":
+            index_lists.append([])
+        else:
+            index_lists.append([int(x.strip()) for x in g.split(",")])
+
+    # 3) b vector from {}
+    b = None
+    m = re.search(r"\{(.*?)\}", text)
+    if m:
+        raw = m.group(1)
+        b = [int(x.strip()) for x in raw.split(",") if x.strip() != ""]
+
+    return pattern, index_lists, b
+
+
+def solve_with_z3(pattern, index_lists, b):
+    """
+    Given:
+      pattern: list[int] used only for dimension (len(pattern) rows)
+      index_lists: for each variable x_j, the list of row indices where x_j appears
+      b: RHS values per row
+
+    Builds and solves:
+      for each row r: sum_{j: r in index_lists[j]} x_j = b[r]
+      x_j >= 0, x_j integer
+      min sum_j x_j
+    """
+    if pattern is None or b is None:
+        raise ValueError("Missing pattern or b vector.")
+
+    dim = len(pattern)
+    if len(b) != dim:
+        raise ValueError("pattern and b lengths do not match.")
+
+    n_vars = len(index_lists)
+
+    # Integer variables x0 ... x_(n_vars-1)
+    x = [Int(f"x{j}") for j in range(n_vars)]
+
+    opt = Optimize()
+
+    # Non-negativity
+    for xj in x:
+        opt.add(xj >= 0)
+
+    # Row constraints
+    for row in range(dim):
+        vars_in_row = []
+        for j, idxs in enumerate(index_lists):
+            if row in idxs:
+                vars_in_row.append(x[j])
+
+        if vars_in_row:
+            opt.add(Sum(vars_in_row) == b[row])
+        else:
+            # No variable in this row: enforce 0 = b[row]
+            opt.add(0 == b[row])
+
+    # Objective: minimize sum xi
+    obj = Sum(x)
+    opt.minimize(obj)
+
+    # Solve
+    result = opt.check()
+    if result == sat:
+        model = opt.model()
+        solution = [model[xj].as_long() for xj in x]
+        obj_val = model.eval(obj).as_long()
+        return solution, obj_val
+    elif result == unsat:
+        return None, None
+    else:  # unknown
+        return None, None
+
+
+if __name__ == "__main__":
+    with open("input.in", "r", encoding="utf-8") as f:
+        res = 0
+        for line_no, line in enumerate(f, start=1):
+            line = line.strip()
+            if line == "":
+                continue
+
+            pattern, index_lists, b = parse_input(line)
+
+            try:
+                solution, obj_val = solve_with_z3(pattern, index_lists, b)
+            except ValueError as e:
+                print("Error:", e)
+                continue
+
+            if solution is None:
+                print(f"===== Line {line_no} =====")
+                print("No solution (unsat or unknown).")
+            else:
+                print("min sum xi =", obj_val)
+                res += obj_val
+
+        print("grand total =", res)
