אני מאוד אוהב את החידות של אריק ווסטל ב 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 המציאות השתנתה. מה שמעניין הוא כבר לא "איך" כותבים את הקוד אלא "איזה" קוד כותבים. עוד נצטרך לגלות איך זה ישפיע על לימודי התכנות בעתיד.