aoc 2025, day 10, part 2

2 files changed, 162 insertions, 0 deletions

diff --git a/2025/src/day10p2.cpp b/2025/src/day10p2.cpp
new file mode 100644
index 0000000..a011bd3
--- /dev/null
+++ b/2025/src/day10p2.cpp
@@ -0,0 +1,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);
+}
diff --git a/makefile b/makefile
index 634c220..536ac76 100644
--- a/makefile
+++ b/makefile
@@ -62,6 +62,9 @@ all: $(patsubst 2015/src/%.cpp,2015/bin/%,$(wildcard 2015/src/*.cpp)) \
 2025/bin/%: 2025/src/%.cpp | 2025/bin
         c++ $(CPPFLAGS) $^ -o $@
 
+2025/bin/day10p2: 2025/src/day10p2.cpp | 2025/bin
+        c++ $(CPPFLAGS) -Wno-sign-conversion $^ -lz3 -o $@
+
 clean:
         rm -rf 2015/bin 2016/bin 2017/bin 2020/bin 2022/bin 2023/bin 2024/bin 2025/bin