/usr/share/mozart/doc/fdt/node5.html is in mozart-doc 1.4.0-8ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>2.3 Spaces, Propagators, and Constraint Stores</TITLE><LINK href="ozdoc.css" rel="stylesheet" type="text/css"></HEAD><BODY><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node4.html#section.constraints.propagation"><< Prev</A></TD><TD><A href="node2.html">- Up -</A></TD><TD><A href="node6.html#section.constraints.intdom">Next >></A></TD></TR></TABLE><DIV id="section.constraints.spaces"><H2><A name="section.constraints.spaces">2.3 Spaces, Propagators, and Constraint Stores</A></H2><P>The computational architecture for constraint propagation is called a <A name="label17"></A><EM>space</EM> and consists of a number of propagators connected to a constraint store: </P><P></P><DIV align="center"><IMG alt="" src="latex27.png"></DIV><P> </P><P>The <A name="label18"></A><EM>constraint store</EM> stores a conjunction of basic constraints up to logical equivalence. An example for such a conjunction is </P><BLOCKQUOTE><P><IMG alt="X\in0\#5
\;\land\;
Y=8
\;\land\;
Z\in13\#23." src="latex28.png"></P></BLOCKQUOTE><P> </P><P>The <A name="label19"></A><EM>propagators</EM> impose nonbasic constraints, for instance, <IMG alt="X<Y" src="latex29.png"> or <IMG alt="{X^2+Y^2=Z^2}" src="latex30.png">. A propagator for a constraint <IMG alt="C" src="latex31.png"> is a concurrent computational agent that tries to narrow the domains of the variables occurring in <IMG alt="C" src="latex31.png">. </P><DIV class="apropos"><P class="margin">example of communicating propagators</P><P> Two propagators that share a variable <IMG alt="X" src="latex24.png"> can communicate with each other through the constraint store. To see an example for communicating propagators, suppose we have two propagators imposing the constraints </P><BLOCKQUOTE><P><IMG alt="X+Y=9
\qquad
2\cdot X+4\cdot Y=24" src="latex32.png"></P></BLOCKQUOTE><P> over a constraint store containing the following information about <IMG alt="X" src="latex24.png"> and <IMG alt="Y" src="latex8.png">: </P><BLOCKQUOTE><P><IMG alt="X\in0\#9
\qquad
Y\in0\#9" src="latex33.png"></P></BLOCKQUOTE><P> </P></DIV><P>As is, the first propagator cannot do anything. The second propagator, however, can narrow the domains of both <IMG alt="X" src="latex24.png"> and <IMG alt="Y" src="latex8.png">: </P><BLOCKQUOTE><P><IMG alt="X\in0\#8
\qquad
Y\in2\#6" src="latex34.png"></P></BLOCKQUOTE><P> </P><P>Now the first propagator can narrow the domain of <IMG alt="X" src="latex24.png">: </P><BLOCKQUOTE><P><IMG alt="X\in3\#7
\qquad
Y\in2\#6" src="latex35.png"></P></BLOCKQUOTE><P> </P><P>Now the second propagator can narrow the domains of both <IMG alt="X" src="latex24.png"> and <IMG alt="Y" src="latex8.png">: </P><BLOCKQUOTE><P><IMG alt="X\in4\#6
\qquad
Y\in3\#4" src="latex36.png"></P></BLOCKQUOTE><P> </P><P>This once more activates the first propagator, which narrows the domain of <IMG alt="X" src="latex24.png">: </P><BLOCKQUOTE><P><IMG alt="X\in5\#6
\qquad
Y\in3\#4" src="latex37.png"></P></BLOCKQUOTE><P> </P><P>Now the second propagator gets active once more and determines the values of <IMG alt="X" src="latex24.png"> and <IMG alt="Y" src="latex8.png">: </P><BLOCKQUOTE><P><IMG alt="X=6
\qquad
Y=3" src="latex38.png"></P></BLOCKQUOTE><P> </P><DIV class="apropos"><P class="margin">telling a constraint</P><P> Given a constraint store storing a constraint <IMG alt="S" src="latex7.png"> and a propagator imposing a constraint <IMG alt="P" src="latex20.png">, the propagator can tell to the constraint store a basic constraint <IMG alt="B" src="latex39.png"> if the conjunction <IMG alt="S\land
P" src="latex40.png"> entails <IMG alt="B" src="latex39.png"> and <IMG alt="B" src="latex39.png"> adds new and consistent information to the store. To <A name="label20"></A><EM>tell</EM> a constraint <IMG alt="B" src="latex39.png"> to a constraint store storing the constraint <IMG alt="S" src="latex7.png"> means to update the store so that it holds the conjunction <IMG alt="S\land B" src="latex41.png">. </P></DIV><DIV class="apropos"><P class="margin">operational and declarative semantics of propagators</P><P> The <A name="label21"></A><EM>operational semantics</EM> of a propagator determines whether the propagator can tell the store a basic constraint or not. The operational semantics of a propagator must of course respect the <A name="label22"></A><EM>declarative semantics</EM> of the propagator, which is given by the constraint the propagator imposes. </P></DIV><P>We require that the constraint store be always consistent; that is, there must always be at least one variable assignment that satisfies all constraints in the constraint store. </P><DIV class="apropos"><P class="margin">determined variables</P><P> We say that the constraint store <A name="label23"></A><EM>determines</EM> a variable <IMG alt="x" src="latex42.png"> if the constraint store knows the value of <IMG alt="x" src="latex42.png">, that is, if there exists an integer <IMG alt="n" src="latex43.png"> such that the constraint store entails <IMG alt="x=n" src="latex17.png">. </P></DIV><DIV class="apropos"><P class="margin">failed propagators</P><P> We say that a propagator is <A name="label24"></A><EM>inconsistent</EM> if there is no variable assignment that satisfies both the constraint store and the constraint imposed by the propagator (e.g., <IMG alt="X+Y=6" src="latex44.png"> over <IMG alt="X\in3\#9" src="latex45.png"> and <IMG alt="Y\in4\#9" src="latex46.png">). We say that a propagator is <A name="label25"></A><EM>failed</EM> if its operational semantics realizes that it is inconsistent. </P></DIV><DIV class="apropos"><P class="margin">entailed propagators</P><P> We say that a propagator is <A name="label26"></A><EM>entailed</EM> if every variable assignment that satisfies the constraint store also satisfies the constraint imposed by the propagator (e.g., <IMG alt="X<Y" src="latex29.png"> over <IMG alt="X\in3\#5" src="latex47.png"> and <IMG alt="Y\in6\#9" src="latex48.png">). As soon as the operational semantics of a propagator realizes that the propagator is entailed, the propagator ceases to exist. </P></DIV><P>We require that the operational semantics of a propagator detects inconsistency and entailment at the latest when the store determines all variables of the propagator. </P><DIV class="apropos"><P class="margin">stable propagators</P><P> We say that a propagator is <A name="label27"></A><EM>stable</EM> if it is either failed or its operational semantics cannot tell new information to the constraint store. </P></DIV><DIV class="apropos"><P class="margin">failed, stable, and solved spaces</P><P> We say that a space is <A name="label28"></A><EM>failed</EM> if one of its propagators is failed. We say that a space is <A name="label29"></A><EM>stable</EM> if all of its propagators are stable. We say that a space is <A name="label30"></A><EM>solved</EM> if it is not failed and there are no propagators left. </P></DIV><DIV class="apropos"><P class="margin">propagation order does not matter</P><P> When a space is created, its propagators start to tell basic constraints to the constraint store. This propagation activity continues until the space becomes stable. An important property of constraint propagation as we consider it here is the fact that the order in which the propagators tell information to the store does not matter. When we start a space repeatedly from the same state, it will either always fail or always arrive at the same constraint store (up to logical equivalence). </P></DIV><DIV class="apropos"><P class="margin">solutions of a space</P><P> A variable assignment is called a <A name="label31"></A><EM>solution</EM> of a space if it satisfies the constraints in the constraint store and all constraints imposed by the propagators. The solutions of a space stay invariant under constraint propagation and deletion of entailed propagators. </P></DIV></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node4.html#section.constraints.propagation"><< Prev</A></TD><TD><A href="node2.html">- Up -</A></TD><TD><A href="node6.html#section.constraints.intdom">Next >></A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~schulte/">Christian Schulte</A> and <A href="http://www.ps.uni-sb.de/~smolka/">Gert Smolka</A><BR><SPAN class="version">Version 1.4.0 (20110908185330)</SPAN></ADDRESS></BODY></HTML>
|