Solution Hint

[aliva]

Hi,

I am wondering if MiniSat has some feature or it can be extended to
use a "hint solution". A "hint solution" is a set of true/false
assignment to each variable, and it may not satisfy the formula that I
am trying to check. However, an actual solution of the formula may
match the hint closely in terms of number of variables that have same
assignment in the actual solution and the hint.

If there have any research on similar ideas, I would appreciate if you
let me know.

Thanks,
Aliva

[Bryan Silverthorn]

On Sun, Mar 27, 2011 at 17:14, aliva <aliv...@gmail.com> wrote:

Hi,

I am wondering if MiniSat has some feature or it can be extended to
use a "hint solution". A "hint solution" is a set of true/false
assignment to each variable, and it may not satisfy the formula that I
am trying to check. However, an actual solution of the formula may
match the hint closely in terms of number of variables that have same
assignment in the actual solution and the hint.

I'm not sure if Minisat provides this functionality, but there are (minimally-tested) patches to Cryptominisat that do, e.g.,

http://lists.gforge.inria.fr/pipermail/cryptominisat-devel/2011-February/000075.html

that have been applied to the differentWatchList branch:

http://gitorious.org/cryptominisat/cryptominisat/commits/differentWatchList

I'm neither a Minisat nor a CryptoMS developer, though; someone else can probably provide a more definitive answer.

It's also relatively simple to patch an SLS solver to take an explicit initialization. I can send you a patch for TNM, if you're interested.

If there have any research on similar ideas, I would appreciate if you
let me know.

I've looked into classifier-based schemes for generating such "hints", and a short paper will appear at SAT 2011. Vegard Nossum, who authored the CryptoMS patch above, has (I believe) been examining hand-generated hints for crypto and BMC instances. I'd be very interested in other related work (what are you considering?), and am happy to send references as I run across them.

By the way, Vegard has also implemented branch-order hints for CryptoMS; see the thread:

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

--

Bryan Silverthorn

[Niklas Sörensson]

Hello,

On Mon, Mar 28, 2011 at 12:14 AM, aliva <aliv...@gmail.com> wrote:
> Hi,
>
> I am wondering if MiniSat has some feature or it can be extended to
> use a "hint solution". A "hint solution" is a set of true/false
> assignment to each variable, and it may not satisfy the formula that I
> am trying to check. However, an actual solution of the formula may
> match the hint closely in terms of number of variables that have same
> assignment in the actual solution and the hint.

Yes, it's possible to specify suggested values for variables that will
be tried first during branching. This is done by the following method:

void setPolarity (Var v, lbool b);

Note that it gives the preferred sign of that variable. I.e.
"setPolarity(x,l_True)" will prefer to branch first on the signed "~x"
and "setPolarity(x,l_False)" will prefer the unsigned "x".

Also, this disables the normal phase-saving polarity heuristics for
that variable, and whether this will be useful or not is heavily
application dependent. The default heuristic behaviour can be restored
for a variable by calling "setPolarity(x,l_Undef)".

I hope this helps,

/Niklas

[Deke Yu]

hello, Niklas. I am wondering if it is possible to just set the polarity of a variable which is chose by VSIDS at the beginning of minisat process.

the polarity of the variable is achieved by SLS. This beginning step may help to improve the search. When and where should I call setPolarity() after I get an assignment from SLS? Would you mind to give me some help, thank you.  

[Niklas Sörensson]

Hello ,

What you can do is the following:

1. Generate the SAT problem in a Solver or SimpSolver object.

2. For all variables x that you have a preferred value for, call setPolarity(x, l_False) if you want it to be true, and setPolarity(x, l_True) otherwise.

3. Run solve.

Not that this completely replaces the internal heuristic for polarities which might not necessarily be a good idea. If you only want it to have effect initially, then this is not directly supported and you'd have to hack minisat to add that functionality (would be simple though).

I think you mentioned in another mail that you are actually using the c-version. That version is old and I don't remember it very well. What I said above may or may not apply to that version.

Best Regards,

Niklas