qqq

Author: encse

2025/Day10/Solution.cs

@@ -14,6 +14,8 @@ namespace AdventOfCode.Y2025.Day10;
 
 record Problem(int target, int[] buttons, int[] jolts);
 
+record Equation(int[] buttonIndices, int sum);
+
 [ProblemName("Factory")]
 class Solution : Solver {
 
@@ -41,16 +43,12 @@ public object PartOne(string input) {
 
     public object PartTwo(string input) {
         var res = 0L;
-        var i = 1;
         foreach (var p in Parse(input)) {
-            Console.WriteLine(i +  " " + p.buttons.Length + " " + p.jolts.Length);
-            i++;
+            var s = Solve(p);
+            Console.WriteLine(s);
+            res += s;
         }
-        return res;
-    }
-
-    bool TooMuch(Problem p, int[] state) {
-        return Enumerable.Range(0, state.Length).Any(i => state[i] > p.jolts[i]);
+        return 0;
     }
 
     int Xor(int[] buttons, int mask) {
@@ -66,35 +64,84 @@ int Xor(int[] buttons, int mask) {
         return res;
     }
 
-    int Solve(Problem p, int pushes, int[] state) {
-        if (pushes > 11) {
-            return int.MaxValue;
+    Dictionary<string, int> cache;
+
+    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);
 
-        if (Array.Equals(state, p.jolts)) {
-            return pushes;
+        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;
         }
 
-        if (Enumerable.Range(0, state.Length).Any(i => state[i] > p.jolts[i])) {
-            return int.MaxValue;
-        } 
+        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 res = int.MaxValue;
-        for (int i = 0; i < p.buttons.Length; i++) {
-            var stateT = Push(state, p.buttons[i]);
-            var m = Solve(p, pushes + 1, stateT);
-            if (m < res) {
-                res = m;
+            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;
     }
 
-    int[] Push(int[] state, int button) {
+    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]++;
+                res[i] += n;
             }
         }
         return res;
@@ -142,4 +189,20 @@ from part in parts[1..^1]
         }
     }
 
+    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;
+            }
+        }
+    }
+
 }

2025/Day10/bar.py

@@ -265,10 +265,10 @@ def combinations(n):
                         s = np.sum(x)
                     if s < best:
                         best = s
-                        print("  x =", x, "i=", i, "sum=", s, "res=", res) 
+                        # print("  x =", x, "i=", i, "sum=", s, "res=", res) 
 
                 if i is None or np.sum(i) >= best:
                     break
-
+            print("  best:", best)
             res += best
     print(int(res))

2025/Day10/eq.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)