 Weighted formula utility representation

A finite rule base pairs propositional formulas with weights and sums the weights of the formulas satisfied by a Boolean valuation. Over a finite set $S$, associate one Boolean variable to membership of each element. Any utility function $u:2^S\to \mathbb{R}$ is represented by giving each subset's minterm weight $u(T)$. Exactly one rule fires at each valuation, so at most $2^{|S|}$ rules suffice. This bound counts rules, not the symbols required to write all formulas.

For computational questions, the weight encoding matters. Binary rational numbers permit exact addition and comparison in polynomial time; unrestricted real constants do not specify an ordinary finite input encoding.