Unsat core and clause assumptions

[Hao Zheng]

I am not sure if my two questions have been answered before, but any pointers would be highly appreciated.

I am developing a model checker that relies on the incremental sat solving. Clauses need to pushed and popped frequently. Minisat supports assumptions using unit clauses. Is there a way to allow general clauses to be used as a part of an assumption?

When an assumption consists of unit clauses, is there a way to extract an unsat core to identify which unit clauses in the assumptions are included in the unsat core? From a model checking paper in FMCAD 2011, the authors suggested they modified the minisat for that purpose. Can anyone shed some light on how to do it?

Thanks,

Hao

[Andreas Morgenstern]

Hello,

Am Sonntag, 3. Februar 2013 19:16:44 UTC+1 schrieb Hao Zheng:

I am not sure if my two questions have been answered before, but any pointers would be highly appreciated.

I am developing a model checker that relies on the incremental sat solving. Clauses need to pushed and popped frequently. Minisat supports assumptions using unit clauses. Is there a way to allow general clauses to be used as a part of an assumption?

No, there is no such mechanism. However, what you can do is to use an activation literal. Suppose you want to use a clause C=[c_0,c_1,...,c_n] as a (temporary) assumption.
You generate a new variable v to generate an activation literal l=v. Then you add the clause C'=[!l, c_0,c_1,...,c_n]. Whenever you want to use clause C as an assumption, you add the literal l as part of the assumption.
 

When an assumption consists of unit clauses, is there a way to extract an unsat core to identify which unit clauses in the assumptions are included in the unsat core?

Not really a minimal unsat core, but something similar. When you look at the conflict, this gives you a (subset) of the assumptions that has been used to derive the UNSAT-result.
It gives you quite good results, meaning that typically the conflict is quite small.
 

Andreas

[Hao Zheng]

Andreas,

Thanks a lot for the reply. For the method using activation variables, I am curious if the dead clauses in the sat solver due to the activation variables would affect the performance of solving?

Thanks,

H

[Mate Soos]

Hi Hao,

On 03/06/2013 12:54 AM, Hao Zheng wrote:
> Thanks a lot for the reply. For the method using activation variables, I am curious if the dead clauses in the sat solver due to the activation variables would affect the performance of solving?

In short: yes, very much. So try to use as few activation variables as
possible: remember that one activation variable can activate more than
one clause, so you can activate groups of clauses. If it's slow you may
try to run more than one instance, and set (not assume) the variables.
It sounds like doing the same job multiple times but after a while the
overhead is so large that it's actually faster.I believe there was a
presentation last year at SAT'12 about too many assumptions slowing down
the solver too much. Flexibility costs.

Cheers,

Mate

[Niklas Sörensson]

Hi all,

Sorry for contradicting you Mate, but if the question is whether dead clauses hurt performance I'd say no. They are garbage collected periodically and shouldn't be too much in the way. Maybe you are thinking about the activation variables that can accumulate and use up too much "index-space"? That is indeed a problem, and some time ago I introduced a simple feature in MiniSat that allows reusing this type of throw-away variables with a short life-span:

    void    releaseVar(Lit l);                                  // Make literal true and promise to never refer to variable again.

Here's how it can be used for activation literals: (beware of untested code)

   Solver    solver;            // Solver context

   vec<Lit> local_clause;  // Some clause we want to use temporarily

   Lit          activate = mkLit(solver.newVar()); // Fresh activation literal

   local_clause.push(~activate);

   solver.addClause(local_clause);

   solver.solve(activate); // some solve-call that activates the local clause

   // when we don't need the local clause any more we can release the activation variable:

   solver.releaseVar(~activate);

Note that releaseVar(~activate) has the same observable effect as just assigning the literal 'activate' to false. This deactivates the local clause, and since the caller at the same time promises to never refer to that variable again it can be reused in the future. Internally it will make sure that all clauses that contained that variable will have disappeared first though.

Taken together this works well for clauses with a short life-span even if there are very many of them. I've used it successfully in my implementation of the IC3 algorithm for instance.

As to the question of unsat core from assumptions, Andreas is right that this feature already exist in MiniSat and no modifications are necessary. After each call to solve one can read a subset of the assumptions sufficient to cause the contradiction from the member variable "conflict" (technically the subset is the negation of assumptions so that it can be interpreted as a conflict clause).

/Niklas

[Mate Soos]

Hi all,

On 03/06/2013 03:15 PM, Niklas Sörensson wrote:

On Wed, Mar 6, 2013 at 11:58 AM, Mate Soos <soos...@gmail.com> wrote:

On 03/06/2013 12:54 AM, Hao Zheng wrote:

> Thanks a lot for the reply. For the method using activation variables, I am curious if the dead clauses in the sat solver due to the activation variables would affect the performance of solving?

In short: yes, very much. So try to use as few activation variables as
possible: remember that one activation variable can activate more than
one clause, so you can activate groups of clauses. If it's slow you may
try to run more than one instance, and set (not assume) the variables.
It sounds like doing the same job multiple times but after a while the
overhead is so large that it's actually faster.I believe there was a
presentation last year at SAT'12 about too many assumptions slowing down
the solver too much. Flexibility costs.

Sorry for contradicting you Mate, but if the question is whether dead clauses hurt performance I'd say no. They are garbage collected periodically and shouldn't be too much in the way.

I am a bit confused, I guess it's a misunderstanding of the question. As I understood it, it was about adding clauses such as:

x1000 V (actual clause)
x1001 V (actual clause)
....

where "actual clause"-s never contain variables >x999 and x1000, x1001.. are activation variables, used to activate or deactivate a clause by giving them as assumptions. If used extensively, as far as I can see, this would hit performance: e.g. no binary irredundant (="non-learnt") clauses in DB. So probably I am misunderstanding something, and I am curious what :) Can you please clarify?

Thanks in advance,

Mate

PS: As for using up index-space, that can be alleviated by renumbering variables. It's not that painful to do and gives significant speedup -- it's one of the few "hip" things I implemented that I don't regret :)

[Niklas Sörensson]

Hi all,

On 03/06/2013 03:15 PM, Niklas Sörensson wrote:

On Wed, Mar 6, 2013 at 11:58 AM, Mate Soos <soos...@gmail.com> wrote:

On 03/06/2013 12:54 AM, Hao Zheng wrote:

> Thanks a lot for the reply. For the method using activation variables, I am curious if the dead clauses in the sat solver due to the activation variables would affect the performance of solving?

In short: yes, very much. So try to use as few activation variables as
possible: remember that one activation variable can activate more than
one clause, so you can activate groups of clauses. If it's slow you may
try to run more than one instance, and set (not assume) the variables.
It sounds like doing the same job multiple times but after a while the
overhead is so large that it's actually faster.I believe there was a
presentation last year at SAT'12 about too many assumptions slowing down
the solver too much. Flexibility costs.

Sorry for contradicting you Mate, but if the question is whether dead clauses hurt performance I'd say no. They are garbage collected periodically and shouldn't be too much in the way.

I am a bit confused, I guess it's a misunderstanding of the question. As I understood it, it was about adding clauses such as:

x1000 V (actual clause)
x1001 V (actual clause)
....

where "actual clause"-s never contain variables >x999 and x1000, x1001.. are activation variables, used to activate or deactivate a clause by giving them as assumptions. If used extensively, as far as I can see, this would hit performance: e.g. no binary irredundant (="non-learnt") clauses in DB. So probably I am misunderstanding something, and I am curious what :) Can you please clarify?

Now I don't understand your concern here :) What I'm saying is that when we are done with a particular clause we set the corresponding activation literal to a value that disables that clause forever. These dead clauses don't affect performance since they will be removed periodically. It's a question that has been asked many times before so that how interpreted it here.

If you are talking about keeping around extensive amounts of clauses that don't have a short life span, but still only a small subset is active in any particular call to solve, then yes that might be a different situation. Hard to say anything general about that though; depends on the particular application what's most appropriate to do.

 

Thanks in advance,

Mate

PS: As for using up index-space, that can be alleviated by renumbering variables. It's not that painful to do and gives significant speedup -- it's one of the few "hip" things I implemented that I don't regret :)

Yes, that's rather nice for reusing eliminated/assigned indices that occurs during preprocessing, but it doesn't really solve the index space issue entirely unless you also add something to the API to let the user "free" a variable. I mean, with renumbering you essentially have user-level indices, and internal indices. The internal indices can be kept compact, but the user-level indices still can be dominated by dead variables. That's what my simple change was designed to address. Renumbering is something I might add too. You're saying that it gives a noticeable speed-up?

Regards,

Niklas

[Mate Soos]

Hi All,

On 03/07/2013 01:28 PM, Niklas Sörensson wrote:

PS: As for using up index-space, that can be alleviated by renumbering variables. It's not that painful to do and gives significant speedup -- it's one of the few "hip" things I implemented that I don't regret :)

Yes, that's rather nice for reusing eliminated/assigned indices that occurs during preprocessing, but it doesn't really solve the index space issue entirely unless you also add something to the API to let the user "free" a variable. I mean, with renumbering you essentially have user-level indices, and internal indices. The internal indices can be kept compact, but the user-level indices still can be dominated by dead variables. That's what my simple change was designed to address. Renumbering is something I might add too. You're saying that it gives a noticeable speed-up?

Yes, a lot, relatively speaking (10%+ speedup, but just compile CryptoMS from 'master' at github, and run with "--renumber 0" and you will see). The watched[] lookup (I am not talking about watched[][]) will be much better (since watched can be quite large), and more importantly, assings[] lookup will be much better. If dead variables are many (which they are, most of the time), your cache is mostly used to store the assignment of dead variables. With renumbering you get your effective cache usage up to ~100%. Since assigns[] is the single most accessed array during propagation, it's not so bad.

Furthermore, implementation is quite simple. I have an inter_to_outer[] and an outer_to_inter[] and translate at the edge: when adding clauses and when outputting models/final conflict clause. I periodically update both arrays with a new map, and apply that map to all clauses and assings[]. The only tricky part is applying the map to watched[] where I implemented a system that swap()-s every circle until all is done. If you want to, you can also take a peek at my solution, for this swapping part I give you MIT licence.

Cheers,

Mate

[Hao Zheng]

Hi, all,

Thanks very much for the discussions. They clarified my confusions a lot. Just to confirm, if temporary clauses are permanently disabled by activation variables, the solving performance will be impacted marginally. On the other hand, if clauses exist in the entire life span of a solving process, but are activated from time to time, then a large number of these clauses could hurt the solving performance. Please correct me if my understanding is not right.

Thanks,

H

[Niklas Sörensson]

Yes, that sounds about right.

/Niklas

Thanks,

H

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.