Weighted SAT: is this a known problem? Given an arbitrary SAT instance, I would like to find the solution with the minimum weight. The weight of a valid assignment is computed using a function.

Is this a known problem or are there other problems that I can reduce this one to?
If the function is linear, then you can reduce to MaxSAT. Then there are some related formalisms like pseudo-boolean optimizatin (PBO) or integer linear programming (ILP).