knapsack_z3.py

import fileinput
import z3
import sys

def solve(sizes, prices, capacity):
	coeffs = list()
	solver = z3.Optimize()
	price = 0
	weight = 0
	
	for i in range(len(sizes)):
		coeff = z3.Int(f'c_{i}')
		coeffs.append(coeff)
		solver.add(z3.Or(coeff == 0, coeff == 1))
		price += coeff * prices[i]
		weight += coeff * sizes[i]
			
	solver.add(weight <= capacity)	
	solver.maximize(price)
	if solver.check() == z3.sat:
		m = solver.model()
		total_weight = m.eval(weight).as_long()
		total_price = m.eval(price).as_long()
		indices = [i + 1 for i, c in enumerate(coeffs) if m.eval(c).as_long()]
		return (total_weight, total_price, indices)
	else:
		print("error")
		return None

def parse_input():
	sizes = []
	prices = []
	capacity = None
	approximation = None
	for line in fileinput.input():
		line = line.strip("\n")
		if not len(line):
			continue
		try:
			if approximation is None:
				approximation = float(line)
			elif capacity is None:
				capacity = int(line)	
			else:
				(s,p) = map(int,line.split())
				if s<0 or p<0:
					raise Exception("negative")
				sizes.append(s)
				prices.append(p)		
		except:
			print("error")	

	if not len(prices):
		print("0 0")
		sys.exit(0)
	return sizes, prices, capacity	

sizes, prices, capacity = parse_input()
total_weight, total_price, indices = solve(sizes, prices, capacity)
print(f"{total_weight} {total_price}")
for i in indices:
	print(i)

sample_input.txt

0.001
165
23 92
31 57
29 49
44 68
53 60
38 43
63 67
85 84
89 87
82 72