Fast Consequence FInders
Updated answer, based upon the revised question:

It sounds like resolution does exactly what you want, so I suggest you implement the resolution algorithm (combined with a subsumption test). Implementing this is a straightforward programming exercise which should take you only a few hours.



Original answer to an earlier version of the question:

I don't know if there are any dedicated solvers aimed at solving this problem, but one "poor man's approach" might be to implement this using an off-the-shelf SAT solver.  The approach will depend on what you are looking for: in particular, from what space consequences are allowed to come from.

A useful building block

Let me first observe that you can use a SAT solver to determine whether a candidate clause is indeed a consequence or not.  This will be a useful building block below.

Suppose $\varphi(x)$ is a formula, on boolean variables $x=(x_1,\dots,x_n)$.  Let $c(x)$ be a clause.  You can easily use a SAT solver to test whether $c(x)$ is a consequence of $\varphi(x)$.  In particular, you test whether $\varphi(x) \land \neg c(x)$ is satisfiable; if it is satisfiable, $c(x)$ is not a consequence, otherwise $c(x)$ is a consequence.

Finding consequences that are conjunctions of literals

If you want each consequence to be a conjunction of literals, you can find the minimal consequence using a SAT solver.  In particular, it suffices to use dumb search.  Focus on clauses that contain a single literal; there are only $2n$ possibilities for them.  Test each of them to see which ones are consequences (if any); this requires $2n$ invocations of the SAT solver.  In other words, for each variable $x_i$, test whether $x_i$ is a consequence, and also test whether $\neg x_i$ is a consequence.

Now you have a bunch of consequences, say the literals $\ell_1,\dots,\ell_m$.  Then $\ell_1 \land \dots \land \ell_m$ is also a consequence -- and it turns out it is the minimal consequence (minimal, among the space of conjunctions of literals).  This procedure requires $O(n)$ invocations of the SAT solver, so it should be pretty efficient.

Finding consequences that are disjunctions of literals

If you want to consequences to be disjunctions of literals, it's also possible to find all minimal consequences (minimal, among the set of disjunctions of literals), though it is somewhat more complex.  Let me build up the ideas step-by-step:


Finding a single consequence. You can use a SAT solver to find a single consequence of $\varphi(x)$ (not necessarily a minimal consequence).  Feed $\neg \varphi(x)$ to the SAT solver, and let it find a satisfying assignment, say $x=\alpha$.  Then from this it is possible to identify a consequence (not necessarily minimal) of $\varphi(x)$.  In particular, the clause $x\ne \alpha$ is a consequence of $\varphi(x)$.  To put it another way, consider the clause $c(x) = \ell_1 \lor \dots \lor \ell_n$, where $\ell_i$ is either $x_i$ or $\neg x_i$ according to whether $\alpha_i$ is false or true; then $c(x)$ is a consequence of $\varphi(x)$.  This is a somewhat trivial and boring consequence, but it is a valid one.
Finding a minimal consequence. Once you have a single consequence $c(x)= \ell_1 \lor \dots \lor \ell_n$, it is now possible to to minimize it.  In particular, we will look for a minimal subset $S \subseteq \{1,2,\dots,n\}$ such that $c_I(x) = \lor_{i \in I} \ell_i$ is a consequence of $\varphi(x)$.  How do we do that?  We can simply try removing one literal at a time from $c(x)$ (removing one index at a time from the set $I$), testing at each step whether the result remains a valid consequence.  If removing a literal from the disjunction leaves it a valid consequence, go ahead and remove that literal; if after removal, it is no longer a valid consequence, then don't remove it.  Each test requires a single invocation to the SAT solver, so this procedure requires $n$ invocations of the SAT solver.  When you are done, you have a single minimal consequence $c_1(x)$ of $\varphi(x)$.
Finding another consequence.  Next, I will show to find a second consequence.  Let me explain using an example.  Suppose that $c^1(x) = x_1 \lor \neg x_3 \lor x_7$ (say), and suppose we know that $c^1(x)$ is a minimal consequence: no literal can be removed from this disjunction while keeping it a consequence.  We want to find a second minimal consequence $c^2(x)$ that is a disjunction of literals.  What can we say about the set of literals that appear in $c^2(x)$?  Well, either $c^2(x)$ does not contain the literal $x_1$, or it does not contain the literal $\neg x_3$, or it does not contain the literal $x_7$ (otherwise it would be a consequence of $c^1(x)$, i.e., subsumed, and thus not minimal).

So let's search for some consequence that satisfies these constraints.  One way to do this is to search for a satisfying assignment to $\neg \varphi(x) \land (\neg x_1 \lor x_3 \lor \neg x_7)$, by feeding this to a SAT solver.  Suppose the SAT solver gives us a satisfying assignment $x=\alpha$.  Then this immediately suggests a consequence that is not subsumed by $c_1(x)$, namely, the clause $x\ne \alpha$ (expressed as a disjunction of literals).  If we want, we can minimize this consequence to get a minimal consequence $c^2(x)$.  By construction, $c^2(x)$ will be minimal and different from $c^1(x)$.  This gives us a way to find two minimal consequences.
Finding all minimal consequences. Now it should be clear how to find all minimal consequences.  Suppose we have found $c^1(x),\dots,c^k(x)$, each of which is a minimal consequence of $\varphi(x)$, where $c^j(x) = \lor_i \ell^j_i$.  We define the formula

$$\neg \varphi(x) \land (\lor_i \neg \ell^1_i) \land \cdots \land (\lor_i \neg \ell^k_i).$$

Feed this formula to a SAT solver.  If it is unsatisfiable, you are done: you have found all minimal consequences.  Otherwise, suppose it finds a satisfying assignment, say $x=\alpha$.  Then this immediately supplies a  new consequence, which you can then minimize as above, to get a new minimal consequence $c^{k+1}(x)$.  Now you can iterate until there are no more to be found.


The running time for this algorithm is best expressed in an output-sensitive measure. If there are $m$ minimal consequence clauses, then this algorithm will complete after making $O(mn)$ queries to the SAT solver.  It might even be somewhat efficient, if you use a SAT solver that allows you to make multiple related queries and that remembers state across those queries.

Finding consequences that are in CNF form

Now suppose you want to allow consequences to be any CNF formula, and you want consequences that are minimal among the set of such consequences.  Then the problem becomes trivial.

In particular, $\varphi(x)$ is a trivial consequence of $\varphi(x)$, and it is possible to show that it is a minimal consequence: any other formula that has the same or more satisfying assignments is subsumed by it, and any formula that has fewer satisfying assignments is not a consequence.

A comment on resolution and on formulating problem statements

Resolution is just a means to an end, not an end goal in itself.  Resolution is one technique that is used in some SAT solvers, but SAT solvers also use other techniques as well -- and that combination of techniques is important.  What we've seen in practice is that current SAT solvers perform a lot better than vanilla resolution on many problems.

Therefore, my advice to you is to articulate the problem statement clearly, and try to keep clear in your mind the distinction between the goal (the problem statement) vs the way you'll achieve the goal (the algorithm you use).  Formulate the goal in a way that describes what you want to achieve, not how you want it to be achieved.  Once you articulate your goal clearly, you might find that resolution is not the optimal method.