Rust
Finally got it, but had to use Z3. Getting Z3 to work was a real pain, they really need to doco the rust crate better.
I'll try redo it at some point without Z3, maybe after I forgot what a pain this was.
spoiler
struct Puzzle2 {
target: Vec<u16>,
buttons: Vec<Vec<u16>>,
}
fn solve_puzzle_z3(puzzle2: &Puzzle2) -> usize {
let optimiser = Optimize::new();
let num_presses: Vec<Int> = (0..puzzle2.buttons.len())
.map(|i| Int::new_const(format!("n_{i}")))
.collect();
num_presses.iter().for_each(|p| optimiser.assert(&p.ge(0)));
(0..puzzle2.target.len()).for_each(|i| {
let r = puzzle2.target[i];
let buttons = puzzle2
.buttons
.iter()
.enumerate()
.filter_map(|(j, b)| {
if b.contains(&(i as u16)) {
Some(&num_presses[j])
} else {
None
}
})
.collect::<Vec<&Int>>();
let sum = buttons.into_iter().sum::<Int>();
optimiser.assert(&sum.eq(r));
});
let all_presses = num_presses.iter().sum::<Int>();
optimiser.minimize(&all_presses);
if optimiser.check(&[]) != SatResult::Sat {panic!("Unsolvable")}
let model = optimiser
.get_model()
.expect("Optimizer should have a model if sat");
let t = model.eval(&all_presses, true).unwrap().as_i64().unwrap();
t as usize
}
#[test]
fn test_y2025_day10_part2() {
let input = include_str!("../../input/2025/day_10.txt");
let puzzles = input
.lines()
.map(|line| {
let parts = line.split(" ").collect::<Vec<_>>();
let display = parts.last().unwrap();
let display = display[1..display.len() - 1]
.split(',')
.map(|c| c.parse::<u16>().unwrap())
.collect::<Vec<u16>>();
let buttons = parts[1..parts.len() - 1]
.iter()
.map(|s| {
s[1..s.len() - 1]
.split(",")
.map(|s| s.parse::<u16>().unwrap())
.collect::<Vec<u16>>()
})
.collect::<Vec<Vec<u16>>>();
Puzzle2 {
target: display,
buttons,
}
})
.collect::<Vec<Puzzle2>>();
let mut min_presses = 0;
for puzzle in &puzzles {
min_presses += solve_puzzle_z3(puzzle)
}
println!("PRESSED: {}", min_presses);
}