1
$\begingroup$

I have been struggling in the search for a modern fast "consequence finder". That is, an implementation based on state-of-the-art theory; things of the ilk of Z3, Prover9, OTTER, etc.

To describe what I mean by "consequence finding" (and please correct my term usage if it's inappropriate):

Given a satisfiable and consistent set of clauses C, where a clause is a finite disjuction of literals, wherever there is some atom $p$ in some clause $\phi = p \lor \alpha$ and $\lnot p$ in some clause $\psi = \lnot p \lor \beta$, we add the new clause $\alpha \lor \beta$ to C (provided it cannot already be found in C). This is what I understand as the process of performing Resolution.

Assuming we generate all possible new clauses from C, contintually adding generated clauses, and trying to find new clauses again, we will have C'.

As a very small example, on the input:

$(\lnot p \lor q) \land (p \lor r)$

$(\lnot p \lor q) \land (p \lor r) \land (q \lor r)$ would be the output.

If we now remove subsumed clauses from C', i.e. clauses which are of the form $\alpha \lor \beta$ where there exists some other clause of the form $\alpha$, then we have a set of clauses C''.

I want C''. I was under the impression that there would be tools like those mentioned to generate this set since C'' is essentially what would remain when having performed vanilla resolution on a satisfiable set of clauses.

$\endgroup$
3
  • $\begingroup$ Thanks, that's much clearer. 1. Basically, you are saying you want an algorithm to do resolution. So why don't you just use the resolution algorithm, then? Implementing vanilla resolution is a straightforward programming exercise which should take you only a few hours. (If you're looking just for a tool recommendation -- a program that already implements this -- that's not a good fit for this site.) $\endgroup$ – D.W. May 24 '14 at 19:01
  • $\begingroup$ 2. You have defined the problem statement in terms of a specific algorithm (i.e., resolution), rather than in terms of any semantic requirement. Generally speaking, my experience is that it is better to give problem statements that are independent of any particular algorithm, and that specify the semantic properties of the output (rather than how it should be generated): specify what you want, not how you want it to be computed. $\endgroup$ – D.W. May 24 '14 at 19:01
  • $\begingroup$ @D.W. I thank you for your answer, and it is good... but, the reason I sought a tool is because I thought that modern theory might have yielded some popular implementation in something like Z3. e.g. There may be some trick or shortcut in the subsumption or some trick in the resolution step itself. $\endgroup$ – d'alar'cop May 25 '14 at 14:09
2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ @d'alar'cop, I've edited my answer substantially. A comment: I find it not clear what you are looking for. Your question & comments seem to conflate what you want to achieve (e.g., finding all minimal consequences) vs how it can be achieved (e.g., resolution). Resolution is just a means to an end, not a goal in itself (it's an algorithmic technique, not a problem statement). If your problem statement refers to resolution, then there's something wrong with the problem statement -- a good problem statement should not make assumptions about the best way to solve the problem. $\endgroup$ – D.W. May 21 '14 at 18:24
  • $\begingroup$ Yes, your comment is totally fair. I don't care so much about the method. I only mentioned Resolution as a means to illustrate what I thought I wanted. $\endgroup$ – d'alar'cop May 22 '14 at 6:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.