You're looking for a mixed integer programming solver. Although the problem is NP-hard, in practice, state of the art MIP solvers run much faster than brute force search in most non-pathological cases.

Are SMT solvers insufficient?

Mixed integer programming is a more specialized task than SMT solving, therefore an MIP implementation is likely to be more optimized for the task, even if you might be able to use an SMT solver to solve the same problem. Moreover, SMT solvers are focused on finding some solution to some constraints, whereas MIP solvers are focused on finding the best solution to the constraints according to some linear objective. Finally, an SMT solver is basically a SAT solver combined with a theory solver for reasoning about integers, etc. If the problem can be expressed just as a conjunction of constraints (i.e, it has no interesting propositional structure), then you don’t really need the SAT solver part and can just use a specialized theory solver (optimizer, in this case) directly.

Like the comment above yours says there are algorithms for SSP that are polynomial in the target value of the sum. For values on the order of something someone would buy with a credit card I think they should be practical.

See: https://en.wikipedia.org/wiki/Subset_sum_problem#Pseudo-poly...

The problem only becomes really difficult when the numbers are so large that it takes a large number of bits to represent them.

The secret solution is called Z3.

This? https://github.com/z3prover/z3

What is secret about it?

That sounds like an interesting problem. Would love to know more of the contraints.

It's for reconciling customers' items such as point of sale, payroll, and other systems with bank transactions. Each client item has date, description, and amount. Each transaction similarly has date, description and amount. The goal is to match all items with corresponding bank transactions. However, it is more complicated because: * bank dates and item dates may not be the same. A sale may take a few days to clear the bank. * amounts may not be the same. A credit card sale may be for 100, but when it clears the bank, the CC provider has deducted fees, so it's 98. * quantities may not be the same. Ten sales may be deposited as one deposit. In some cases, multiple items may match to multiple transactions. * there are rules about which matches are best. A sale may match ten transactions, but it can be important to match the right one, typically the closest date.

As others have suggested, I can take shortcuts by ignoring some sets. But it is tricky and slow, especially for large sets.