אני מאוד אוהב את החידות של אריק ווסטל ב Advent Of Code ואת רובן פתרתי לפני שהיה AI והן עזרו לי ללמוד שפות תכנות חדשות. ואז המודלים נהיו מספיק טובים ואיבדתי מוטיבציה. אני רוצה לעצור ולשים לב מה בעצם קרה שם, איזה חלק מהחידות הפסיק לעניין, איזה חלק עדיין מעניין ומה זה אומר על לימודי תכנות בראייה קדימה.
נתחיל ברעיון הפשוט - הפרומפט הבא פתר לי את יום 10 של Advent Of Code בלי שכתבתי שורת קוד אחת. כאן יש את תיאור החידה:
https://adventofcode.com/2025/day/10
זה היה הפרומפט:
Solve
https://adventofcode.com/2025/day/10
for the demo input
[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
[...#.] (0,2,3,4) (2,3) (0,4) (0,1,2) (1,2,3,4) {7,5,12,7,2}
[.###.#] (0,1,2,3,4) (0,3,4) (0,1,2,4,5) (1,2) {10,11,11,5,10,5}
should yield 7
זה היה קימי בתוך קלוד קוד. הוא הגיע לתשובה הנכונה גם בקלט הבדיקה וגם על הקלט האמיתי. זה לבד מספיק בשביל להפוך את החידה ללא מאוד מעניינת. זה אגב הפתרון שהוא כתב:
import itertools
import re
def parse_machine(line):
"""Parse a line into (target_pattern, list_of_button_sets)"""
# Extract bracketed target pattern
target_match = re.search(r'\[([^\]]+)\]', line)
target = target_match.group(1)
# Extract parenthesized button schematics
buttons = []
for m in re.finditer(r'\(([^)]+)\)', line):
btn = tuple(int(x.strip()) for x in m.group(1).split(','))
buttons.append(btn)
return target, buttons
def solve_machine(target, buttons):
n = len(target)
goal = [1 if c == '#' else 0 for c in target]
best = float('inf')
# Try all subsets of buttons
for r in range(len(buttons) + 1):
for combo in itertools.combinations(range(len(buttons)), r):
state = [0] * n
for idx in combo:
for pos in buttons[idx]:
if 0 <= pos < n:
state[pos] ^= 1
if state == goal:
best = min(best, r)
break # for this r, all combos have same size r, so first match is optimal
if best != float('inf'):
break
return best if best != float('inf') else None
def main():
total = 0
unsolved = 0
with open('input.txt') as f:
for line_num, line in enumerate(f, 1):
line = line.strip()
if not line:
continue
target, buttons = parse_machine(line)
best = solve_machine(target, buttons)
if best is None:
print(f"Line {line_num}: NO SOLUTION")
unsolved += 1
else:
total += best
print(f"\nTotal minimum presses: {total}")
if unsolved:
print(f"Unsolved machines: {unsolved}")
if __name__ == '__main__':
main()
עכשיו מצד אחד אני רוצה להגיד לעצמי שלכתוב כזה פרומפט זה כמו להעתיק מהפתרון ועדיף לפתור לבד, אבל מצד שני אני יודע שזה לא מדויק. להעתיק מהפתרון זה בזבוז זמן כי שינוי הכי קטן בשאלה ואתה כבר לא יודע להתמודד איתה. לכתוב פרומפט זה ידע שממשיך אתך הלאה. לא משנה איזה שינוי יהיה בשאלה, הפרומפט יוכל לפתור אותה.
אבל זה לא כל הסיפור. כשאני פותח את קוד הפייתון שהמודל כתב אני רואה דרך פתרון אחת - פתרון Brute Force שרץ 2 בחזקת n פעמים. פה זה התחיל לעניין. האם אפשר לפתור את זה בפחות עבודה? מה המנגנון? איך כדאי לשמור את המידע?
בנוסף אחרי הפתרון מגיע החלק השני של השאלה ועכשיו יש עוד שאלות מעניינות - האם הפתרון של קלוד יכול להתמודד בשינויים לא גדולים עם החלק השני? האם היה אפשר לדמיין כיוון אחר שכן יצליח להתמודד עם החלק השני?
אז נכנסתי לעובי הקורה וראיתי איך הכפתורים והאורות בחידה ממופים למעשה למערכת משוואות. בעזרת קלוד למדתי שיש כלי בשם z3 שיודע לפתור אוטומטית מערכות משוואות או למצוא אופטימיזציות לפתרונות. התחלתי עם פתרון מונחה עצמים אבל מהר מאוד ראיתי ששום דבר לא משתנה ובסך הכל יש לנו אוביקטי מידע ופונקציות. בסוף הגעתי לקוד הזה ברובי:
LightDiagram = Data.define(:state, :buttons) do
# Convert diagram to a system of equations over GF(2) in z3 script syntax.
# Each bit position becomes an equation: XOR of buttons affecting that bit = target state.
# x0..xn are boolean variables (one per button), addition is XOR.
def to_z3
lines = []
buttons.each_with_index do |_, i|
lines << "(declare-const x#{i} Bool)"
end
state.each_with_index do |target, bit|
relevant = buttons.each_with_index.select { |btn, _| btn.bits.include?(bit) }
if relevant.empty?
# No button affects this bit — impossible if target is true
lines << "(assert false)" if target
else
terms = relevant.map { |_, i| "x#{i}" }.join(" ")
lines << "(assert (= (xor #{terms}) #{target}))"
end
end
lines.join("\n")
end
end
Button = Data.define(:bits)
def parse(filename)
diagrams = []
File.readlines(filename).each do |line|
line = line.strip
next if line.empty?
pattern = line[/\[(.*?)\]/, 1]
state = pattern.chars.map { |c| c == '#' }
buttons = []
line.scan(/\((.*?)\)/) do |match|
bits = match[0].split(",").map(&:to_i)
buttons << Button.new(bits:)
end
diagrams << LightDiagram.new(state:, buttons:)
end
diagrams
end
class Z3
def initialize(script)
@script = script
end
# Run z3 and return the raw model output (or nil if unsatisfiable)
def call
full_script = "(set-option :produce-models true)\n#{@script}\n(check-sat)\n(get-model)"
result = `echo '#{full_script}' | z3 -in`
return nil unless result.include?("sat")
result
end
# Return the minimum number of buttons that need to be pressed to satisfy all equations.
# Uses z3's optimization to minimize the count of true variables.
def size
n = @script.scan(/x(\d+)/).map(&:first).map(&:to_i).max
return 0 if n.nil?
n += 1 # number of variables is max index + 1
opt_script = "(set-option :produce-models true)\n#{@script}\n"
# Create integer cost variables: 1 if button pressed, 0 otherwise
n.times do |i|
opt_script += "(declare-const c#{i} Int)\n"
opt_script += "(assert (= c#{i} (ite x#{i} 1 0)))\n"
end
cost_vars = (0...n).map { |i| "c#{i}" }.join(" ")
opt_script += "(minimize (+ #{cost_vars}))\n"
opt_script += "(check-sat)\n(get-model)"
result = `echo '#{opt_script}' | z3 -in`
return nil unless result.include?("sat")
# Count how many x variables are true in the optimal model
count = 0
result.scan(/\(define-fun (x\d+) \(\) Bool\s+(true|false)\)/) do |_, val|
count += 1 if val == "true"
end
count
end
end
diagrams = parse('input.txt')
pp diagrams.sum { |diagram| Z3.new(diagram.to_z3).size }
הוא יותר ארוך כי הוא מייצר סקריפט ל z3 שיפתור את המשוואה אבל עבורי הוא גם יותר מסודר ובטח יותר מוכן לפתרון של החלק השני.
גם אם אני מבין את שני הפתרונות, רק אחד מהם אני בחרתי.
ב 2026 המציאות השתנתה. מה שמעניין הוא כבר לא "איך" כותבים את הקוד אלא "איזה" קוד כותבים. עוד נצטרך לגלות איך זה ישפיע על לימודי התכנות בעתיד.
