Overriding VSIDS

[Chanseok Oh]

Dear All,

Is there an option to partly enforce the order of selecting decision
variables before everything (even above VSIDS)? I generate a partial
list of variables that I want to make MiniSat branch on these variable
first in order and then later branch normally with VSIDS. Any MiniSat
version would suffice.

If MiniSat doesn't provide such an option, I would appreciate it if
you could suggest any other SAT solver (it doesn't have to be very
efficient) that supports this.

Otherwise, I will have to modify MniSat by myself, which I definitely
want to avoid.

Regards,
Chanseok Oh

[Niklas Een]

If you use MiniSat through the API, you can use the assumption interface to achieve this. Suppose you want to branch on variables a, b, c first; then you essentially enumerate all assignments of these variables and pass them to solve(), but (importantly) you record the conflict clause returned through the member variable "conflict" and avoid any assignment that would violate these recorded clauses. Example:

   (1) You start with solve({a, b, c}).
   (2) The returned conflict is {~a, ~b}
   (3) You skip over {a, b, ~c} (if this was your next assignment
        in the enumeration) and go directly to {a, ~b, c}.

It is not perfect, but hopefully it will do for your purposes.

// Niklas

[Chanseok Oh]

Thank you very much for the explanation. Unfortunately, this approach
is not suitable in my case for a few reasons.

(1) Most importantly, this alternative method appears to lose all the
benefit of learning clauses and confict analysis.
(2) I am experimenting with very large instances (~180K variables),
and the number of variables I want to branch on first ranges from
hundreds to a few thousands (even larger than this sometimes). My
speculation is that following this approach will incur hugh overhead.
I cannot think of storing every conflict clause returned and analyzing
them to decide the next assignment.

Basically, what I have developed is a new branching scheme which I
believe will outperform VSIDS for a very definite reason, and what I
am trying to do is benchmarking. Judging from your response, I think I
need to modify the code a bit to simulate this. I have never looked
into it, so it would be very helpful if you could point out where to
start. Just pointing out which files or (hopefully) functions would be
modifed would be fine.

Again, thank you for your kind answer.

Regards,
Chanseok Oh

> > Chanseok Oh- Hide quoted text -
>
> - Show quoted text -

[Chanseok Oh]

Okay, I found one of the group members, Bryan Silverthorn, left in the
past a relevant information in a discussion:

http://groups.google.com/group/minisat/browse_thread/thread/564cc6f26348ec28


So, it looks like that I can apply a patch described below to the
latest CryptoMiniSat 2.9.0 to achieve this. Several people confirmed
that the patch is actually working.

http://lists.gforge.inria.fr/pipermail/cryptominisat-devel/2011-March/000131.html


Regards,
Chanseok Oh

> > - Show quoted text -- Hide quoted text -

[Niklas Sörensson]

Hello,

On Wed, Aug 10, 2011 at 12:43 AM, Chanseok Oh <chans...@gmail.com> wrote:
> Thank you very much for the explanation. Unfortunately, this approach
> is not suitable in my case for a few reasons.
>
> (1) Most importantly, this alternative method appears to lose all the
> benefit of learning clauses and confict analysis.
> (2) I am experimenting with very large instances (~180K variables),
> and the number of variables I want to branch on first ranges from
> hundreds to a few thousands (even larger than this sometimes). My
> speculation is that following this approach will incur hugh overhead.
> I cannot think of storing every conflict clause returned and analyzing
> them to decide the next assignment.
>
> Basically, what I have developed is a new branching scheme which I
> believe will outperform VSIDS for a very definite reason, and what I
> am trying to do is benchmarking. Judging from your response, I think I
> need to modify the code a bit to simulate this. I have never looked
> into it, so it would be very helpful if you could point out where to
> start. Just pointing out which files or (hopefully) functions would be
> modifed would be fine.

I've made a patch to the current mainline of MiniSat that allows you
to do what you want. You can find it in the github minisat repository.
Here's a direct link to the branch with the patch:

https://github.com/niklasso/minisat/tree/top/varorder/partial-static-order

There is one new method to the solver class that is called
"setVarOrdering()" that one can use the declare fixed priorities for
variables. In the variable heuristic variables are then chosen based
on a lexicographic order of priorites (increasing) and dynamic
activity (decreasing). For example:

setVarOrdering(x, 0);
setVarOrdering(y, 1);
setVarOrdering(z, 2);
setVarOrdering(w, 2);

This will guarantee that x is chosen first, then y, then the order of
z and w is decided by their current VSIDS activity.

Note that there is a slight performance hit with this patch, but it is
small enough that I'd be very surprised if it matters for you.

Let me know if you have any questions,

Regards,

/Niklas

[Chanseok Oh]

Hello Niklas,

It is very kind of you to have actually implemented this. I have never
expected that someone would ever set out to do it just for me. I am
really impressed, and I cannot thank you enough.

Regards,
Chanseok Oh

On Aug 10, 8:28 am, Niklas Sörensson <nikla...@gmail.com> wrote:
> Hello,
>
>
>
>
>
> On Wed, Aug 10, 2011 at 12:43 AM, Chanseok Oh <chanseok...@gmail.com> wrote:
> > Thank you very much for the explanation. Unfortunately, this approach
> > is not suitable in my case for a few reasons.
>
> > (1) Most importantly, this alternative method appears to lose all the
> > benefit of learning clauses and confict analysis.
> > (2) I am experimenting with very large instances (~180K variables),
> > and the number of variables I want to branch on first ranges from
> > hundreds to a few thousands (even larger than this sometimes). My
> > speculation is that following this approach will incur hugh overhead.
> > I cannot think of storing every conflict clause returned and analyzing
> > them to decide the next assignment.
>
> > Basically, what I have developed is a new branching scheme which I
> > believe will outperform VSIDS for a very definite reason, and what I
> > am trying to do is benchmarking. Judging from your response, I think I
> > need to modify the code a bit to simulate this. I have never looked
> > into it, so it would be very helpful if you could point out where to
> > start. Just pointing out which files or (hopefully) functions would be
> > modifed would be fine.
>
> I've made a patch to the current mainline of MiniSat that allows you
> to do what you want. You can find it in the github minisat repository.
> Here's a direct link to the branch with the patch:
>

> https://github.com/niklasso/minisat/tree/top/varorder/partial-static-...

>
> There is one new method to the solver class that is called
> "setVarOrdering()" that one can use the declare fixed priorities for
> variables. In the variable heuristic variables are then chosen based
> on a lexicographic order of priorites (increasing) and dynamic
> activity (decreasing). For example:
>
>   setVarOrdering(x, 0);
>   setVarOrdering(y, 1);
>   setVarOrdering(z, 2);
>   setVarOrdering(w, 2);
>
> This will guarantee that x is chosen first, then y, then the order of
> z and w is decided by their current VSIDS activity.
>
> Note that there is a slight performance hit with this patch, but it is
> small enough that I'd be very surprised if it matters for you.
>
> Let me know if you have any questions,
>
> Regards,
>

> /Niklas- Hide quoted text -

[Chanseok Oh]

I would like to verify a few things:

(1) I noticed that if I do not call 'setVarOrdering()' for any
variable, it will have the highest priority, 0 by default. I do not
intend to call setVarOrdering() for every variable, and I want those
variables to have the lowest priority. So, I changed the code for the
default value to be INT_MAX instead of 0:

activity .reserve(v);
activity[v].fixed = INT_MAX;
activity[v].dynamic = rnd_init_act ? drand(random_seed) *
0.00001 : 0;

Will this be okay?

(2) I also noticed that the type Var is just int and MiniSat is
assigning an integer value that is one less than the actual variable
number read from input. Accordingly, I call the method in the
following way, subtracting 1 from the value I read from an input file.
Am I doing right?

for (not EOF) { // Pseudo-code
infs >> var;
if (var == 0) priority++;
else S.setVarOrdering(var-1, priority);
}

(3) I am setting the variable ordering (inserting the above code in
reality) after the Solver finished reading a CNF input file. I mean,
right after parse_DIMACS(in, S); in Main.cc. I believe there will be
no problem with this.


Again, thank you for your kindness.


Regards,
Chanseok Oh

> > - Show quoted text -- Hide quoted text -

[Niklas Sörensson]

On Wed, Aug 10, 2011 at 9:59 PM, Chanseok Oh <chans...@gmail.com> wrote:
> Hello Niklas,
>
> It is very kind of you to have actually implemented this. I have never
> expected that someone would ever set out to do it just for me. I am
> really impressed, and I cannot thank you enough.

No problem. It didn't take long (15 min + testing) and I expect others
my find this useful at times.

The hard part of evaluating your idea is still up to you :)

Regards,

/Niklas

[khushi chndrakar]

hello

        can anyone tell me is thr any new SAT Solver comes in SAT family