diff --git a/examples/csp1.lp b/examples/csp1.lp new file mode 100644 index 00000000..b5965f85 --- /dev/null +++ b/examples/csp1.lp @@ -0,0 +1,3 @@ +&dom{-3..3} = a. +&dom{-3..3} = b. +&minimize{3*a-b}. diff --git a/examples/csp2.lp b/examples/csp2.lp new file mode 100644 index 00000000..1c35960e --- /dev/null +++ b/examples/csp2.lp @@ -0,0 +1,4 @@ +&dom{0..1} = x. +&dom{0..1} = y. +{a}. +&sum{x; -1*y} < 0 :- a. diff --git a/examples/csp3.lp b/examples/csp3.lp new file mode 100644 index 00000000..a22a1599 --- /dev/null +++ b/examples/csp3.lp @@ -0,0 +1,3 @@ +&dom{0..1} = x. +&dom{0..1} = y. +a :- &sum{x; -1*y} < 0. diff --git a/examples/csp4.lp b/examples/csp4.lp new file mode 100644 index 00000000..6a76f23f --- /dev/null +++ b/examples/csp4.lp @@ -0,0 +1,13 @@ +machine(1). machine(2). +task(a). duration(a,1,3). duration(a,2,4). +task(b). duration(b,1,1). duration(b,2,6). +task(c). duration(c,1,5). duration(c,2,5). + +% jobs start at zero and must finish before a given bound +&dom { 0..B } = (J,M) :- duration(J,M,T), B=bound-T. + +% a job has to be finished on a machine before starting on the next one. +&sum{ (J,M)+T } <= (J,M+1) :- duration(J,M,T), machine(M+1). + +% the processing times of two jobs must not overlap on a machine +&disjoint { (J,M)@T : duration(J,M,T) } :- machine(M). diff --git a/guide.ind b/guide.ind deleted file mode 100644 index 3f013614..00000000 --- a/guide.ind +++ /dev/null @@ -1,167 +0,0 @@ -\begin{theindex} - - \item aggregate, \hyperpage{30} - \subitem average, \code{\#avg}, \hyperpage{120} - \subitem body, \hyperpage{31} - \subitem condition, \hyperpage{28} - \subitem count, \code{\#count}, \hyperpage{31} - \subitem even, \code{\#even}, \hyperpage{120} - \subitem head, \hyperpage{32} - \subitem maximum, \code{\#max}, \hyperpage{31} - \subitem minimum, \code{\#min}, \hyperpage{31} - \subitem odd, \code{\#odd}, \hyperpage{120} - \subitem sum plus, \code{\#sum+}, \hyperpage{31} - \subitem sum, \code{\#sum}, \hyperpage{31} - \item arithmetic function, \hyperpage{24} - \subitem absolute value, \mbox{\textbar$\cdot$\textbar}, - \hyperpage{24} - \subitem addition, \code{+}, \hyperpage{24} - \subitem bitwise and, \code{\&}, \hyperpage{24} - \subitem bitwise complement, \code{\textasciitilde}, \hyperpage{24} - \subitem bitwise or, \code{?}, \hyperpage{24} - \subitem bitwise xor, \code{\^}, \hyperpage{24} - \subitem division, \code{/}, \hyperpage{24} - \subitem exponentiation, \code{**}, \hyperpage{24} - \subitem modulo, \code{\textbackslash}, \hyperpage{24} - \subitem multiplication, \code{*}, \hyperpage{24} - \subitem subtraction, \code{-}, \hyperpage{24} - \subitem unary minus, \code{-}, \hyperpage{24} - \item atom, \hyperindexformat{\seealso{literal}}{19}, \hyperpage{19} - \subitem \gobblecomma, \hyperindexformat{\see{aggregate}}{30} - \subitem Boolean constant, \hyperpage{24} - \subitem \gobblecomma, - \hyperindexformat{\see{comparison predicate}}{25} - \subitem \gobblecomma, \hyperindexformat{\see{pooling}}{28} - - \indexspace - - \item comparison predicate, \hyperpage{25} - \subitem greater or equal, \code{>=}, \hyperpage{25} - \subitem greater, \code{>}, \hyperpage{25} - \subitem inequality, \code{!=}, \hyperpage{25} - \subitem less or equal, \code{<=}, \hyperpage{25} - \subitem less, \code{<}, \hyperpage{25} - \item conditional literal, \hyperpage{28} - - \indexspace - - \item domain predicate, \hyperpage{30} - - \indexspace - - \item external function, \hyperpage{39} - - \indexspace - - \item heuristic predicate, \hyperpage{85} - \subitem \code{factor}, \hyperpage{89} - \subitem \code{false}, \hyperpage{87} - \subitem \code{init}, \hyperpage{89} - \subitem \code{level}, \hyperpage{86} - \subitem \code{sign}, \hyperpage{85} - \subitem \code{true}, \hyperpage{87} - - \indexspace - - \item literal, \hyperindexformat{\seealso{atom}}{19}, \hyperpage{19} - \subitem conditional, \hyperpage{28} - \subitem head, \hyperpage{23} - \item logic program, \hyperpage{19} - \subitem disjunctive, \hyperpage{22} - \subitem normal, \hyperpage{19} - \item lua, \hyperpage{39} - - \indexspace - - \item meta-statement, \hyperpage{42} - \subitem comment, \hyperpage{43} - \subitem const, \code{\#const}, \hyperpage{44} - \subitem external, \code{\#external}, \hyperpage{44} - \subitem \gobblecomma, \hyperindexformat{\see{optimization}}{38} - \subitem program part, \code{\#program}, \hyperpage{45} - \subitem show, \code{\#show}, \hyperpage{43} - - \indexspace - - \item negation, \hyperindexformat{\seealso{literal}}{19} - \subitem classical, \hyperpage{21} - \subitem default, \hyperpage{19} - \subitem double, \hyperpage{23} - - \indexspace - - \item optimization, \hyperpage{37} - \subitem maximize, \code{\#maximize}, \hyperpage{37} - \subitem minimize, \code{\#minimize}, \hyperpage{37} - \subitem optimization directive, \hyperpage{97} - \subitem preference program, \hyperpage{107} - \subitem preference specification, \hyperpage{97} - \subsubitem preference element, \hyperpage{97} - \subsubitem preference statement, \hyperpage{97} - \subsubitem weighted formula, \hyperpage{97} - \subitem \gobblecomma, - \hyperindexformat{\see{preference type}}{100} - \subitem weak constraint, \hyperpage{37} - - \indexspace - - \item pooling, \code{;}, \hyperpage{28} - \item preference type, \hyperpage{100} - \subitem \code{and}, \hyperpage{106} - \subitem \code{aso}, \hyperpage{101} - \subitem \code{cp}, \hyperpage{101} - \subitem \code{less(cardinality)}, \hyperpage{101} - \subitem \code{less(weight)}, \hyperpage{101} - \subitem \code{lexico}, \hyperpage{106} - \subitem \code{maxmin}, \hyperpage{101} - \subitem \code{minmax}, \hyperpage{101} - \subitem \code{more(cardinality)}, \hyperpage{101} - \subitem \code{more(weight)}, \hyperpage{101} - \subitem \code{neg}, \hyperpage{106} - \subitem \code{pareto}, \hyperpage{106} - \subitem \code{poset}, \hyperpage{101} - \subitem \code{subset}, \hyperpage{101} - \subitem \code{superset}, \hyperpage{101} - \item python, \hyperpage{39} - - \indexspace - - \item rule - \subitem disjunctive, \hyperpage{22} - \subitem fact, \hyperpage{19} - \subitem integrity constraint, \hyperpage{19} - \subitem normal, \hyperpage{19} - - \indexspace - - \item safety, \hyperpage{21} - \subitem aggregate, \hyperpage{35} - \subitem arithmetic function, \hyperpage{25} - \subitem comparison predicate, \hyperpage{27} - \subitem external, \code{\#external}, \hyperpage{45} - \subitem interval, \hyperpage{27} - \subitem maximize, \code{\#maximize}, \hyperpage{38} - \subitem minimize, \code{\#minimize}, \hyperpage{38} - \subitem preference statement, \hyperpage{99} - \subitem show, \code{\#show}, \hyperpage{44} - \subitem weak constraint, \hyperpage{38} - - \indexspace - - \item term, \hyperpage{17} - \subitem \code{\#inf}, \hyperpage{17} - \subitem \code{\#sup}, \hyperpage{17} - \subitem anonymous variable, \hyperpage{17} - \subitem \gobblecomma, - \hyperindexformat{\see{arithmetic function}}{24} - \subitem constant, \hyperpage{17} - \subitem \gobblecomma, - \hyperindexformat{\see{external function}}{39} - \subitem function, \hyperpage{17} - \subitem integer, \hyperpage{17}, \hyperpage{24} - \subitem interval, \hyperpage{27} - \subitem \gobblecomma, \hyperindexformat{\see{pooling}}{28} - \subitem string, \hyperpage{17} - \subitem variable, \hyperpage{17} - -\end{theindex} diff --git a/guide.tex b/guide.tex index c0b1b8a5..5040688c 100644 --- a/guide.tex +++ b/guide.tex @@ -8,7 +8,7 @@ \usepackage{listings} \usepackage[dvipsnames]{xcolor} \usepackage[pdfborder={0 0 0},pagebackref=true]{hyperref} -%\usepackage{comments} +\usepackage{comments} \usepackage{pict2e} \usepackage{tikz} \usetikzlibrary{arrows,chains,positioning,automata,decorations,shapes} diff --git a/theory.tex b/theory.tex index 5f6ca126..dea85b94 100644 --- a/theory.tex +++ b/theory.tex @@ -660,15 +660,216 @@ \subsection{ASP and Constraint Programming}\label{sec:constraint} \subsubsection{ASP and Constraint Programming with \clingcon} \label{sec:clingcon} -\begin{itemize} -\item URL: \url{http://potassco.org/clingcon} -\item Literature: \cite{bakaossc16a} -\item Description: \clingoM{LP} - \begin{itemize} - \item deals with integer variables - \item uses propagators for lazy constraint propagation (based on the order-encoding) - \end{itemize} -\end{itemize} +The \clingcon{} system provides a way to integrate constraints over integer variables, into ASP. +Its main focus is on linear constraints, but other constraints such as $distinct$ and $disjoint$ are also supported. +It uses lazy constraint propagation and utilizes lazy variable creation based on the order-encoding to be able to handle huge domains explicitly. +A formal introduction of \clingcon{} is given in \cite{bakaossc16a}. +% +The following description is conform with the $\clingcon\ 5.5.0$ system available at \url{https://github.com/potassco/clingcon}. +% +The following constraints are support by \clingcon. + +\paragraph{Domain Constraints} have the form +\code{\&dom\text{ }\{$v_1$;\dots;$v_n$\}\text{ }=\text{ }$x$} where $v_i$ is either a constant expression% +\footnote{A term that can be evaluated to an integer during grounding.} +or of the form $l$..$u$ where $l$ and $u$ are constant expressions defining the lower and upper bound of a range, for $1\leq i\leq n$. +This construct constrains the domain of integer variable $x$ to the union of the given values and ranges. +E.g.~\code{\&dom\text{ }\{$1$..$3$;$5$;$7$..$9$\}\text{ }=\text{ }$x$} constrains $x$ to be in domain $\{1,2,3,5,7,8,9\}$. +Domain constraints are only allowed to occur in the head of rules. + +\paragraph{Linear Constraints} have the form +\code{\&sum\text{ }\{$e_1$;\text{ }\dots;\text{ }$e_{n-1}$\}\text{ }$\rhd$\text{ }$e_n$} +where $e_i$ is an expressions, for $1\leq i\leq n$, +and $\rhd \in \{\code{<=},\code{<},\code{>=},\code{>},\code{=},\code{!=}\}$. +An expressions $e_i$ can be any linear constraint of the form $w_1$*$x_1$ $\circ$ \text{ }\dots $\circ$ \text{ }$w_m$*$x_m$ +with $\circ \in \{\code{+}, \code{-}\}$. +The weight $w_j$ is a constant expression that can be omitted if it is equal to $1$. +The term $x_j$ represents a variable, and can be omitted to express a constant in the linear expression. +If the values of the variables $x_j$ satisfy the constraint $e_1+\dots+e_{n-1} \rhd e_{n}$, +for $1\leq j\leq m$, the constraint must be true, and false otherwise. +Linear constraints can occur anywhere in a rule. +E.g.~\code{\&sum\text{ }\{a-3*b;x+y\}\text{ }=\text{ }2*z+3*w} is a constraint according to the definition. + +\paragraph{Distinct constraints} have the form +\code{\&distinct\text{ }\{$e_1$;\text{ }\dots;\text{ }$e_n$\}} and constrain the values of all expressions +$e_i$ to be distinct, for $1\leq i\leq n$. +Distinct constraints are only allowed to occur as facts in the logic program. +E.g.~\code{\&distinct\text{ }\{a;3*b;a-b\}} ensures that \code{a}, \code{3*b}, and \code{a-b} all evaluate to different values. + +\paragraph{Disjoint constraints} have the form +\code{\&disjoint\text{ }\{$v_1$@$d_1$;\text{ }\dots;\text{ }$v_n$@$d_1$\}} and constrain the values of all variables +$v_i$ and its integer durations $d_i$ to be disjoint, for $1\leq i\leq n$. +This constraint is equivalent to the conjunction of the expressions $(v_i+d_i < v_j) \lor (v_j+d_j < v_i)$ for all $1\leq i \leq j \leq n$. +Distinct constraints are only allowed to occur as facts in the logic program. +The following example encodes a flow shop problem using the distinct constraint. +\lstinputlisting{examples/csp4.lp} + + +\paragraph{Optimization constraints} have either the form +\code{\&minimize\text{ }\{$e_1$;\text{ }\dots;\text{ }$e_n$\}} or +\code{\&maximize\text{ }\{$e_1$;\text{ }\dots;\text{ }$e_n$\}} +and minimize/maximize the values of all expressions $e_i$, +for $1\leq i\leq n$. +Optimize constraints are only allowed to occur as facts in the logic program. +\begin{example}\label{ex:lp:csp1} +Consider the following optimize constraint: +\lstinputlisting{examples/csp1.lp} +Calling the system with the example produces following output: +\marginlabel{ + To inspect the output, invoke:\\ + \code{\mbox{~}clingcon \attach{examples/csp1.lp}{csp1.lp}} \\ +} +\begin{lstlisting}[numbers=none] +... +Answer: 9 + +Assignment: +a=-3 b=2 +Cost: -11 +Answer: 10 + +Assignment: +a=-3 b=3 +Cost: -12 +SATISFIABLE +... +\end{lstlisting} +\clingcon{} successively produces better answers with respect to the optimize statement. +The last answer produced is the optimal solution to the problem. +\end{example} +It is not recommended to mix Boolean and CSP optimization statements, as the results are implementation defined. + +\subsubsection{Modeling and Solving with \clingcon} +In practice, it is often useful to declare the domain of variables when modeling a problem. +% +To describe the domain of a variable +one could use two linear constraint atoms as follows: +\begin{align*} +&\code{\&sum\text{ }\{$x$\}\text{ }>=\text{ }$l$}\\ +&\code{\&sum\text{ }\{$x$\}\text{ }<=\text{ }$u$} +\end{align*} +where $l$ and $u$ represent reals and $x$ is a variable name. +% +Alternatively we are allowed to specify the domain of a variable by using the shorthand +\[ +\code{\&dom\text{ }\{$l$..$u$\}\text{ }=\text{ }$x$} +\] + +The solutions produced by the system will include each valid assignment to each integer variable that is +used in a ground constraint. +Variables that occur in a constraint (independent of its truth value in the answer set) that are not +restricted by any constraints are automatically restricted by the system to the range $maxint..minint$. +These values can be configured using the options of the \clingcon{} system. + +Note that truth value of a constraint is determined from outside the logic program. +This means that constraints that only occur in the body of a rule also become true, +if the values of its variables satisfy the constraint. + +\begin{example}\label{ex:lp:csp2} +Let us consider the following program: +\lstinputlisting{examples/csp2.lp} +Calling the system with the example produces following output: +\marginlabel{ + To inspect the output, invoke:\\ + \code{\mbox{~}clingcon \attach{examples/csp2.lp}{csp2.lp} 0} \\ +} +\begin{lstlisting}[numbers=none] +... +Answer: 1 + +Assignment: +x=0 y=0 +Answer: 2 + +Assignment: +x=0 y=1 +Answer: 3 + +Assignment: +x=1 y=0 +Answer: 4 + +Assignment: +x=1 y=1 +Answer: 5 +a +Assignment: +x=0 y=1 +SATISFIABLE +... +\end{lstlisting} +There are four answer sets where \code{a} is false. +Therefore, all combinations of values from the domains of the variables \code{x} and \code{y} are possible. +The fifth answer contains \code{a}, +and the only possible assignment to the integer variables is \code{x=0} and \code{y=1}, +as they are constrained by the constraint \code{\&sum\text{ }\{x; -1*y\}\text{ }<\text{ }0}. +% +Since \code{a} was set to false in the first answer set, +there was no linear constraint to be solved by the underlying constraint solver, +still an enumeration of all variables occuring in the ground program is done. +% +\end{example} + +\begin{example}\label{ex:lp:csp3} +Now consider an example with a constraint in the body of a rule: +\lstinputlisting{examples/csp3.lp} +Calling the system with the example produces the following output: +\marginlabel{ + To inspect the output, invoke:\\ + \code{\mbox{~}clingcon \attach{examples/csp3.lp}{csp3.lp} 0} \\ +} +\begin{lstlisting}[numbers=none] +... +Answer: 1 + +Assignment: +x=0 y=0 +Answer: 2 + +Assignment: +x=1 y=0 +Answer: 3 + +Assignment: +x=1 y=1 +Answer: 4 +a +Assignment: +x=0 y=1 +SATISFIABLE +... +\end{lstlisting} +There are again 4 possible combinations for the assignment of the integer variables \code{x} and \code{y}. +The first three answers do not satisfy the constraint \code{\&sum\text{ }\{x; -1*y\}\text{ }<\text{ }0}, and therefore \code{a} is not contained in the answer set. +Given the valuation in the fourth answer, +the constraint is actually satisfied, directly deriving \code{a}. +\end{example} + +\subsubsection{Advanced Options of \clingcon}\label{sec:clingcon:advanced} + +This is an incomplete list of options to configure \clingcon. +We restricted ourselves to options that drastically influence the search behaviour. + +\paragraph{\texttt{--translate-clauses=[,]}} enables translation of linear constraints prior to solving. +Setting \texttt{n} restricts the preprocessor to only translate constraints that can be translated using at most \texttt{n} clauses. +The additional parameter \texttt{m} stops translation to clauses once \texttt{m} clauses have been created. + +\paragraph{\texttt{--[no-]literals-only}} ensures that only order literals are created during translation but no clauses are added. + +\paragraph{\texttt{--translate-pb=}} enables translation of linear constraints to pseudo Boolean constraints, if less than \texttt{n} order literals are needed per constraint. +\comment{I changed this option, open PR} + +\paragraph{\texttt{--translate-distinct=}} forces the translation of $distinct$ constraint to pseudo Boolean constraints, if less than \texttt{n} pseudo Boolean constraints are needed per $distinct$ constraint. + +\paragraph{\texttt{--translate-opt=}} enables the translation of the \code{\&minimize}/\code{\&maximize} constraints to clasp internal optimization constraints, if less than \texttt{n} literals are needed for the translation. +Translating optimization statements can be advantageous in combination with \clingo's option \texttt{--opt-strategy=usc} to allow for different optimization strategies. + +\paragraph{\texttt{--[no-]add-order-clauses}} adds all binary order clauses needed for the integer variables before solving. + +\paragraph{\texttt{--sign-value=}} influences the strategy which values are assigned first to an integer variable. While \texttt{+}/\texttt{-} tend to assign larger/smaller numbers, +and integer \texttt{n} can be used to steer variable assignment to this value. + +\paragraph{\texttt{--min-int=}} and \texttt{--max-int=} sets the default domain of integer variables to $l..u$ if no specific domain is given in the program. \subsubsection{ASP and Constraint Programming with \gringo}