#!/usr/bin/env python # coding: utf-8 # In[4]: import import_ipynb import helper f = helper.open_file('2021_8.txt') c = 0 for l in f: l = l.strip() examples, output = l.split(' | ') digits = output.split() for digit in digits: if len(digit) in (2, 3, 4, 7): c += 1 print(c) # In[5]: from z3 import * # In[7]: x = Real('x') y = Real('y') z = Real('z') s = Solver() s.add(3*x + 2*y - z == 1) s.add(2*x - 2*y + 4*z == -2) s.add(-x + 0.5*y - z == 0) print(s.check()) print(s.model()) # In[ ]: