|
| 1 | +use std::str::FromStr; |
| 2 | + |
| 3 | +use z3::ast::Int; |
| 4 | +use z3::*; |
| 5 | + |
| 6 | +use aoc_derive::aoc_main; |
| 7 | +use itertools::Itertools; |
| 8 | +use lazy_regex::regex; |
| 9 | +use utils::{ |
| 10 | + graphs::{UnweightedGraph, bfs}, |
| 11 | + *, |
| 12 | +}; |
| 13 | + |
| 14 | +#[derive(Debug, Clone)] |
| 15 | +struct Machine { |
| 16 | + target_bitmask: usize, |
| 17 | + buttons: Vec<Vec<usize>>, |
| 18 | + target_joltages: Vec<usize>, |
| 19 | +} |
| 20 | + |
| 21 | +impl Machine { |
| 22 | + fn solve(&self) -> usize { |
| 23 | + bfs(self, 0_usize, self.target_bitmask).distance.unwrap() |
| 24 | + } |
| 25 | + |
| 26 | + fn solve_part2(&self) -> usize { |
| 27 | + let matrix = (0..self.target_joltages.len()) |
| 28 | + .map(|idx| { |
| 29 | + self.buttons |
| 30 | + .iter() |
| 31 | + .map(|buttons| if buttons.contains(&idx) { 1 } else { 0 }) |
| 32 | + .collect_vec() |
| 33 | + }) |
| 34 | + .collect_vec(); |
| 35 | + |
| 36 | + let opt = Optimize::new(); |
| 37 | + |
| 38 | + let num_presses = |
| 39 | + (0..self.buttons.len()).map(|i| Int::new_const(format!("x_{}", i))).collect_vec(); |
| 40 | + |
| 41 | + for x in &num_presses { |
| 42 | + opt.assert(&x.ge(Int::from_i64(0))); |
| 43 | + } |
| 44 | + |
| 45 | + // Hand-written Matrix-vector product: matrix * x = target_joltages |
| 46 | + for (row, target_joltage) in matrix.iter().zip(self.target_joltages.iter()) { |
| 47 | + let sum = row |
| 48 | + .iter() |
| 49 | + .zip(num_presses.iter()) |
| 50 | + .map(|(&presses, target_joltage)| presses * target_joltage) |
| 51 | + .sum::<Int>(); |
| 52 | + opt.assert(&sum.eq(Int::from(*target_joltage as i64))); |
| 53 | + } |
| 54 | + |
| 55 | + opt.minimize(&num_presses.iter().sum::<Int>()); |
| 56 | + |
| 57 | + // Solve |
| 58 | + match opt.check(&[]) { |
| 59 | + SatResult::Sat => { |
| 60 | + let model = opt.get_model().unwrap(); |
| 61 | + num_presses |
| 62 | + .iter() |
| 63 | + .map(|var| model.eval(var, true).unwrap().as_i64().unwrap()) |
| 64 | + .sum_usize() |
| 65 | + } |
| 66 | + _ => panic!(), |
| 67 | + } |
| 68 | + } |
| 69 | +} |
| 70 | + |
| 71 | +impl UnweightedGraph for Machine { |
| 72 | + type Node = usize; |
| 73 | + |
| 74 | + fn neighbors<'a, 'b: 'a>( |
| 75 | + &'a self, |
| 76 | + node: &'b Self::Node, |
| 77 | + ) -> impl Iterator<Item = Self::Node> + 'a { |
| 78 | + self.buttons |
| 79 | + .iter() |
| 80 | + .map(|buttons| buttons.iter().fold(*node, |next, &idx| next ^ (1 << idx))) |
| 81 | + } |
| 82 | +} |
| 83 | + |
| 84 | +impl FromStr for Machine { |
| 85 | + type Err = (); |
| 86 | + |
| 87 | + fn from_str(s: &str) -> Result<Self, Self::Err> { |
| 88 | + let (target, buttons, joltages) = regex!(r#"\[(.*)\] (.*) \{(.*)\}"#).capture_into_tuple(s); |
| 89 | + |
| 90 | + let target_bitmask = target |
| 91 | + .chars() |
| 92 | + .enumerate() |
| 93 | + .fold(0, |val, (i, c)| if c == '#' { val ^ (1 << i) } else { val }); |
| 94 | + |
| 95 | + let buttons = |
| 96 | + buttons.split_whitespace().map(|s| extract_numbers(s).collect_vec()).collect_vec(); |
| 97 | + let target_joltages = extract_numbers(joltages).collect_vec(); |
| 98 | + |
| 99 | + Ok(Self { target_bitmask, buttons, target_joltages }) |
| 100 | + } |
| 101 | +} |
| 102 | + |
| 103 | +#[aoc_main] |
| 104 | +fn solve(input: Input) -> impl Into<Solution> { |
| 105 | + let machines = input.lines().flat_map(Machine::from_str); |
| 106 | + |
| 107 | + (machines.clone().map(|m| m.solve()).sum_usize(), machines.map(|m| m.solve_part2()).sum_usize()) |
| 108 | +} |
| 109 | + |
| 110 | +#[cfg(test)] |
| 111 | +mod tests { |
| 112 | + use super::*; |
| 113 | + #[test] |
| 114 | + fn test_examples() { |
| 115 | + use utils::assert_example; |
| 116 | + assert_example!( |
| 117 | + r#" |
| 118 | +[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7} |
| 119 | +[...#.] (0,2,3,4) (2,3) (0,4) (0,1,2) (1,2,3,4) {7,5,12,7,2} |
| 120 | +[.###.#] (0,1,2,3,4) (0,3,4) (0,1,2,4,5) (1,2) {10,11,11,5,10,5} |
| 121 | +"#, |
| 122 | + 7, |
| 123 | + 33 |
| 124 | + ); |
| 125 | + } |
| 126 | +} |
0 commit comments