Challenge
|
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 |
--- Day 7: Some Assembly Required --- This year, Santa brought little Bobby Tables a set of wires and bitwise logic gates! Unfortunately, little Bobby is a little under the recommended age range, and he needs help assembling the circuit. Each wire has an identifier (some lowercase letters) and can carry a 16-bit signal (a number from 0 to 65535). A signal is provided to each wire by a gate, another wire, or some specific value. Each wire can only get a signal from one source, but can provide its signal to multiple destinations. A gate provides no signal until all of its inputs have a signal. The included instructions booklet describes how to connect the parts together: x AND y -> z means to connect wires x and y to an AND gate, and then connect its output to wire z. For example: 123 -> x means that the signal 123 is provided to wire x. x AND y -> z means that the bitwise AND of wire x and wire y is provided to wire z. p LSHIFT 2 -> q means that the value from wire p is left-shifted by 2 and then provided to wire q. NOT e -> f means that the bitwise complement of the value from wire e is provided to wire f. Other possible gates include OR (bitwise OR) and RSHIFT (right-shift). If, for some reason, you'd like to emulate the circuit instead, almost all programming languages (for example, C, JavaScript, or Python) provide operators for these gates. For example, here is a simple circuit: 123 -> x 456 -> y x AND y -> d x OR y -> e x LSHIFT 2 -> f y RSHIFT 2 -> g NOT x -> h NOT y -> i After it is run, these are the signals on the wires: d: 72 e: 507 f: 492 g: 114 h: 65412 i: 65079 x: 123 y: 456 In little Bobby's kit's instructions booklet (provided as your puzzle input), what signal is ultimately provided to wire a? |
Solution
Wow this one was fun! I decided to use Z3Py, a theorem prover module for python. My solution essentially parses each command using regexp and adds the various boolean rules to a solver object. Finally, the theorem solver checks all possible values and prints out the results of every ‘wire’. Determining the answer is then very simple. To solve part 2 I simply changed the value of b in my input.txt to the answer from part a and reran the script.
|
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 |
# Day 7 - Part 1 and Part 2 # # To find Part 1 answer: python day7.py | grep ' a = ' # To find Part 2 answer: Edit value of b in input.txt to result from part 1 and rerun script import re from z3 import * z3Vars = {} s = Solver() with open('input.txt') as f: lines = f.readlines() for line in lines: # Get command -> store variables res = re.search(r'(.*)\s*->\s*(.*)', line) command, store_var = res.group(1).strip(), res.group(2) # Store var if store_var not in z3Vars: z3Vars[store_var] = BitVec(store_var, 32) #32 bit integers # Add logical constraints to solver # Store other variables in commands if they don't exit on the way # Assign operation (integer) == res = re.search(r'^(\d*?)$', command) if res and res.group(1) != '': s.add(z3Vars[store_var] == res.group(1)) continue # Bitwise AND (with integer) res = re.search(r'(\d*)\s*AND\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(2) not in z3Vars: z3Vars[res.group(2)] = BitVec(res.group(2), 32) s.add(z3Vars[store_var] == int(res.group(1)) & z3Vars[res.group(2)]) continue # Bitwise AND res = re.search(r'(.*?)\s*AND\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) if res.group(2) not in z3Vars: z3Vars[res.group(2)] = BitVec(res.group(2), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] & z3Vars[res.group(2)]) continue # Bitwise OR res = re.search(r'(.*?)\s*OR\s*(.*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) if res.group(2) not in z3Vars: z3Vars[res.group(2)] = BitVec(res.group(2), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] | z3Vars[res.group(2)]) continue # Bit LSHIFT res = re.search(r'(.*?)\s*LSHIFT\s*(\d*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] << int(res.group(2))) continue # Bit RSHIFT res = re.search(r'(.*?)\s*RSHIFT\s*(\d*)', command) if res and res.group(1) != '' and res.group(2) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)] >> int(res.group(2))) continue # Bitwise NOT res = re.search(r'NOT\s*(.*)', command) if res and res.group(1) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == (~z3Vars[res.group(1)]) & 0xFFFF ) # 0xFFFF logical and to contrain value to [0, 2^16) continue # Assign operation (variable) == res = re.search(r'(.*)', command) if res and res.group(1) != '': if res.group(1) not in z3Vars: z3Vars[res.group(1)] = BitVec(res.group(1), 32) s.add(z3Vars[store_var] == z3Vars[res.group(1)]) continue # Print answers set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000) print(s.check()) print(s.model()) |
