1
$\begingroup$

There are a couple of weeks that I am trying to understand how I can eliminate/remove from the analysis some clauses in a propositional formula. For example, I have this formula:

$\phi_m = x \wedge (\neg y \vee x) \wedge (\neg x \vee y) \wedge (\neg c \vee x) \wedge (\neg d \vee x) \wedge (\neg a \vee y) \wedge (\neg b \vee y) \wedge (a \vee b \vee \neg y) $

I want to evaluate only those clauses that contain variables $\mathcal{Select} = \{y, a, b\}$, i.e., the $\phi_m$ becomes

$\phi_m' = (\neg y \vee x) \wedge (\neg x \vee y) \wedge (\neg a \vee y) \wedge (\neg b \vee y) \wedge (a \vee b \vee \neg y)$

As you can see, I keep the clauses as they are, I do not remove the other (not to be selected) variables if there is at least one variable in that clause that is required to be selected. E.g., the first 2 clauses contain the variable $x$ (not required to be selected) because those clauses contain the variable $y$ which is specified to be selected.

Well, till now, what I am doing is generating a new formula $\phi_m'$ by removing those clauses that do not have any variable specified in the $\mathcal{Select}$ set.

But, as I would like to operate in the same formula $\phi_m$, I tried to adapt the idea of assumptions, or selector variables. To apply this idea, I inserted a selector variable in each clause, as in the following (see the variables $\mathcal{A} = \{p, q, r, s, t, u, v, n\})$:

$\phi_m = (p \vee x) \wedge (q \vee \neg y \vee x) \wedge (r \vee \neg x \vee y) \wedge (s \vee \neg c \vee x) \wedge (t \vee \neg d \vee x) \wedge (u \vee \neg a \vee y) \wedge (v \vee \neg b \vee y) \wedge (n \vee a \vee b \vee \neg y) $

As I have understand, and tried in a solver so many times using the assumptions, when I assume that the selector variables from $\mathcal{A}$ are $false$ then those clauses are selected. Which is Cool. But, when I give any assumtion to $true$ and I analyse the generated models from the formula (and these models are very important for me, as they help me to analyse the semantics of my problems) then I get far more models as the other variables in the clause that is meant to be eliminated, they are becoming free (taking values $true$ and $false$).

For example, if I assume that the selector variable $s = true$ then the 4rth clause in $\phi_m$ insetad of becoming $TRUE$, the variables $\{c, x\}$ are still shown in my models and taking once with values $true$ then $false$.

Sorry, for a long explanation, but I need to know what I am missing when I want to apply the method of selector variables? Is there a way to really eliminate the clauses like commenting it, or removing physically as I am doing, while we use only a single formula $\phi_m$?

Thanks for any help, or references.

Edit.

I saw another method for eliminating the variables (not specifically clauses, as I have written here), using existential quantifications. For example, in your case (@Bram28 - most probably you know but just to demonstrate here), if we want to remove the variable B, then we quantify it with values $T$ for True then $F$ for False as in the following:

$\phi = (a \vee b) \wedge (\neg a \vee b) \wedge \neg b$

$\phi_{remove B}' = ((a \vee T) \wedge (\neg a \vee T) \wedge \neg T) \vee ((a \vee F) \wedge (\neg a \vee F) \wedge \neg F) $

$\phi_{remove B}' = F \vee (a \wedge \neg a \wedge T) = a \wedge \neg a$ which, in this case is UnSat, but just for demonstration.

Well, there are some reasons why I avoided this solution:

  • The formula is becoming twice longer, and should be iterated for each variable that has to be removed,

  • I am analyzing quite large formulas, and I wanted to analyze only excerpts of this large formula (let say in an incremental way!). The selected excerpts are really small parts of this large formula, so I wanted to select those relevant clauses instead of processing the whole formula to remove so many variables.

  • I wanted to keep the dependency of a selected variable with another unselected variable that is in the same clause. By removing clauses (not variables as with the existential quantifiers) I am still keeping a kind of dependency between the variables $A$ and $B$.

  • I am trying to avoid writing another algorithm, as I have then to measure still it's efficiency, and it's not my primary interest :( - that's why I started to use an existing solver.

$\endgroup$
0
$\begingroup$

I don't understand why you use this method of inserting 'selector variables' because, as you yourself point out, in doing so the clause set becomes trivially satisfiable by setting all those selector variables to true. And setting them to false will only remove them back out of the clause where you had just put them in. in other words: these selector variables seem to do absolutely no useful work for you!

On another note: I a, concerned that you are removing clauses from the clause set when they don't contain any of the variables you are interested in, because those clauses can of course still effect constrain the satisfiability of the original formula. To give a simple examplev, suppose you have the following formula:

$(A \lor B) \land (\neg A \lor B) \land \neg B$

And suppose you are only interested in the variable $A$. So then, if I understand you correctly, you would reduce this to:

$(A \lor B) \land ( \neg A \lor B)$

And that clause set is satisfiable, since you can set $B$ to true. But of course you could not have done that in the original clause set.

Maybe I am missing what you are trying to do here, but I am just concerned that you are removing clauses. Here is an amended example without any single literal clauses:

$(A \lor B) \land (\neg A \lor B) \land (\neg B \lor C) \land (\neg B \lor \neg C)$

So, in general it is not a good idea to cut clauses, even if they are clauses that are not directly related to the variables you are really interested in ... because they can have an indirect effect on those variables nevertheless!

OK, so what can you do to try and simplify things?

Well, let's take your original formula again:

$\phi_m = x \wedge (\neg y \vee x) \wedge (\neg x \vee y) \wedge (\neg c \vee x) \wedge (\neg d \vee x) \wedge (\neg a \vee y) \wedge (\neg b \vee y) \wedge (a \vee b \vee \neg y) $

Now, rather than throwing out the $x$ clause since $x \not \in Select$, you can in fact make great use of this $x$, because given that $x$ has to be true, that means that every other clause that contains $x$ is automatically satisfied as well (and can thus be removed .. this is an instance of Subsumption Elimination), and for very clause that contains $\neg x$: since $\neg x$ is false, one of the other literals in the clause must be satisfied, meaning that effectively we can remove the $\neg x$ from that clause.

(logically: $x \land (\neg x \lor y) \Leftrightarrow x \land y)

In general: when we reduce a clause set with regard to some literal $x$, we remove all the clauses containing $x$, and we remove all the instances of $\neg x$

So, applied to this formula, we can immediately reduce it with regard to $x$, which leaves us with:

$\phi_m' = y \wedge(\neg a \vee y) \wedge (\neg b \vee y) \wedge (a \vee b \vee \neg y) $ ($x$)

OK, but now we have $y$ as a unit clause, so we can reduce with regard to $y$:

$\phi_m'' = a \vee b $ ($x, y$)

... and that's about as you can get: we now know that $x$ and $y$ are forced to be true, and other than that either $a$ or $b$ needs to be true.

$\endgroup$
  • $\begingroup$ Yes, you have understood it well. I wrote some explanation (see the Edit, up) about the reason why I am removing the clauses. Actually, till now, in all kind of test that I have done, it's well functioning to remove the clauses. But, I have to say that I am really keeping the single literal clauses! I discovered, that I have to keep them to save the semantics of my problem. Thank you, for mentioning/highlighting this thing. Otherwise, I don't know if there is another reason why I should be aware of not removing the clauses! ? $\endgroup$ – user4712458 Feb 16 '17 at 14:22
  • $\begingroup$ @user4712458 Notice that my example also involved a single literal clause ($\neg B$) that should be kept. But, in general, with more complex formulas, you can easily run into scenarios where you really can't theow away any clauses. Let me add an example of that to my post. $\endgroup$ – Bram28 Feb 16 '17 at 14:53
  • $\begingroup$ Yep, I get your point. I can say that, if this happens then it is fine to process the whole formula once or few times (only when the variables like B, that appear in most of the clauses, has to be selected). But, in other cases, e.g., when I have to select the clauses that contain C then only the last 2 clauses are analysed, or similarly with the A. I am not saying that is the ideal solution, and I am not insisting to use only this, that's why I am here :), asking if there is another way of analysing a big formula by analysing a relevant subset of its clauses or variables? $\endgroup$ – user4712458 Feb 16 '17 at 15:11
  • $\begingroup$ @user4712458 There are some basic elimination strategies like tautology elimination, subsumptin elimination, and pure literal elimnation .. Are you familiar with those? Also, you can use a Davis Putnam strategy of splitting on any literal. $\endgroup$ – Bram28 Feb 17 '17 at 2:23
  • $\begingroup$ I didn't know about these elimination strategies. I checked the first three...their applicability is slightly different. I am trying to think if I can find useful any of them, because, in my understanding, they are more focused in how to solve quicker a formula by simplifying it first. While, in my case, I just want to have the right to cut a formula and to analyse it, where the truth values of this small formula will be the truth values (subset) even when I analyse the whole formula (in the whole set). Thanks a lot, btw, for mentioning them. $\endgroup$ – user4712458 Feb 17 '17 at 10:39

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.