/usr/share/mozart/doc/cpitut/node2.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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>1.1 Basic Concepts</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="node1.html">- Up -</A></TD><TD><A href="node3.html#u_getting_started">Next >></A></TD></TR></TABLE><DIV id="u_basic_concepts"><H2><A name="u_basic_concepts">1.1 Basic Concepts</A></H2><P>This chapter explains the basic concepts of computation with finite domain constraints in Oz. Further, it explains the implementation of constraints by propagators. For more details see <A href="../fdt/index.html">``Finite Domain Constraint Programming in Oz. A Tutorial.''</A>. </P><DIV id="u_basic_concepts.computation"><H3><A name="u_basic_concepts.computation">1.1.1 Computation with Constraints in Oz</A></H3><P></P><DIV class="apropos"><P class="margin">Basic Constraint</P><P> A <EM>Basic Constraint</EM> takes the form <IMG alt="x=n, x=y" src="latex2.png"> or <IMG alt="x \in D" src="latex3.png">, where <IMG alt="x" src="latex4.png"> and <IMG alt="y" src="latex5.png"> are variables, <IMG alt="n" src="latex6.png"> is a non-negative integer and <IMG alt="D" src="latex7.png"> is a finite domain. </P></DIV><DIV class="apropos"><P class="margin">Constraint Store</P><P> The basic constraints reside in the <EM>Constraint Store</EM>. Oz provides efficient algorithms to decide satisfiability and entailment for basic constraints. </P></DIV><DIV class="apropos"><P class="margin">Propagators</P><P> For more expressive constraints, like <IMG alt="x + y = z" src="latex8.png">, deciding their satisfiability is not computationally tractable. Such non-basic constraints are not contained in the constraint store but are imposed by <EM>propagators</EM>. A propagator is a <EM>computational agent</EM> which is <EM>imposed on</EM> the variables occurring in the corresponding constraint. These variables are called the propagator's <EM>parameters</EM>. The propagator tries to narrow the domains of the variables it is imposed on by amplifying the store with basic constraints. </P></DIV><DIV class="apropos"><P class="margin">Constraint Propagation</P><P> This narrowing is called <EM>constraint propagation</EM>. A propagator <IMG alt="P" src="latex9.png"> amplifies the store <IMG alt="S" src="latex10.png"> by writing a basic constraint <IMG alt="\phi" src="latex11.png"> to it, if <IMG alt="P \wedge S" src="latex12.png"> entails <IMG alt="\phi" src="latex11.png"> but <IMG alt="S" src="latex10.png"> on its own does not. If <IMG alt="P" src="latex9.png"> ceases to exist, it is either entailed by the store <IMG alt="S" src="latex10.png">, or <IMG alt="P\wedge S" src="latex13.png"> is unsatisfiable. Note that the amount of propagation depends on the operational semantics of the propagator. </P></DIV><P> As an example, assume a store containing <IMG alt="x,y,z \in \{1,\ldots,10\}" src="latex14.png">. The propagator for <IMG alt="x+y<z" src="latex15.png"> narrows the domains to <IMG alt="x,y \in
\{1,\ldots,8\}" src="latex16.png"> and <IMG alt="z \in \{3,\ldots,10\}" src="latex17.png"> (since the other values cannot satisfy the constraint). Adding the constraint <IMG alt="z=5" src="latex18.png"> causes the propagator to strengthen the store to <IMG alt="x,y \in \{1,\ldots,3\}" src="latex19.png"> and <IMG alt="z=5" src="latex18.png">. Imposing <IMG alt="x=3" src="latex20.png"> lets the propagator narrow the domain of <IMG alt="y" src="latex5.png"> to 1. We say that the propagator <IMG alt="x+y<z" src="latex15.png"> <EM>constrains</EM> the variables <IMG alt="x,y" src="latex21.png"> and <IMG alt="z" src="latex22.png">.</P><P></P><DIV class="apropos"><P class="margin">Computation Space</P><P> Computation in Oz takes place in so-called <EM>computation spaces</EM>. For the purpose of the tutorial it is sufficient to consider a computation space as consisting of the <EM>constraint store</EM> and <EM>propagators</EM> connected to the store. </P></DIV></DIV><DIV id="u_basic_concepts.impprop"><H3><A name="u_basic_concepts.impprop">1.1.2 Implementation of Propagators</A></H3><P>The computational model sketched in <A href="node2.html#u_basic_concepts.computation">Section 1.1.1</A> is realised by the Oz runtime system, which is implemented by an abstract machine <A href="bib.html#absmachine">[MM95]</A>, called the <EM>emulator</EM>. In this section, the internal structure of propagators and their interaction with the emulator is explained. </P><P>A propagator exists in different execution states and has to be provided with resources like computation time and heap memory by the emulator. A propagator synchronises on the constraint store and may amplify it with basic constraints.</P><P>A propagator <EM>reads</EM> the basic constraints of its parameters. In the process of constraint propagation it <EM>writes</EM> basic constraints to the store.</P><P>The emulator <EM>resumes</EM> a propagator when the store has been amplified in a way the propagator is waiting for. For example, many propagators will be resumed only in case the bounds of a domain have been narrowed. </P><P class="margin">Handling Propagators</P><P> A propagator is created by the execution of an Oz program. To resume a propagator if one of its parameters is further constrained, one has to attach the propagator somehow to the parameters. To this end, a reference to the propagator is added to so-called <EM>suspension lists</EM> of the propagator's parameters; we say, a propagator is <EM>suspending</EM> on its parameters. </P><P>A resumed propagator returns a value of the predefined type <CODE>OZ_Return</CODE>:</P><P><CODE> enum OZ_Return {OZ_ENTAILED<SPAN class="keyword">,</SPAN> OZ_FAILED<SPAN class="keyword">,</SPAN> OZ_SLEEP}</CODE> </P><P>In order to schedule propagators, the emulator maintains for each propagator an execution state, namely <CODE>running</CODE>, <CODE>runnable</CODE>, <CODE>sleeping</CODE>, <CODE>entailed</CODE>, and <CODE>failed</CODE>. The emulator's scheduler switches a propagator between the execution states as shown in <A href="node2.html#propagatorstates">Figure 1.1</A>.</P><P>When a propagator is created, its state is immediately set <CODE>running</CODE> and the scheduler allocates a time slice for its first run. After every run, when the constraint propagation was performed, the emulator evaluates the propagator's return value. </P><DIV id="propagatorstates"><HR><P><A name="propagatorstates"></A></P><DIV align="center"><IMG alt="" src="propagatorstates.gif" id="propagatorstates.pic"></DIV><P class="caption"><STRONG>Figure 1.1:</STRONG> Propagator states and the transitions between them</P><HR></DIV><P> The value <CODE>OZ_FAILED</CODE> is returned if the propagator (according to its operational semantics) detects its inconsistency with the store. The emulator sets the propagator's execution state to <CODE>failed</CODE> and the computation is aborted. The propagator will be ignored by the emulator until it is eventually disposed by the next garbage collection. </P><P>The return value <CODE>OZ_ENTAILED</CODE> indicates that the propagator has detected its entailment by the constrained store, i. e. it cannot further amplify the constraint store. The emulator sets the propagator's execution state to <CODE>entailed</CODE>. It happens the same as for a failed propagator: it will be ignored until it is disposed by garbage collection.</P><P>If the propagator can neither detect inconsistency nor entailment, it returns <CODE>OZ_SLEEP</CODE>. Because the propagator may amplify the store in the future, it remains in the suspension lists. Its execution state is set to <CODE>sleeping</CODE>.</P><P>A propagator is resumed when the domain of at least one of its parameters is further narrowed. In this case, the emulator scans the suspension list of that variable and either deletes entries where the propagator's execution state is <CODE>failed</CODE> resp. <CODE>entailed</CODE> or switches the execution state of the corresponding propagator to <CODE>runnable</CODE>. This is indicated by transition (1) in <A href="node2.html#propagatorstates">Figure 1.1</A>. Now, the scheduler takes care of the propagator and will schedule it later on (the transition (2) from <CODE>runnable</CODE> to <CODE>running</CODE> is subject to the scheduler's policy and will be not discussed here).</P><P>The parameters of a propagator are stored in its state. Hence, reading and writing of basic constraints is done by the propagator itself. If a propagator constrains a variable according to its operational semantics, it informs the emulator that the corresponding suspension lists have to be scanned. </P></DIV></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node1.html">- Up -</A></TD><TD><A href="node3.html#u_getting_started">Next >></A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~tmueller/">Tobias Müller</A><BR><SPAN class="version">Version 1.4.0 (20110908185330)</SPAN></ADDRESS></BODY></HTML>
|