Line data Source code
1 : #include "PuzzleImpl.h"
2 :
3 : #include "IntegerCast.h"
4 : #include "Parsing.h"
5 : #include "Views.h"
6 :
7 : #include "z3++.h"
8 :
9 : #include <algorithm>
10 : #include <flat_set>
11 : #include <queue>
12 : #include <stdexcept>
13 : #include <string_view>
14 : #include <vector>
15 :
16 : namespace {
17 :
18 : struct MachinePt1 {
19 : unsigned numNodes = 1u;
20 : unsigned target = 0u;
21 : std::vector<unsigned> edges;
22 : };
23 :
24 1 : std::vector<MachinePt1> parsePt1(std::string_view const input) {
25 1 : std::vector<MachinePt1> machines;
26 :
27 1 : std::vector<unsigned> edgeToggles;
28 176 : for (auto const &line : input | views::splitLines) {
29 176 : MachinePt1 machine;
30 :
31 : // Indicator light (target)
32 176 : auto it = line.begin();
33 176 : DEBUG_ASSERT(it != line.end() && *it == '[');
34 176 : ++it;
35 176 : auto lightEndIt = std::find(it, line.end(), ']');
36 176 : DEBUG_ASSERT(lightEndIt != line.end());
37 176 : std::span<char const> const lights{it, lightEndIt};
38 1245 : for (auto const c : lights | std::views::reverse) {
39 1245 : machine.numNodes <<= 1u;
40 1245 : machine.target <<= 1u;
41 1245 : if (c == '#')
42 648 : machine.target |= 1u;
43 597 : else
44 1245 : DEBUG_ASSERT(c == '.');
45 1245 : }
46 176 : it = std::next(lightEndIt);
47 :
48 : // Buttons (edges)
49 1437 : for (auto edgeBeginIt = std::find(it, line.end(), '('); edgeBeginIt != line.end();
50 1261 : edgeBeginIt = std::find(it, line.end(), '(')) {
51 1261 : auto edgeEndIt = std::find(edgeBeginIt, line.end(), ')');
52 1261 : DEBUG_ASSERT(edgeEndIt != line.end());
53 1261 : std::string_view const edgeStr{std::next(edgeBeginIt), edgeEndIt};
54 1261 : edgeToggles.clear();
55 1261 : parseIntegerRange<unsigned>(edgeStr, std::back_inserter(edgeToggles), ',');
56 1261 : DEBUG_ASSERT(edgeToggles.size() <= lights.size());
57 1261 : unsigned edge = 0u;
58 1261 : for (auto const toggle : edgeToggles)
59 4970 : edge |= (1u << toggle);
60 1261 : machine.edges.push_back(edge);
61 1261 : it = std::next(edgeEndIt);
62 1261 : }
63 :
64 176 : machines.push_back(std::move(machine));
65 176 : }
66 :
67 1 : return machines;
68 1 : }
69 :
70 : struct MachinePt2 {
71 : std::vector<std::flat_set<unsigned>> buttons;
72 : std::vector<int> joltages;
73 : };
74 :
75 1 : std::vector<MachinePt2> parsePt2(std::string_view const input) {
76 1 : std::vector<MachinePt2> machines;
77 :
78 1 : std::vector<unsigned> edgeToggles;
79 176 : for (auto const &line : input | views::splitLines) {
80 176 : MachinePt2 machine;
81 :
82 176 : auto it = line.begin();
83 :
84 : // Buttons (edges)
85 1437 : for (auto edgeBeginIt = std::find(it, line.end(), '('); edgeBeginIt != line.end();
86 1261 : edgeBeginIt = std::find(it, line.end(), '(')) {
87 1261 : auto edgeEndIt = std::find(edgeBeginIt, line.end(), ')');
88 1261 : DEBUG_ASSERT(edgeEndIt != line.end());
89 1261 : std::string_view const edgeStr{std::next(edgeBeginIt), edgeEndIt};
90 1261 : std::flat_set<unsigned> &button = machine.buttons.emplace_back();
91 1261 : parseIntegerRange<unsigned>(edgeStr, std::inserter(button, button.end()), ',');
92 1261 : it = std::next(edgeEndIt);
93 1261 : }
94 :
95 : // Joltages
96 176 : auto joltageIt = std::find(it, line.end(), '{');
97 176 : DEBUG_ASSERT(joltageIt != line.end());
98 176 : ++joltageIt;
99 176 : auto joltageEndIt = std::find(joltageIt, line.end(), '}');
100 176 : DEBUG_ASSERT(joltageEndIt != line.end());
101 176 : std::string_view const joltageStr{joltageIt, joltageEndIt};
102 176 : parseIntegerRange<int>(joltageStr, std::back_inserter(machine.joltages), ',');
103 :
104 176 : machines.push_back(std::move(machine));
105 176 : }
106 :
107 1 : return machines;
108 1 : }
109 :
110 : struct QueueEntry {
111 : unsigned node;
112 : unsigned dist;
113 :
114 111374 : bool operator<(QueueEntry const &other) const { return dist > other.dist; }
115 : };
116 :
117 176 : uint64_t minNumButtonPushesPt1(MachinePt1 const &machine) {
118 176 : std::vector<unsigned> dist(machine.numNodes, std::numeric_limits<unsigned>::max());
119 176 : constexpr unsigned source = 0u;
120 176 : dist[source] = 0;
121 :
122 176 : std::priority_queue<QueueEntry> pq;
123 176 : pq.emplace(source, 0);
124 13496 : while (!pq.empty()) {
125 13496 : auto const [node, nodeDist] = pq.top();
126 13496 : pq.pop();
127 :
128 13496 : if (nodeDist > dist[node])
129 0 : continue;
130 :
131 13496 : if (node == machine.target)
132 176 : return nodeDist;
133 :
134 131735 : for (auto const edge : machine.edges) {
135 131735 : unsigned const nextNode = node ^ edge;
136 131735 : unsigned const nextDist = nodeDist + 1;
137 131735 : if (nextDist < dist[nextNode]) {
138 22920 : dist[nextNode] = nextDist;
139 22920 : pq.emplace(nextNode, nextDist);
140 22920 : }
141 131735 : }
142 13320 : }
143 :
144 176 : UNREACHABLE("No solution found");
145 0 : }
146 :
147 176 : uint64_t minNumButtonPushesPt2(MachinePt2 const &machine, z3::context &c) {
148 176 : z3::optimize opt(c);
149 :
150 176 : z3::expr_vector buttonPushesVar(c);
151 1437 : for (size_t i = 0; i < machine.buttons.size(); ++i) {
152 1261 : buttonPushesVar.push_back(c.int_const(std::format("b{}", i).c_str()));
153 1261 : opt.add(buttonPushesVar.back() >= 0);
154 1261 : }
155 176 : z3::expr totalButtonPushes = z3::sum(buttonPushesVar);
156 :
157 1421 : for (unsigned i = 0; i < machine.joltages.size(); ++i) {
158 1245 : z3::expr_vector exprVec(c);
159 10948 : for (size_t j = 0; j < machine.buttons.size(); ++j) {
160 9703 : if (machine.buttons[j].contains(i)) {
161 4970 : exprVec.push_back(buttonPushesVar[j]);
162 4970 : }
163 9703 : }
164 1245 : opt.add(z3::sum(exprVec) == machine.joltages[i]);
165 1245 : }
166 :
167 176 : z3::optimize::handle h1 = opt.minimize(totalButtonPushes);
168 :
169 176 : if (opt.check() == z3::sat) {
170 176 : return opt.lower(h1).as_uint64();
171 176 : }
172 :
173 176 : UNREACHABLE("No solution found");
174 0 : }
175 :
176 : } // namespace
177 :
178 1 : template <> std::string solvePart1<2025, 10>(std::string_view const input) {
179 1 : std::vector<MachinePt1> const machines = parsePt1(input);
180 1 : uint64_t sum = 0u;
181 1 : for (auto const &machine : machines)
182 176 : sum += minNumButtonPushesPt1(machine);
183 1 : return std::to_string(sum);
184 1 : }
185 :
186 1 : template <> std::string solvePart2<2025, 10>(std::string_view const input) {
187 1 : std::vector<MachinePt2> const machines = parsePt2(input);
188 1 : z3::context c;
189 1 : uint64_t sum = 0u;
190 1 : for (auto const &machine : machines)
191 176 : sum += minNumButtonPushesPt2(machine, c);
192 1 : return std::to_string(sum);
193 1 : }
|
