title: SAT ‒ set maximal number of variables to true
body: <p>I wish to solve the following SAT-related problem, preferably using Z3 or some other freely available solver:</p>
  <p>Given a set of formulae of predicate logic (without quantifiers or negation) over a set of Boolean variables, find the maximal subset of the variables, such that if <code>true</code> is assigned precisely to all variables in this subset, all the formulae are satisfied. The formulae are all of the form <code>variable =&gt; CNF-formula</code>.</p>
  <p>Generally, I want to find an &quot;optimal&quot; solution to the classical SAT problem, which is the valuation assigning <code>true</code> to the most variables possible.</p>