From e8bdb4f2ddb1a5137ecbfbe528f40c1cd253df17 Mon Sep 17 00:00:00 2001
From: Thomas Schmucker <ts@its1.de>
Date: Wed, 10 Dec 2025 21:01:19 +0100
Subject: aoc 2025, day 10, part 2

---
 2025/src/day10p2.cpp | 159 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 159 insertions(+)
 create mode 100644 2025/src/day10p2.cpp

(limited to '2025/src/day10p2.cpp')

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);
+}
-- 
cgit v1.3