1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
#include <algorithm>
#include <filesystem>
#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#include <z3++.h>
using namespace std;
namespace {
struct Machine {
Machine(const vector<vector<unsigned long>>& buttons, const vector<unsigned long>& joltages)
: buttons_{ buttons }
, joltages_{ joltages }
{
}
vector<vector<unsigned long>> buttons_;
vector<unsigned long> joltages_;
};
vector<string>
split(const string& str, const string& delims)
{
vector<string> result;
size_t start = str.find_first_not_of(delims);
while ( start != string::npos ) {
size_t end = str.find_first_of(delims, start);
if ( end == string::npos ) {
// letzter Teil
result.push_back(str.substr(start));
break;
}
result.push_back(str.substr(start, end - start));
start = str.find_first_not_of(delims, end);
}
return result;
}
vector<unsigned long>
split(const string& str)
{
stringstream strm{ str };
vector<unsigned long> values;
for ( string part; getline(strm, part, ','); ) {
values.emplace_back(stoul(part));
}
return values;
}
vector<Machine>
read_file(const filesystem::path& filename)
{
ifstream file{ filename };
vector<Machine> machines;
for ( string line; getline(file, line); ) {
const auto parts = split(line, "[] (){}");
vector<vector<unsigned long>> buttons;
for ( size_t i = 1; i < parts.size() - 1; ++i ) {
buttons.emplace_back(split(parts[i]));
}
const auto joltages = split(parts[parts.size() - 1]);
machines.emplace_back(buttons, joltages);
}
return machines;
}
unsigned long
simulate(const Machine& machine)
{
using namespace z3;
context ctx;
optimize opt(ctx);
const size_t num_buttons = machine.buttons_.size();
const size_t num_counters = machine.joltages_.size();
// Z3-Variablen: Anzahl der Button-Presses
vector<expr> vars;
vars.reserve(num_buttons);
for ( size_t i = 0; i != num_buttons; ++i ) {
expr var = ctx.int_const(("x_" + to_string(i)).c_str());
opt.add(var >= 0); // natürliche Zahlen
vars.emplace_back(var);
}
// Joltage-Constraints: Für jeden Counter i
for ( size_t i = 0; i != num_counters; ++i ) {
expr sum = ctx.int_val(0);
for ( size_t j = 0; j != num_buttons; ++j ) {
// Prüfen: affectet Button j den Counter i?
const auto& btn = machine.buttons_[j];
if ( ranges::find(btn, i) != btn.end() ) {
sum = sum + vars[j];
}
}
opt.add(sum == (int) machine.joltages_[i]);
}
// Zielfunktion: Minimale Gesamtzahl der Presses
expr total = ctx.int_val(0);
for ( size_t i = 0; i != num_buttons; ++i ) {
total = total + vars[i];
}
opt.minimize(total);
// Solve
if ( opt.check() != sat ) {
throw runtime_error("Machine has no valid solution!");
}
auto model = opt.get_model();
unsigned long presses = 0;
for ( size_t j = 0; j < num_buttons; ++j ) {
presses += model.eval(vars[j]).get_numeral_uint();
}
return presses;
}
void
part2(const vector<Machine>& machines)
{
unsigned long count = 0;
for ( const auto& machine: machines ) {
count += simulate(machine);
}
cout << "Part 2: " << count << '\n';
}
} // namespace
int
main()
{
auto machines = read_file("data/day10.txt");
part2(machines);
}
|
