Z3Py 例題 コイン問題２ - Qiita

from z3 import * coin__2cent = Int("coin__2cent") coin__5cent = Int("coin__5cent") coin_10cent = Int("coin_10cent") coin_20cent = Int("coin_20cent") s = Solver() s.add(And(0 <= coin__2cent, coin__2cent <= 4)) s.add(And(0 <= coin__5cent, coin__5cent <= 4)) s.add(And(0 <= coin_10cent, coin_10cent <= 4)) s.add(And(0 <= coin_20cent, coin_20cent <= 4)) s.add(2*coin__2cent + 5*coin__5cent + 10*coin_10ce