Constraint Propagation

;; Standard demo preamble:

|= (in-package "STELLA")


|= (defmodule "/PL-USER/CONSTRAINTS")

|MDL|/PL-USER/CONSTRAINTS

|= (in-module "/PL-USER/CONSTRAINTS")


|= (clear-module "/PL-USER/CONSTRAINTS")


|= (reset-features)

|i|()

|= (in-dialect :KIF)

:KIF

;; The already familiar `Person' class:

|= (defclass PERSON (STANDARD-OBJECT)
  :documentation "The class of human beings."
  :slots
  ((happy :type BOOLEAN)
   (age :type INTEGER)))

|C|PERSON

|= (assert (Person Fred))

|P|(PERSON FRED)

;; In PowerLoom constraint propagation is performed on a per-module
;; basis.  By default, it is turned off for every module.  To enable
;; it, we can use PowerLoom's `propagate-constraints' command (we
;; leave out the optional module argument, which means that constraint
;; propagation will be enabled in the current module):

|= (propagate-constraints)


;; We start by asserting the following disjunction:

|= (assert (or (happy Fred) (= (age Fred) 40)))

|P|(or (HAPPY FRED)
    (= (AGE FRED) 40))

;; When we ask for one of the disjuncts, we do not get an answer,
;; since nothing is known about the individual disjuncts:

|= (ask (= (age Fred) 40))


;; Now we assert the negation of the first disjunct, which, since
;; constraint propagation is turned on, will propagate to the second
;; disjunct and assert it to be true:

|= (assert (not (happy Fred)))

|P~|(HAPPY FRED)

;; To show that no inference is necessary to answer the next question,
;; we turn on goal-tracing of the inference engine:

|= (set-feature goal-trace)

|i|(:GOAL-TRACE)

;; Now the query below returns true.  The goal trace shows that no
;; inference needs to be performed to get the answer, since the asked
;; proposition is available directly, just like a regular assertion:

|= (ask (= (age Fred) 40))

PATTERN: []
| GOAL: (= (AGE FRED) 40)
| SUCC: 
|L|TRUE

;; Constraint propagation picks up certain inferences much more
;; efficiently than the backward chainer.  Note that, currently,
;; PowerLoom would have not been able to make the above inference
;; without having constraint propagation turned on.  

;; A shortcoming of the current implementation of constraint
;; propagation is that its inferences are truth-maintained only in a
;; very coarse-grained fashion (this will change in future versions).
;; As long as the assertions in a module grow monotonically, all
;; inferences are cached in a strict-inference world, but that world
;; gets blown away completely as soon as some retraction is performed
;; in the module.  E.g., if we retract the following proposition, the
;; previous query will not return true anymore:

|= (retract (not (happy Fred)))

|P?|(HAPPY FRED)

|= (ask (= (age Fred) 40))

PATTERN: []
| GOAL: (= (AGE FRED) 40)
| FAIL 

;; As mentioned above, after a retraction constraint propagation
;; inferences get blown away.  Additionally, constraint propagation
;; gets turned off completely.  To turn it back on we have to call
;; `propagate-constraints' again.  Note, that `propagate-constraints'
;; not only enables constraint propagation, but it also performs
;; constraint propagation on all propositions currently asserted in a
;; module, which for large KBs could cause a significant amount of
;; recomputation.

|= (propagate-constraints)


;; Below, we run a variation of the previous example that makes use of
;; the violation of an equality constraint:

|= (assert (Person Fritz))

|P|(PERSON FRITZ)

|= (assert (= (age Fritz) 25))

|P|(= (AGE FRITZ) 25)

;; So far, we don't know whether Fritz is happy:

|= (ask (happy Fritz))

PATTERN: []
| GOAL: (HAPPY FRITZ)
| FAIL 

;; Now we assert a similar disjunction as used in the example above.
;; Since the second disjunct clashes with the age asserted above,
;; constraint propagation asserts the first disjunct to be true:

|= (assert (or (happy Fritz) (= (age Fritz) 40)))

|P|(or (HAPPY FRITZ)
    (= 25 40))

;; Now this query succeeds without any inference:

|= (ask (happy Fritz))

PATTERN: []
| GOAL: (HAPPY FRITZ)
| SUCC: 
|L|TRUE

;; Propagation of equality constraints:

|= (assert (Person John))

|P|(PERSON JOHN)

|= (assert (Person Mary))

|P|(PERSON MARY)

;; John is the same age as Mary:

|= (assert (= (age John) (age Mary)))

|P|(= (AGE JOHN) (AGE MARY))

;; We don't yet know Mary's age:

|= (ask (= (age Mary) 25))

PATTERN: []
| GOAL: (= (AGE MARY) 25)
| FAIL 

;; Now we set John's age to be 25:

|= (assert (= (age John) 25))

|P|(= (AGE JOHN) 25)

;; This assertion got propagated through the previously asserted
;; equality, thus, now we also know that Mary's age is 25:

|= (ask (= (age Mary) 25))

PATTERN: []
| GOAL: (= (AGE MARY) 25)
| SUCC: 
|L|TRUE

|=