UNSAT core
bee
to generate the UNSAT core for UNSAT problems? If so, how does minisat
do it?
Thanks.
Niklas Sörensson
MiniSat2 does not have support for UNSAT core or proof logging at the
moment. There is an older version that has very basic support for
proof-logging:
http://minisat.se/downloads/MiniSat-p_v1.14.2006-Sep-07.src.zip
However this is fairly old and to get what you need you may have to
hack it a bit. Chances are good that you may be better off with some
other solver that comes with good proof-logging support such as
PicoSat:
On the positive side, the time when I will release the next version of
MiniSat is now closing in. I'm not sure yet, but I'm aiming for a
release in end of June beginning July. I've had working proof-logging
support in this version for some time which works, but it needs some
more work before I'm comfortable to release it to the general public.
Cheers,
/Niklas
bee
Alberto Griggio
> MiniSat2 does not have support for UNSAT core or proof logging at the
> moment.
get an unsat core:
1. label each clause with a fresh literal !lbl
2. Assume each lbl (positively)
3. Extract the conflict in terms of the original assumptions: the
(one, actually) unsat core is given by all the clauses whose labels
occur in the final conflict
HTH,
Alberto
Daniel Le Berre
Alberto,
How does that method scale?
Is it possible for instance to compute an UNSAT core for tens of
thousand of clauses?
Daniel
Niklas Sörensson
I have not tried it myself, but I think there is a chance that it
works well enough. In theory it should not make any difference to the
search behavior. In practice there will be a constant slowdown by the
presence of extra variables and more memory for the clauses. If one
makes sure to allocate all *real* variables before any of the
label-variables the memory behavior is probably a bit better since it
is good to have a compact representation of the real variables.
Note that a proof-logging based approach also has a cost, and it could
be the case that this approach is actually better in some instances.
In practice there is also sometimes no need for one label for each
clause, but there are natural groups where the label can be reused.
Anyway, if someone has experience with this approach compared to the
proof-logging based one it would be nice to hear about it!
/Niklas
Joao Marques-Silva
The method you are describing is know as the 'Marker Literals' method.
As far as I know it was first described in the following reference:
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-
Carbonell: Efficient Generation of Unsatisfiability Proofs and Cores
in SAT. LPAR 2008: 16-30
If I recall correctly, the performance is not good compared to other
approaches.
-- Joao
On May 2, 4:24 pm, Niklas Sörensson <nikla...@gmail.com> wrote:
Niklas Sörensson
<jpmarqu...@gmail.com> wrote:
>
> Alberto, Daniel and Niklas,
>
> The method you are describing is know as the 'Marker Literals' method.
> As far as I know it was first described in the following reference:
>
> Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-
> Carbonell: Efficient Generation of Unsatisfiability Proofs and Cores
> in SAT. LPAR 2008: 16-30
>
> If I recall correctly, the performance is not good compared to other
> approaches.
That's a nice paper that I've missed! I guess it is rather obvious
that this doesn't work well when you think about it more than 30 sec
:)
/Niklas
Daniel Le Berre
Le 3 mai 09 à 17:34, Niklas Sörensson a écrit :
I also missed that paper.
I guess it is sufficient in some cases, and it allows current minisat2
users to have access to unsat core.
I checked the code of minisat2 and I noticed that the assumptions are
now always propagated after the learned unit clauses, in order to
allow such conflict analysis based on assumptions.
When you use an assumption per clause, that might take a while to
unset and set all those literals at each learned literal.
I am wondering if it is possible to do the final conflict analysis
when the assumptions are propagated first, as it used to be in minisat
1.x.
I know that an analyzeFinal function exists in minisat 1.14, but the
code is tagged "experimental" :)
Anybody around used analyzeFinal in minisat 1.14?
Cheers,
Daniel
Alberto Griggio
> Alberto, Daniel and Niklas,
>
> The method you are describing is know as the 'Marker Literals' method.
> As far as I know it was first described in the following reference:
>
> Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-
> Carbonell: Efficient Generation of Unsatisfiability Proofs and Cores
> in SAT. LPAR 2008: 16-30
implemented in the Yices SAT/SMT solver already in 2006, and briefly
described here: https://disi.unitn.it/~griggio/papers/sat07_extended.pdf
(extended version of a SAT'07 short paper). In fact, I thought that it
was invented by you MiniSat guys...
However, the above paper does a much better job in describing its
practical shortcomings.
> If I recall correctly, the performance is not good compared to other
> approaches.
current version of minisat :-) And if the input is not that big, it
might still work...
Best,
Alberto
Niklas Sörensson
>
> I also missed that paper.
>
> I guess it is sufficient in some cases, and it allows current minisat2 users
> to have access to unsat core.
Indeed.
> I checked the code of minisat2 and I noticed that the assumptions are now
> always propagated after the learned unit clauses, in order to allow such
> conflict analysis based on assumptions.
It's true that this was changed, but the change was not necessary for
analyzeFinal to work I think. The motivation for the change is a bit
different: previously a call to search would never backtrack past the
node after the last assumption. There is a problem with this, namely
that some learned implications really belong to earlier levels and
should be propagated there but instead they are propagated at the
so-called root-level. This is bad since it breaks the desirable
invariant that all implications are performed at the level where they
are first implied. Since it only happens in this special situation we
were able to live with this, but it is dangerous since as soon as you
make changes this could break things badly. Another important drawback
is that learned unit clauses not be remembered after the call to
solve.
I guess that a side effect is that analyzeFinal is more obviously
correct as you say, but I think that the previous implementation was
fairly extensively tested during the development of the old
proof-logging version of MiniSat.
> When you use an assumption per clause, that might take a while to unset and
> set all those literals at each learned literal.
There are certainly cases were this may be a problem, and the
application that started the discussion is a likely candidate. I still
think the advantages outweigh this disadvantage. Moreover, maybe one
could do something better to avoid this bad behavior when it occurs.
> I am wondering if it is possible to do the final conflict analysis when the
> assumptions are propagated first, as it used to be in minisat 1.x.
>
> I know that an analyzeFinal function exists in minisat 1.14, but the code is
> tagged "experimental" :)
>
> Anybody around used analyzeFinal in minisat 1.14?
I have mostly used it since after I did this change and I don't know
much about if others have used this feature at all. At least I never
received any bug-reports for this.
As you say it is not really documented, which is a pity since it is
very nice and useful. On the other hand, people seems to have picked
it up anyway to some extent.
Chhers,
/Niklas