/usr/share/mozart/doc/fdt/node3.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 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>2.1 Finite Domains and Constraints</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="node2.html">- Up -</A></TD><TD><A href="node4.html#section.constraints.propagation">Next >></A></TD></TR></TABLE><DIV id="section.constraints.constraints"><H2><A name="section.constraints.constraints">2.1 Finite Domains and Constraints</A></H2><P>A <A name="label10"></A><EM>finite domain</EM> is a finite set of nonnegative integers. The notation <IMG alt="m\# n" src="latex13.png"> stands for the finite domain <IMG alt="m,\ldots,n" src="latex14.png">. </P><P>A <A name="label11"></A><EM>constraint</EM> is a formula of predicate logic. Here are typical examples of constraints occurring with finite domain problems: </P><BLOCKQUOTE><P><IMG alt="\begin{array}{rcl}
&X=67
\qquad
X\in0\#9
\qquad
X=Y\\
&X^2-Y^2=Z^2
\qquad
X+Y+Z<U
\qquad
X+Y\neq5\cdot Z\\
&X_1,\ldots,X_9\;\hbox{are pairwise distinct}
\end{array}" src="latex15.png"></P></BLOCKQUOTE><P> </P><DIV class="apropos"><P class="margin">domain constraints</P><P> A <A name="label12"></A><EM>domain constraint</EM> takes the form <IMG alt="x\in D" src="latex16.png">, where <IMG alt="D" src="latex1.png"> is a finite domain. Domain constraints can express constraints of the form <IMG alt="x=n" src="latex17.png"> since <IMG alt="x=n" src="latex17.png"> is equivalent to <IMG alt="x\in n\#n" src="latex18.png">. </P></DIV><DIV class="apropos"><P class="margin">basic constraints</P><P> A <A name="label13"></A><EM>basic constraint</EM> takes one of the following forms: <IMG alt="x=n" src="latex17.png">, <IMG alt="x=y" src="latex19.png">, or <IMG alt="x\in D" src="latex16.png">, where <IMG alt="D" src="latex1.png"> is a finite domain. </P></DIV><DIV class="apropos"><P class="margin">finite domain problems</P><P> A <A name="label14"></A><EM>finite domain problem</EM> is a finite set <IMG alt="P" src="latex20.png"> of quantifier-free constraints such that <IMG alt="P" src="latex20.png"> contains a domain constraint for every variable occurring in a constraint of <IMG alt="P" src="latex20.png">. A <A name="label15"></A><EM>variable assignment</EM> is a function mapping variables to integers. </P></DIV><DIV class="apropos"><P class="margin">solutions</P><P> A <A name="label16"></A><EM>solution</EM> of a finite domain problem <IMG alt="P" src="latex20.png"> is a variable assignment that satisfies every constraint in <IMG alt="P" src="latex20.png">. </P></DIV><P>Notice that a finite domain problem has at most finitely many solutions, provided we consider only variables that occur in the problem (since the problem contains a finite domain constraint for every variable occurring in it). </P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node2.html">- Up -</A></TD><TD><A href="node4.html#section.constraints.propagation">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>
|