Before sending a bug report to the screamer people, I thought I'd just
ask here if maybe I'm just stupid. I hope we have some screamer experts
around...
I just wanted to compare the power of =v and funcallv, and for the
latter I wrote this function:
(defun test ()
(let ((a (an-integer-betweenv 0 10))
(b 6)
(c (an-integer-betweenv 2 1000)))
(assert! (funcallv #'= a b))
(assert! (funcallv #'= a c))
(all-values
(solution
(list a b c)
(static-ordering 'linear-force)))))
This should return ((6 6 6)), but somehow it gives me many many
different values as c doesn't seem to be restricted. Any clue what might
be wrong?
Regards,
Benjamin
Benjamin Teuber wrote:
> Before sending a bug report to the screamer people, I thought I'd just
> ask here if maybe I'm just stupid. I hope we have some screamer experts
> around...
Not stupid, you've hit a snag it can be hard to spot.
You have to do something like this:
(defun test2 ()
(let* ((a (an-integer-betweenv 0 10))
(b 6)
(c (an-integer-betweenv 2 1000))
(t1 (funcallv #'= a b))
(t2 (funcallv #'= a c)))
(assert! t1)(assert! t2)
(all-values
(solution
(list a b c t1 t2)
(static-ordering #'linear-force)))))
That is, you must in general include all the involved variables to the
call to SOLUTION. This is documented in the Screamer-docs in that
constraint-propagation is incomplete; I forget where exactly.
Iver Odin Kvello wrote:
> You have to do something like this:
> (defun test2 ()
> (let* ((a (an-integer-betweenv 0 10))
> (b 6)
> (c (an-integer-betweenv 2 1000))
> (t1 (funcallv #'= a b))
> (t2 (funcallv #'= a c)))
> (assert! t1)(assert! t2)
> (all-values
> (solution
> (list a b c t1 t2)
> (static-ordering #'linear-force)))))
>
> That is, you must in general include all the involved variables to the
> call to SOLUTION. This is documented in the Screamer-docs in that
> constraint-propagation is incomplete; I forget where exactly.
>
Thanks for your help, this version works. Do you think this has to be
done with all funcallv (or even other **v functions) or just some? If
the former is true, I'll have to change a lot of code...
Too bad I don't find that place in the docs you mentioned.
Now I also tried to reach the Screamer people, but until I didn't find a
working contact adress...
Don't send a bug report :) Integer "discretization" constraints, not
a bug, are behind your confusion. See *maximum-discretization-range* in
screamer.lisp... You can either explicitly set the value of this
variable or "discretize" everything by setting it to nil.
(defun test ()
(let ((*maximum-discretization-range* NIL))
(all-values
(solution
(let ((a (an-integer-betweenv 0 10))
(b 6)
(c (an-integer-betweenv 2 1000)))
(assert! (funcallv #'= a b))
(assert! (funcallv #'= a c))
(list a b c))
(static-ordering #'linear-force)))))
> (test)
((6 6 6))
>
Scott Douglass wrote:
> Don't send a bug report :) Integer "discretization" constraints, not
> a bug, are behind your confusion. See *maximum-discretization-range* in
> screamer.lisp... You can either explicitly set the value of this
> variable or "discretize" everything by setting it to nil.
>
> (defun test ()
> (let ((*maximum-discretization-range* NIL))
> (all-values
> (solution
> (let ((a (an-integer-betweenv 0 10))
> (b 6)
> (c (an-integer-betweenv 2 1000)))
> (assert! (funcallv #'= a b))
> (assert! (funcallv #'= a c))
> (list a b c))
> (static-ordering #'linear-force)))))
>
>
> > (test)
> ((6 6 6))
> >
Okay, I guess this means that only assert!-funcallv's used on
not-discretetized variables don't work directly and should instead be
done by introducing another variable, right? Are there other cases where
I need this?
If I use a-member-ofv instead, will the variable always be discrete?
Thanks,
Benjamin
> Thanks for your help, this version works. Do you think this has to be
> done with all funcallv (or even other **v functions) or just some? If
> the former is true, I'll have to change a lot of code...
The relevant documentation is in the "Constraint Propagation" section
of
the AAAI93.PS paper in the docs catalog of the Screamer distribution.
From
this paper:
"By design all of the constraint primitives described so far use only
fast
local propagation techniques. Such techniques are necessarily
incomplete;
they cannot always solve systems of constraints or determine that they
are unsolvable."
so the answer is 'just some', but in general one should solve all
relevant variables as a
system.
Some examples using ORV:
(defun test-1 ()
(let* ((v (an-integer-betweenv 0 3))
(o01 (orv (=v v 0)(=v v 1)))
(o23 (orv (=v v 2)(=v v 3)))
(both (andv o01 o23)))
(one-value (solution (list both) (static-ordering
#'linear-force)))))
This 'should' return (NIL), but returns
(test-1) => (T)
But when solving all variables:
(defun test-2 ()
(let* ((v (an-integer-betweenv 0 3))
(o01 (orv (=v v 0)(=v v 1)))
(o23 (orv (=v v 2)(=v v 3)))
(both (andv o01 o23)))
(all-values (solution (list both v) (static-ordering
#'linear-force)))))
This returns ((NIL 0) (NIL 1) (NIL 2) (NIL 3)).
With MEMBERV however, one gets the expected result:
(defun test-3 ()
(let* ((v (an-integer-betweenv 0 3))
(o01 (memberv v '(0 1)))
(o23 (memberv v '(2 3)))
(both (andv o01 o23)))
(one-value (solution (list both) (static-ordering
#'linear-force)))))
(test-3) => (NIL)
But not here by changing discretization range, obviously:
(defun test-4 ()
(let ((*maximum-discretization-range* NIL))
(let* ((v (an-integer-betweenv 0 3))
(o01 (orv (=v v 0)(=v v 1)))
(o23 (orv (=v v 2)(=v v 3)))
(both (andv o01 o23)))
(one-value (solution (list both) (static-ordering
#'linear-force))))))
(test-4) => (T)