Re: Is there a problem of library sbds ?

From: <wh_at_icparc.ic.ac.uk>
Date: Fri 29 Apr 2005 02:39:22 PM GMT
Message-ID: <20050429143922.GB10995@tempest.icparc.ic.ac.uk>
Hi Ma Long,

On Thu, Apr 28, 2005 at 11:06:01PM -0700, Ma Long wrote:
> May I conclude for library sbds usage, the variable matrix
> generated by symmetry breaking should be not prefixed by
> some constraints, otherwise some possible solutions will be
> missed in symmetry breaking search.

That is correct.  The behaviour of the library is not defined if the
symmetries you provide are not symmetries of the problem/constraints you
provide.  By adding a partial assignment to the original symmetric problem,
you are changing the problem and potentially changing its symmetries
(depending upon exactly which assignments you make).

The solution is straightforward: use sbds_try/2 to make the heuristic
assignments (after sbds_initialise/5 has been called, of course).  That way
the SBDS library knows about the assignments and takes them into account
when doing the symmetry breaking (as far as it is concerned, these are just
the first assignments that you are choosing to make during the search).

Note that if you don't want to explore the alternatives to your heuristic
assignments, you should use a cut or once/1 or something to prune the choice
point(s) so that sbds_try/2 won't backtrack and try the other choice.  If
there's a chance your heuristic assignments might fail, it's probably worth
making sure that sbds_try/2 has actually made the assignment you asked for
and not tried something else because the original assignment failed.  For
example, you might use a small utility predicate:

committed_sbds_try(X, Val) :-
	( sbds_try(X, Val), X == Val ->
	    true
	;
	    printf(error, "Committed assignment %w = %w failed.%n", [X, Val]),
	    abort
	).

(The if-then-else structure prunes any choice points introduced in the
conditional.)

Cheers,
Warwick
Received on Fri Apr 29 15:45:37 2005

This archive was generated by hypermail 2.1.8 : Wed 16 Nov 2005 06:07:36 PM GMT GMT