I have ~4000 variables that are used in ~5000 logical formulas, where each formula consists only of conjunctions of the (non-negated) variables. I want to find the maximum number of satisfied formulas, given the number of variables that I can set to 1.
Does this problem have a name? Is it equivalent to the MAX-SAT problem? Which algorithm would be applicable to solve it exactly or using heuristics?