doc/CODD.html

<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<!-- 2024-08-19 Mon 11:58 -->
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>C++DDOopt : The CODD Solver</title>
<meta name="author" content="Laurent Michel" />
<meta name="generator" content="Org Mode" />
<link rel="stylesheet" type="text/css" href="https://fniessen.github.io/org-html-themes/src/readtheorg_theme/css/htmlize.css"/>
<link rel="stylesheet" type="text/css" href="https://fniessen.github.io/org-html-themes/src/readtheorg_theme/css/readtheorg.css"/>
<script src="https://ajax.googleapis.com/ajax/libs/jquery/2.1.3/jquery.min.js"></script>
<script src="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.4/js/bootstrap.min.js"></script>
<script type="text/javascript" src="https://fniessen.github.io/org-html-themes/src/lib/js/jquery.stickytableheaders.min.js"></script>
<script type="text/javascript" src="https://fniessen.github.io/org-html-themes/src/readtheorg_theme/js/readtheorg.js"></script>
<style type="text/css">
pre.src:hover:before { display: none; }
</style>
<script>
  window.MathJax = {
    tex: {
      ams: {
        multlineWidth: '85%'
      },
      tags: 'ams',
      tagSide: 'right',
      tagIndent: '.8em'
    },
    chtml: {
      scale: 1.0,
      displayAlign: 'center',
      displayIndent: '0em'
    },
    svg: {
      scale: 1.0,
      displayAlign: 'center',
      displayIndent: '0em'
    },
    output: {
      font: 'mathjax-modern',
      displayOverflow: 'overflow'
    }
  };
</script>

<script
  id="MathJax-script"
  async
  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js">
</script>
</head>
<body>
<div id="content" class="content">
<h1 class="title">C++DDOopt : The CODD Solver</h1>
<div id="table-of-contents" role="doc-toc">
<h2>Table of Contents</h2>
<div id="text-table-of-contents" role="doc-toc">
<ul>
<li><a href="#org3ec3c33">1. Introduction</a>
<ul>
<li><a href="#org0d8efc4">1.1. What is <b>CODD</b>?</a></li>
<li><a href="#orge51648f">1.2. Dynamic Programming as a Computational Model</a>
<ul>
<li><a href="#org0454217">1.2.1. Exact Decision Diagrams</a></li>
<li><a href="#org3a3ec05">1.2.2. Restricted Decision Diagrams</a></li>
<li><a href="#orgab5b715">1.2.3. Relaxed Decision Diagrams</a></li>
</ul>
</li>
<li><a href="#org2833cd9">1.3. <b>CODD</b> Modeling</a>
<ul>
<li><a href="#orgc706806">1.3.1. TSP Example High Level</a></li>
<li><a href="#orgdf0259b">1.3.2. TSP Example in <b>CODD</b></a></li>
</ul>
</li>
<li><a href="#org0962cc5">1.4. <b>CODD</b> Solving</a></li>
</ul>
</li>
<li><a href="#orgef98ce8">2. Installing CODD</a>
<ul>
<li><a href="#org483e01b">2.1. Download</a></li>
<li><a href="#orgcdba51e">2.2. Compilation</a>
<ul>
<li><a href="#org003185e">2.2.1. Dependencies</a></li>
<li><a href="#org5edca69">2.2.2. C++ Standard</a></li>
<li><a href="#org0c8f8b3">2.2.3. Build system</a></li>
<li><a href="#orge23d76f">2.2.4. Unit tests</a></li>
<li><a href="#orgfd7b0f3">2.2.5. Library</a></li>
</ul>
</li>
<li><a href="#orgee60d9a">2.3. Examples</a></li>
</ul>
</li>
<li><a href="#org1d2344f">3. The Maximum Independent Set Problem (MISP)</a>
<ul>
<li><a href="#orgc9ab23d">3.1. Preamble</a></li>
<li><a href="#org4785a9c">3.2. Reading the instance</a></li>
<li><a href="#orgf4e64b2">3.3. State definition</a></li>
<li><a href="#org69587b7">3.4. Main Model</a>
<ul>
<li><a href="#org9c34c3e">3.4.1. Getting started</a></li>
<li><a href="#orgaa5301e">3.4.2. The Bound Tracker</a></li>
<li><a href="#org73bff9d">3.4.3. Defining neighbors</a></li>
<li><a href="#orgb6066fb">3.4.4. The actual CODD Model</a></li>
</ul>
</li>
</ul>
</li>
<li><a href="#org6476352">4. Papers</a>
<ul>
<li><a href="#org9d1380f">4.1. CODD</a></li>
</ul>
</li>
<li><a href="#org679490b">5. Related Systems</a>
<ul>
<li><a href="#org92841f9">5.1. DDO</a></li>
<li><a href="#org7b5ee8f">5.2. Domain Independent DP</a></li>
<li><a href="#org6a6630c">5.3. Peel &amp; Bound</a></li>
</ul>
</li>
</ul>
</div>
</div>
<div id="outline-container-org3ec3c33" class="outline-2">
<h2 id="org3ec3c33"><span class="section-number-2">1.</span> Introduction</h2>
<div class="outline-text-2" id="text-1">
</div>
<div id="outline-container-org0d8efc4" class="outline-3">
<h3 id="org0d8efc4"><span class="section-number-3">1.1.</span> What is <b>CODD</b>?</h3>
<div class="outline-text-3" id="text-1-1">
<p>
<b>CODD</b> is a system for modeling and solving combinatorial optimization problems using decision diagram technology. Problems are represented as state-based dynamic programming models using the CODD language specification.  The model specification is used to automatically compile relaxed and restricted decision diagrams, as well as to guide the search process. <b>CODD</b> introduces abstractions that allow to generically implement the solver components while maintaining overall execution efficiency.  We demonstrate the functionality of <b>CODD</b> on a variety of combinatorial optimization problems and compare its performance to other state-based solvers as well as integer programming and constraint programming solvers.
</p>

<p>
We consider discrete optimization problems of the form
</p>

\begin{array}{rl}
P : ~~ \max & f(y)\\
\textrm{s.t.} & C_j(y), j = 1, \dots, m,\\
& y \in D
\end{array}

<p>
where \(y=(y_1,\ldots,y_n)\) is a tuple of decision variables, \(f\) is a real-valued objective function over \(y\) and \(C_1,\ldots,C_m\) are constraints over \(y\) with \(D=D_1 \times \ldots \times D_n\) denoting the  cartesian product of the domains of the variables \(y_i\) (\(1 \leq i \leq n\)).
</p>
</div>
</div>
<div id="outline-container-orge51648f" class="outline-3">
<h3 id="orge51648f"><span class="section-number-3">1.2.</span> Dynamic Programming as a Computational Model</h3>
<div class="outline-text-3" id="text-1-2">
<p>
Dynamic programming can be understood as a labeled transition system where sequences of state-based decisions that delivers a sequence of states \((s_1,\ldots,s_{n+1})\).
At each step \(i\), a transition \(\tau(s_i,x_i) = s_i \stackrel{x_i}{\rightarrow} s_{i+1}\) is labeled by the decision \(x_i\). Each such transition induces a cost \(c(s_i,x_i)\). The DP formulation then boils down to:
</p>
<ul class="org-ul">
<li>the definition of the state space \({\cal S}\) with \(s_i \in {\cal S}\).</li>
<li>two distinguished states \(s_\top\) and \(s_\bot\)  in \({\cal S}\) encoding, respectively, the start state for an empty sequence of decision and the sink state for the full problem</li>
<li>a label generation function \(\lambda : {\cal S} \rightarrow {\cal U}\) representing the values one can use to follow a transition out of a state \(s \in {\cal S}\).</li>
<li>The state transition function \(\tau : {\cal S} \times {\cal U} \rightarrow {\cal S}\) modeling the decisions effects</li>
<li>The transition cost function \(c : {\cal S} \times {\cal U} \rightarrow \mathbb{R}\).</li>
</ul>

<p>
The Dynamic Program over the state sequence \((s_1,\ldots,s_{n+1})\) and the decision sequence \((x_1,\ldots,x_{n})\) has the following form
</p>

\begin{array}{rll}
\max & v(t) & \\
\textrm{ s.t. } & v(s_{i+1}) = \displaystyle \max_{\substack{x_i \in \lambda(s_i)\\\tau(s_i,x_i)=s_{i+1}}} v(s_i) + c(s_i,x_i) & \forall s_i \in {\cal S} \setminus \{t\} \\
 & v(r) = K
\end{array}
<div class="important" id="orgd625a5b">
<p>
Observe how the valuation function on the root state \(r\) is the constant \(K\). Also note how the 
constraints \((C_1,\ldots,C_m)\) are captured by the state transition function \(\tau\) and the value generator \(\lambda(s_i)\) that proposes appropriate values for decision \(x_i\) out of state \(s_i\).
</p>

</div>
<p>
Clearly \(s_\top\)'s value is \(K\) and \(s_{n+1}=s_\bot\), a state satisfying all the constraints and corresponding to the full problem (all decisions were made).
The valuation function \(v\) defined by the Bellman equation above accumulates the cost incurred along each
transition and modeled by the cost function \(c\).
</p>

<p>
The path with the globally optimal cost is the global optimum to the original maximization problem \(P\). Naturally, there are potentially exponentially many such path. 
</p>
</div>
<div id="outline-container-org0454217" class="outline-4">
<h4 id="org0454217"><span class="section-number-4">1.2.1.</span> Exact Decision Diagrams</h4>
<div class="outline-text-4" id="text-1-2-1">
<p>
<b>CODD</b> provides (for generality's sake) an <i>exact</i> decision diagram that builds the state of the LTS just described and can therefore produce a globally optimal solution. While it is relatively direct, it requires the construction of an exponentially size structure and is therefore only useful as a proof of concept. Formally, the solution set of the
exact decision diagram induced by \(DD_{Exact}(P)\) is identical to the solution set of \(P\), namely \({\cal Sol}(DD_{Exact}(P)) = {\cal Sol}(P)\).
</p>
</div>
</div>
<div id="outline-container-org3a3ec05" class="outline-4">
<h4 id="org3a3ec05"><span class="section-number-4">1.2.2.</span> Restricted Decision Diagrams</h4>
<div class="outline-text-4" id="text-1-2-2">
<p>
<b>CODD</b> provides <i>restricted</i> decision diagrams. Those differ from exact diagram by discarding (during their top-down construction) nodes whose presence would lead to overflowing a maximal imposed <i>width</i>. Since the approach throws away states, and therefore <i>paths</i> it runs the risk of loosing the optimal solution. Yet, if they yield  paths leading to \(s_\bot\), the best of them is a primal bound to the original problem.
Formally, the solution set of the restricted decision diagram is a subset of the solution set of the original problem \(P\). Namely,
\({\cal Sol}(DD_{Restricted}(P)) \subseteq {\cal Sol}(P)\).
</p>
</div>
</div>
<div id="outline-container-orgab5b715" class="outline-4">
<h4 id="orgab5b715"><span class="section-number-4">1.2.3.</span> Relaxed Decision Diagrams</h4>
<div class="outline-text-4" id="text-1-2-3">
<p>
<b>CODD</b> provides <i>relaxed</i> decision diagrams. Those differ from exact diagram by <i>merging</i> states whose presence would induce a diagram <i>width</i> exceeding a given bound. The state merge operator must be a legit relaxation in the following sense: it yields a state that no longer satisfies all constraints in \((C_1,\ldots,C_m)\). While the width ensure that the size of the diagram remains under control, it <i>introduces</i> new states that are no longer satisfiable. Path leading to \(s_\bot\) going through at least one such unsatisfiable state are no longer modeling a solution of the original problem. Formally, the solution set of the relaxed diagram is now a super set of the solution set of the original problem \(P\). Namely,
\({\cal Sol}(DD_{Relaxed}(P)) \supseteq {\cal Sol}(P)\).
</p>

<p>
From the above, one gets to derive primal bounds using the restricted diagrams and dual bounds using the relaxed one.
</p>

<div class="important" id="org936902c">
<p>
Note how all three diagrams are based on the same LTS abstractions of states, labels, transitions, merge and costs and equality to \(s_\bot\). These abstractions are the core
modeling facilities offered by <b>CODD</b>. 
</p>

</div>
</div>
</div>
</div>
<div id="outline-container-org2833cd9" class="outline-3">
<h3 id="org2833cd9"><span class="section-number-3">1.3.</span> <b>CODD</b> Modeling</h3>
<div class="outline-text-3" id="text-1-3">
<p>
Unsurprisingly, the abstractions presented above match exactly with the <b>CODD</b> API that expects:
</p>
<ul class="org-ul">
<li>A structure to define a state</li>
<li>Two distinguished states \(s_\top\) and \(s_\bot\) used to represent a state with no decisions made (\(s_\top\)) and all possible decision made (\(s_\bot\)).</li>
<li>A label generation function \(\lambda\) which given a state \(s_i\), produces the set of potentially viable transitions</li>
<li>A state transition function \(\tau\) which, given a state \(s_i\) and a potentially viable label \(\ell\), produces either nothing (\(\bot\)) or a new state \(s_{i+1}\) such that
\(s_i \stackrel{x_i=\ell}{\longrightarrow} s_{i+1} \in \tau\).</li>
<li>A cost function \(c\) which, given a state \(s_i\) and a viable label \(\ell\) produces the cost of the transition \(s_i \stackrel{x_i=\ell}{\longrightarrow} s_{i+1}\)</li>
<li>An <i>optional</i> equality to \(s_\bot\) function that returns true whenever its input state <i>is</i> \(s_\bot\).</li>
</ul>

<div class="note" id="org955d84c">
<p>
An <i>optional</i> local dual bounding function which, given a state \(s_i\) compute a coarse dual bound for completing \(s_i\). <i>this optional abstraction</i> is helpful to quickly assess whether a state has any hope of leading to an improving \(s_\bot\). If a state does not, it can be discarded from the relaxation.
</p>

</div>
<p>
Thankfully, C++ is a rich language supporting polymorphic types, first order and higher order functions. Those provide the basis to naturally convey the formal abstractions given above. The <i>state</i> become a <i>type</i> in C++ and all the other abstractions becomes first-order functions (lambdas in C++ parlance).
</p>
</div>
<div id="outline-container-orgc706806" class="outline-4">
<h4 id="orgc706806"><span class="section-number-4">1.3.1.</span> TSP Example High Level</h4>
<div class="outline-text-4" id="text-1-3-1">
<p>
Consider the task of solving instances of the traveling salesman problem. With the abstraction defined above, to express a TSP over a set of cities \(V=\{1..n\}\) we define:
</p>

<ul class="org-ul">
<li>Let a state \(s \in {\cal S}\) be a triplet \(\langle S,e,h\rangle\) with \(S \subseteq V\) the set of cities visited thus far, \(e\) the name of the city last visited (or 0 at the start), and \(h\) the number of hops made thus far (or 0 at the start).</li>
<li>Let \(s_\top = \langle \{1\},1,0\rangle\) since no cities have been visited, hence last city is the
depot 1 and the salesman did not do any "hops".</li>
<li>Let \(s_\bot = \langle V,1,n\rangle\). Indeed, without loss of generality, we will start from the depot 1 and thus <i>return</i> to the depot 1 (which will thus be the last visited). The trip will have carried out \(n\) hops and visited all cities in \(V\).</li>
<li><p>
The label generator is a function \(\lambda : {\cal S} \rightarrow {\cal U}\) defined as
</p>

\begin{array}{lccl}
  \lambda(\langle S,e,h\rangle)  &=& V \setminus S & \Leftrightarrow h < n-1,\\ 
   &=&\{1\} & \Leftrightarrow h=n-1
\end{array}</li>

<li>The state transition function \(\tau : {\cal S} \times {\cal L} \rightarrow {\cal S}\) is</li>
</ul>
\begin{array}{lcll}
\tau(\langle S,e,h \rangle,\ell) &=& \langle V,\ell,n\rangle  & \Leftrightarrow \ell=1  \\
&& \langle S \cup \{\ell\},\ell,h+1\rangle & \Leftrightarrow \mbox{otherwise} 
\end{array}
<p>
The condition \(\ell=1\)  indicates a return to the depot (1).
The alternative extends the set of visited cities with \(\ell\) and adds one hop. Naturally, the cost
function is straightforwardly defined as \(c(\langle S,e,h\rangle,\ell) = d_{e,\ell}\) while the merge operator \(\oplus(\langle S_1,e_1,h_1\rangle,\langle S_2,e_2,h_2\rangle) = \langle S_1 \cup S_2,e_1,h_1\rangle\) provided that \(e_1=e_2 \wedge h_1=h_2\).
</p>
</div>
</div>
<div id="outline-container-orgdf0259b" class="outline-4">
<h4 id="orgdf0259b"><span class="section-number-4">1.3.2.</span> TSP Example in <b>CODD</b></h4>
<div class="outline-text-4" id="text-1-3-2">
<p>
Modeling with <b>CODD</b> first requires a type to represent a state. Since a state is a triplet, the model uses a <code>C</code> structure.
</p>

<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #6434A3;">TSP</span> {
   <span style="color: #6434A3;">GNSet</span>  <span style="color: #BA36A5;">s</span>;
   <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">last</span>;
   <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">hops</span>;
   <span style="color: #0000FF; font-weight: bold;">friend</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">ostream</span>&amp; <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">&lt;&lt;</span>(<span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">ostream</span>&amp; <span style="color: #BA36A5;">os</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">m</span>) {
      <span style="color: #0000FF; font-weight: bold;">return</span> os &lt;&lt; <span style="color: #008000;">"&lt;"</span> &lt;&lt; m.s &lt;&lt; <span style="color: #008000;">','</span> &lt;&lt; m.last &lt;&lt; <span style="color: #008000;">','</span> &lt;&lt; m.hops &lt;&lt; <span style="color: #008000;">"&gt;"</span>;
   }
};
</pre>
</div>
<p>
Note the additional (and optional) output operator used to inspect state.
In addition to the state, <b>CODD</b> expects 2 standard operations on state. Equality testing and hashing. Namely, 
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">template</span>&lt;&gt; <span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">equal_to</span>&lt;TSP&gt; {
   <span style="color: #0000FF; font-weight: bold;">constexpr</span> <span style="color: #6434A3;">bool</span> <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">()</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s1</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s2</span>) <span style="color: #0000FF; font-weight: bold;">const</span> {
      <span style="color: #0000FF; font-weight: bold;">return</span> s1.last == s2.last &amp;&amp; s1.hops==s2.hops &amp;&amp; s1.s == s2.s;
   }
};
</pre>
</div>
<p>
Is a STL compliant implementation of equality testing for a type <code>T</code> which, here, is none other than the <code>TSP</code> structure.
Likewise, the STL compliant fragment
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">template</span>&lt;&gt; <span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">hash</span>&lt;TSP&gt; {
   <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">size_t</span> <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">()</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">v</span>) <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">noexcept</span> {
      <span style="color: #0000FF; font-weight: bold;">return</span> (<span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">hash</span>&lt;GNSet&gt;{}(v.s) &lt;&lt; 24) |
         (<span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">hash</span>&lt;<span style="color: #6434A3;">int</span>&gt;{}(v.last) &lt;&lt; 16) |
         <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">hash</span>&lt;<span style="color: #6434A3;">int</span>&gt;{}(v.hops);
   }
};
</pre>
</div>
<p>
defines a <code>hash</code> operator for the state type <code>TSP</code>.  Both state equality and state hashing are used internally by <b>CODD</b>.
Given \(V\) a constant set holding the set of cities and \(n\) its size, 
it is now easy to define both \(s_\top\) and \(s_\bot\) with:
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">init</span> = []() {   <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">The root state</span>
   <span style="color: #0000FF; font-weight: bold;">return</span> TSP { GNSet{1},1,0 };
};
<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">target</span> = [&amp;<span style="color: #BA36A5;">V</span>,<span style="color: #D0372D;">n</span>]() {    <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">The sink state</span>
   <span style="color: #0000FF; font-weight: bold;">return</span> TSP { V,1,n };
};
</pre>
</div>
<p>
Note how the <code>init</code> and the <code>target</code> closures can be called to manufacture the desired states.
The label generation function is also defined with a simple closure
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">lgf</span> = [&amp;<span style="color: #BA36A5;">V</span>,<span style="color: #D0372D;">n</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s</span>)  {
   <span style="color: #0000FF; font-weight: bold;">if</span> (s.hops == n - 1)
      <span style="color: #0000FF; font-weight: bold;">return</span> GNSet {1};
   <span style="color: #0000FF; font-weight: bold;">else</span> 
      <span style="color: #0000FF; font-weight: bold;">return</span> V - s.s;
};
</pre>
</div>
<p>
The body of the closure uses the capture set of cities <code>V</code>
and returns a singleton with just the depot city (1) if this is the last hop or \(V \setminus s.s\) otherwise.
</p>

<p>
The function \(\tau\) is, unsurprisingly, another closure (which captures <code>n</code> and <code>V</code> denoting, respectively, the number of cities and the set of all cities.)
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">stf</span> = [&amp;<span style="color: #BA36A5;">V</span>,<span style="color: #D0372D;">n</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">label</span>) -&gt; <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">optional</span>&lt;<span style="color: #6434A3;">TSP</span>&gt; {
    <span style="color: #0000FF; font-weight: bold;">if</span> (label==1)
       <span style="color: #0000FF; font-weight: bold;">return</span> TSP { V,1,n};
    <span style="color: #0000FF; font-weight: bold;">else</span> 
       <span style="color: #0000FF; font-weight: bold;">return</span> TSP { s.s | GNSet{label},label,s.hops + 1};     
};
</pre>
</div>
<p>
The case analysis carried out in the code mirrors exactly the formal definition. If the value \(label\) indicates a return  to the depot, we return the sink state. Otherwise, we add \(label\) to the set of visited cities \(s.s\), set the last visited city as \(label\) and increase the number of hops by 1.
</p>

<p>
The cost of a transition is also modeled with a closure that captures the distance matrix \(d\) and reads:
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">scf</span> = [&amp;<span style="color: #BA36A5;">d</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s</span>,<span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">label</span>) { <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">partial cost function </span>
   <span style="color: #0000FF; font-weight: bold;">return</span> d[s.e][label];
};
</pre>
</div>
<p>
The state merge \(\oplus\) is simply:
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">smf</span> = [](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s1</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s2</span>) -&gt; <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">optional</span>&lt;<span style="color: #6434A3;">TSP</span>&gt; {
   <span style="color: #0000FF; font-weight: bold;">if</span> (s1.last == s2.last &amp;&amp; s1.hops == s2.hops) 
      <span style="color: #0000FF; font-weight: bold;">return</span> TSP {s1.s &amp; s2.s , s1.last, s1.hops};
   <span style="color: #0000FF; font-weight: bold;">else</span> <span style="color: #0000FF; font-weight: bold;">return</span> <span style="color: #D0372D;">std</span>::nullopt; <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">return  the empty optional</span>
};
</pre>
</div>
<p>
Observe how this closure takes two states \(s_1\) and \(s_2\) and considers them
mergeable if they both end in the same city and have the same number of hops. The relaxation stems from the fact that the set <i>intersection</i> between \(s_1.s\) and \(s_2.s\) will only retain cities that were visited in both.
</p>

<p>
Finally, the equality to the sink (target) state is also closure:
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">eqs</span> = [<span style="color: #D0372D;">n</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">TSP</span>&amp; <span style="color: #BA36A5;">s</span>) -&gt; <span style="color: #6434A3;">bool</span> {
   <span style="color: #0000FF; font-weight: bold;">return</span> s.last == 1 &amp;&amp; s.hops == n;
};  
</pre>
</div>
<p>
Which deems state \(s\) equal to the sink if the last city is 1 and we have the desired number of hops \(sz\). 
</p>
</div>
</div>
</div>
<div id="outline-container-org0962cc5" class="outline-3">
<h3 id="org0962cc5"><span class="section-number-3">1.4.</span> <b>CODD</b> Solving</h3>
<div class="outline-text-3" id="text-1-4">
<p>
Solving the TSP then reduces to <i>instantiating</i> the generic solver with all the closures defined earlier. Namely:
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #6434A3;">BAndB</span> <span style="color: #BA36A5;">engine</span>(<span style="color: #D0372D;">DD</span>&lt;TSP,<span style="color: #6434A3;">Minimize</span>&lt;<span style="color: #6434A3;">double</span>&gt;, <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">to minimize</span>
             <span style="color: #0000FF; font-weight: bold;">decltype</span>(target),
             <span style="color: #0000FF; font-weight: bold;">decltype</span>(lgf),
             <span style="color: #0000FF; font-weight: bold;">decltype</span>(stf),
             <span style="color: #0000FF; font-weight: bold;">decltype</span>(scf),
             <span style="color: #0000FF; font-weight: bold;">decltype</span>(smf),
             <span style="color: #0000FF; font-weight: bold;">decltype</span>(eqs)
             &gt;::makeDD(init,target,lgf,stf,scf,smf,eqs,labels),1);
engine.search(bnds);
</pre>
</div>
<p>
Note how the <code>DD</code> template is specialized with the state type <code>TSP</code>, the type
<code>Minimize&lt;double&gt;</code> to convey that this is a minimization, and the types of the various
closures using the C++-23 <code>decltype</code> operator. The solver is invoked with the last line.
</p>
<div class="important" id="org1a845cb">
<p>
<b>CODD</b> users never directly call any of those closures. Calls to the closures are
choreographed by the solver to build the diagrams and reason with them. <b>CODD</b> users are strictly focused on defining the DP LTS in a mathematical sense and then doing the 1-1 translation to C++. 
</p>

</div>
</div>
</div>
</div>
<div id="outline-container-orgef98ce8" class="outline-2">
<h2 id="orgef98ce8"><span class="section-number-2">2.</span> Installing CODD</h2>
<div class="outline-text-2" id="text-2">
</div>
<div id="outline-container-org483e01b" class="outline-3">
<h3 id="org483e01b"><span class="section-number-3">2.1.</span> Download</h3>
<div class="outline-text-3" id="text-2-1">
<p>
The CODD solver is available on <a href="https://github.com/ldmbouge/CPPddOpt">github</a>. 
</p>
</div>
</div>
<div id="outline-container-orgcdba51e" class="outline-3">
<h3 id="orgcdba51e"><span class="section-number-3">2.2.</span> Compilation</h3>
<div class="outline-text-3" id="text-2-2">
<p>
The CODD C++ library implements both the modeling and the solving framework. It extensively
relies on functional closures to deliver concise, declarative and elegant models.
It has:
</p>
<ul class="org-ul">
<li>Restricted / exact / relax diagrams</li>
<li>State definition, initial, terminal, tranistion and state merging functions separated</li>
<li>Label generation functions</li>
<li>Equivalence predicate for sink.</li>
</ul>
<p>
It allows to define model to solve problems using a dynamic programming style with the
support of underlying decision diagrams.
</p>
</div>
<div id="outline-container-org003185e" class="outline-4">
<h4 id="org003185e"><span class="section-number-4">2.2.1.</span> Dependencies</h4>
<div class="outline-text-4" id="text-2-2-1">
<p>
You need <code>graphviz</code> (The <code>dot</code> binary) to create graph images. It happens
automatically when the <code>display</code> method is called. Temporary files are created
in <code>/tmp</code> and the macOS <code>open</code> command is used (via <code>fork/execlp</code>)  to open the generated PDF. The rest of the system is vanilla C++-23 and <code>cmake</code>.
</p>
<div class="hint" id="org28e4ebd">
<p>
Keep in mind that this is optional and only needed if you wish to generate images of
diagrams (typically to debug models).
</p>

</div>
</div>
</div>
<div id="outline-container-org5edca69" class="outline-4">
<h4 id="org5edca69"><span class="section-number-4">2.2.2.</span> C++ Standard</h4>
<div class="outline-text-4" id="text-2-2-2">
<p>
You need a C++-23 capable compiler. gcc and clang should both work. I work on macOS where I use the mainline clang coming with Xcode. The implementation uses templates and concepts to factor the code.
</p>
</div>
</div>
<div id="outline-container-org0c8f8b3" class="outline-4">
<h4 id="org0c8f8b3"><span class="section-number-4">2.2.3.</span> Build system</h4>
<div class="outline-text-4" id="text-2-2-3">
<p>
This is <code>cmake</code>. Simply do the following
</p>
<div class="org-src-container">
<pre class="src src-bash">mkdir build
<span style="color: #006FE0;">cd</span> build
cmake ..
make -j4
</pre>
</div>
<p>
And it will compile the whole thing. To compile in optimized mode, simply change
the variable <code>CMAKE_BUILD_TYPE</code> from <code>Debug</code> to <code>Release</code> as shown below:
</p>
<div class="org-src-container">
<pre class="src src-bash">cmake .. -DCMAKE_BUILD_TYPE=Release
</pre>
</div>
</div>
</div>
<div id="outline-container-orge23d76f" class="outline-4">
<h4 id="orge23d76f"><span class="section-number-4">2.2.4.</span> Unit tests</h4>
<div class="outline-text-4" id="text-2-2-4">
<p>
In the <code>test</code> folder. Mostly for the low-level containers.
</p>
</div>
</div>
<div id="outline-container-orgfd7b0f3" class="outline-4">
<h4 id="orgfd7b0f3"><span class="section-number-4">2.2.5.</span> Library</h4>
<div class="outline-text-4" id="text-2-2-5">
<p>
All of it in the <code>src</code> folder.
</p>
<div class="org-src-container">
<pre class="src src-shell">scc  -i cpp,org,h,hpp ..
</pre>
</div>

<pre class="example" id="org69c2864">
───────────────────────────────────────────────────────────────────────────────
Language                 Files     Lines   Blanks  Comments     Code Complexity
───────────────────────────────────────────────────────────────────────────────
C++                         33      5068      343       311     4414        812
C++ Header                  16      3330      151       352     2827        451
Org                          3       818      100         0      718         92
───────────────────────────────────────────────────────────────────────────────
Total                       52      9216      594       663     7959       1355
───────────────────────────────────────────────────────────────────────────────
Estimated Cost to Develop (organic) $238,504
Estimated Schedule Effort (organic) 7.98 months
Estimated People Required (organic) 2.66
───────────────────────────────────────────────────────────────────────────────
Processed 303650 bytes, 0.304 megabytes (SI)
───────────────────────────────────────────────────────────────────────────────
</pre>
</div>
</div>
</div>
<div id="outline-container-orgee60d9a" class="outline-3">
<h3 id="orgee60d9a"><span class="section-number-3">2.3.</span> Examples</h3>
<div class="outline-text-3" id="text-2-3">
<p>
To be found in the <code>examples</code> folder
</p>
<ul class="org-ul">
<li><code>coloringtoy</code> tiny coloring bench (same as in python)</li>
<li><code>foo</code> maximum independent set (toy size)</li>
<li><code>tstpoy</code> tiny TSP instance (same as in python)</li>
<li><code>gruler</code> golomb ruler (usage &lt;size&gt; &lt;ubOnLabels&gt;)</li>
<li><code>misp</code> the maximum independent set problem</li>
</ul>
</div>
</div>
</div>
<div id="outline-container-org1d2344f" class="outline-2">
<h2 id="org1d2344f"><span class="section-number-2">3.</span> The Maximum Independent Set Problem (MISP)</h2>
<div class="outline-text-2" id="text-3">
<p>
It is, perhaps, most effective to look at some models
to get a reasonable sense of the effort it takes to model and
solve a problem with <b>CODD</b>. 
</p>
</div>
<div id="outline-container-orgc9ab23d" class="outline-3">
<h3 id="orgc9ab23d"><span class="section-number-3">3.1.</span> Preamble</h3>
<div class="outline-text-3" id="text-3-1">
<p>
To start using CODD, it is sufficent to include its main header as follow
</p>
<div class="org-src-container">
<pre class="src src-c++" id="orge5379cd"><span style="color: #808080;">#include</span> <span style="color: #008000;">"codd.hpp"</span>
</pre>
</div>
</div>
</div>
<div id="outline-container-org4785a9c" class="outline-3">
<h3 id="org4785a9c"><span class="section-number-3">3.2.</span> Reading the instance</h3>
<div class="outline-text-3" id="text-3-2">
<div class="org-src-container">
<pre class="src src-c++" id="org526e639"><span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #6434A3;">GE</span> {
   <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">a</span>,<span style="color: #BA36A5;">b</span>;
   <span style="color: #0000FF; font-weight: bold;">friend</span> <span style="color: #6434A3;">bool</span> <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">==</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">GE</span>&amp; <span style="color: #BA36A5;">e1</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">GE</span>&amp; <span style="color: #BA36A5;">e2</span>) {
      <span style="color: #0000FF; font-weight: bold;">return</span> e1.a == e2.a &amp;&amp; e1.b == e2.b;
   }
   <span style="color: #0000FF; font-weight: bold;">friend</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">ostream</span>&amp; <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">&lt;&lt;</span>(<span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">ostream</span>&amp; <span style="color: #BA36A5;">os</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">GE</span>&amp; <span style="color: #BA36A5;">e</span>) {
      <span style="color: #0000FF; font-weight: bold;">return</span> os  &lt;&lt; e.a &lt;&lt; <span style="color: #008000;">"--&gt;"</span> &lt;&lt; e.b;
   }
};

<span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #6434A3;">Instance</span> {
   <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">nv</span>;
   <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">ne</span>;
   <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">vector</span>&lt;<span style="color: #6434A3;">GE</span>&gt; <span style="color: #BA36A5;">edges</span>;
   <span style="color: #6434A3;">FArray</span>&lt;GNSet&gt; <span style="color: #BA36A5;">adj</span>;
   <span style="color: #006699;">Instance</span>() : adj(0) {}
   <span style="color: #006699;">Instance</span>(<span style="color: #6434A3;">Instance</span>&amp;&amp; <span style="color: #BA36A5;">i</span>) : nv(i.nv),ne(i.ne),edges(<span style="color: #D0372D;">std</span>::move(i.edges)) {}
   <span style="color: #6434A3;">GNSet</span> <span style="color: #006699;">vertices</span>() {
      <span style="color: #0000FF; font-weight: bold;">return</span> setFrom(<span style="color: #D0372D;">std</span>::<span style="color: #D0372D;">views</span>::iota(0,nv));
   }
   <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #006699;">getEdges</span>() <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">noexcept</span> { <span style="color: #0000FF; font-weight: bold;">return</span> edges;}
   <span style="color: #6434A3;">void</span> <span style="color: #006699;">convert</span>() {
      adj = FArray&lt;<span style="color: #6434A3;">GNSet</span>&gt;(nv+1);
      <span style="color: #0000FF; font-weight: bold;">for</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span>&amp; <span style="color: #BA36A5;">e</span> : edges) {
         adj[e.a].insert(e.b);
         adj[e.b].insert(e.a);
      }         
   }
};

<span style="color: #6434A3;">Instance</span> <span style="color: #006699;">readFile</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">char</span>* <span style="color: #BA36A5;">fName</span>)
{
   <span style="color: #6434A3;">Instance</span> <span style="color: #BA36A5;">i</span>;
   <span style="color: #0000FF; font-weight: bold;">using</span> <span style="color: #0000FF; font-weight: bold;">namespace</span> <span style="color: #D0372D;">std</span>;
   <span style="color: #6434A3;">ifstream</span> <span style="color: #BA36A5;">f</span>(fName);
   <span style="color: #0000FF; font-weight: bold;">while</span> (!f.eof()) {
      <span style="color: #6434A3;">char</span> <span style="color: #BA36A5;">c</span>;
      f &gt;&gt; c;
      <span style="color: #0000FF; font-weight: bold;">if</span> (f.eof()) <span style="color: #0000FF; font-weight: bold;">break</span>;
      <span style="color: #0000FF; font-weight: bold;">switch</span>(c) {
         <span style="color: #0000FF; font-weight: bold;">case</span> <span style="color: #008000;">'c'</span>: {
            <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">string</span> <span style="color: #BA36A5;">line</span>;
            <span style="color: #D0372D;">std</span>::getline(f,line);
         }<span style="color: #0000FF; font-weight: bold;">break</span>;
         <span style="color: #0000FF; font-weight: bold;">case</span> <span style="color: #008000;">'p'</span>: {
            <span style="color: #6434A3;">string</span> <span style="color: #BA36A5;">w</span>;
            f &gt;&gt; w &gt;&gt; i.nv &gt;&gt; i.ne;
         }<span style="color: #0000FF; font-weight: bold;">break</span>;
         <span style="color: #0000FF; font-weight: bold;">case</span> <span style="color: #008000;">'e'</span>: {
            <span style="color: #6434A3;">GE</span> <span style="color: #BA36A5;">edge</span>;
            f &gt;&gt; edge.a &gt;&gt; edge.b;
            edge.a--,edge.b--;      <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">make it zero-based</span>
            assert(edge.a &gt;=0);
            assert(edge.b &gt;=0);
            i.edges.push_back(edge);
         }<span style="color: #0000FF; font-weight: bold;">break</span>;
      }
   }
   f.close();
   i.convert();
   <span style="color: #0000FF; font-weight: bold;">return</span> i;
}  
</pre>
</div>

<p>
The C structure <code>GE</code> is meant to represent a <i>graph edge</i>. It inlines a friend function to print edges and an equality operator.  The C struct <code>Instance</code> is used to encapsulate
an instance of the MISP problem read from a text file. It holds the number of vertices <code>nv</code>, the number of edges <code>ne</code>, the list of <code>edges</code> and computes and holds the adjacency list <code>adj</code>. The latter is computed by the <code>convert</code> method which simply scans the edges
in <code>edges</code> and adds the endpoints in the respective sets of the adjacency vector. Note that the vertices are numbered from 0 onward (so the last vertex number is <code>nv - 1</code>). 
</p>

<p>
The <code>readFile</code>  function produces an <code>Instance</code> from a named file <code>fName</code>. Note how it shifts the vertex identifiers of edges down by 1 since the standard instances use a 1-based numbering scheme rather than a 0-based numbering scheme.
</p>
</div>
</div>
<div id="outline-container-orgf4e64b2" class="outline-3">
<h3 id="orgf4e64b2"><span class="section-number-3">3.3.</span> State definition</h3>
<div class="outline-text-3" id="text-3-3">
<div class="org-src-container">
<pre class="src src-c++" id="orgc566bff">
<span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #6434A3;">MISP</span> {
   <span style="color: #6434A3;">GNSet</span> <span style="color: #BA36A5;">sel</span>;
   <span style="color: #6434A3;">int</span>   <span style="color: #BA36A5;">n</span>;
   <span style="color: #0000FF; font-weight: bold;">friend</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">ostream</span>&amp; <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">&lt;&lt;</span>(<span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">ostream</span>&amp; <span style="color: #BA36A5;">os</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">m</span>) {
      <span style="color: #0000FF; font-weight: bold;">return</span> os &lt;&lt; <span style="color: #008000;">"&lt;"</span> &lt;&lt; m.sel &lt;&lt; <span style="color: #008000;">','</span> &lt;&lt; m.n &lt;&lt; <span style="color: #008000;">','</span> &lt;&lt; <span style="color: #008000;">"&gt;"</span>;
   }
};

<span style="color: #0000FF; font-weight: bold;">template</span>&lt;&gt; <span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">equal_to</span>&lt;<span style="color: #6434A3;">MISP</span>&gt; {
   <span style="color: #6434A3;">bool</span> <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">()</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s1</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s2</span>) <span style="color: #0000FF; font-weight: bold;">const</span> {
      <span style="color: #0000FF; font-weight: bold;">return</span> s1.n == s2.n &amp;&amp; s1.sel == s2.sel;         
   }
};

<span style="color: #0000FF; font-weight: bold;">template</span>&lt;&gt; <span style="color: #0000FF; font-weight: bold;">struct</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">hash</span>&lt;<span style="color: #6434A3;">MISP</span>&gt; {
   <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">size_t</span> <span style="color: #0000FF; font-weight: bold;">operator</span><span style="color: #006699;">()</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">v</span>) <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">noexcept</span> {
      <span style="color: #0000FF; font-weight: bold;">return</span> <span style="color: #D0372D;">std</span>::rotl(<span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">hash</span>&lt;<span style="color: #6434A3;">GNSet</span>&gt;{}(v.sel),32) ^ <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">hash</span>&lt;<span style="color: #6434A3;">int</span>&gt;{}(v.n);
   }
};
</pre>
</div>
<p>
The <code>MISP</code> struct defines the state representation for the DP model. For the <i>maximum independent set problem</i> the state is simply a set of integers named <code>sel</code> and an
integer <code>n</code> representing the index of the next vertex to consider for inclusion (or exclusion) from the independent set. The next two classe are standard C++ and define the following:
</p>
<ul class="org-ul">
<li><code>std::equal_to&lt;MISP&gt;</code>: this structure conforms to the STL and defines as equality operator over the state <code>MISP</code></li>
<li><p>
<code>sth::hash&lt;MISP&gt;</code>: this structure conforms to the STL and defines a hash function for
</p>

<p>
  the state <code>MISP</code>. Note how it uses the hash functions for the <code>int</code> type and the
<code>GNSet</code> types provided by the STL or the <code>CODD</code> library.
</p></li>
</ul>
</div>
</div>
<div id="outline-container-org69587b7" class="outline-3">
<h3 id="org69587b7"><span class="section-number-3">3.4.</span> Main Model</h3>
<div class="outline-text-3" id="text-3-4">
</div>
<div id="outline-container-org9c34c3e" class="outline-4">
<h4 id="org9c34c3e"><span class="section-number-4">3.4.1.</span> Getting started</h4>
<div class="outline-text-4" id="text-3-4-1">
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #6434A3;">int</span> <span style="color: #006699;">main</span>(<span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">argc</span>,<span style="color: #6434A3;">char</span>* <span style="color: #BA36A5;">argv</span>[])
{
   <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">using STL containers for the graph</span>
   <span style="color: #0000FF; font-weight: bold;">if</span> (argc &lt; 2) {
      <span style="color: #D0372D;">std</span>::cout &lt;&lt; <span style="color: #008000;">"usage: coloring &lt;fname&gt; &lt;width&gt;\n"</span>;
      exit(1);
   }
   <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">char</span>* <span style="color: #BA36A5;">fName</span> = argv[1];
   <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">w</span> = argc==3 ? atoi(argv[2]) : 64;
   <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">instance</span> = readFile(fName);

   <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">GNSet</span> <span style="color: #BA36A5;">ns</span> = instance.vertices();
   <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">top</span> = ns.size();
   <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">vector</span>&lt;GE&gt; <span style="color: #BA36A5;">es</span> = instance.getEdges();

   <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">labels</span> = ns | GNSet { top };     <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">using a plain set for the labels</span>
   <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">vector</span>&lt;<span style="color: #6434A3;">int</span>&gt; <span style="color: #BA36A5;">weight</span>(ns.size()+1);
   weight[top] = 0;
   <span style="color: #0000FF; font-weight: bold;">for</span>(<span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">v</span> : ns) weight[v] = 1;
   ...
</pre>
</div>

<p>
The <code>main</code> program simply gets the filename from the command line and reads the
instance from the file. It then extract in <code>ns</code> the set of vertices, in <code>top</code> its cardinality and in <code>es</code> the list of edges. The last four lines define the <code>labels</code> to be used (the identifier of all vertices together with <code>top</code> to encode the transition to the final state in  the decision diagram). They also define the weights of the
vertices. Since the instances are cliques (from the DIMACS challenge), the <code>weight</code> of every vertex is 1 while the <code>weight</code> of <code>top</code> is 0.
</p>
</div>
</div>
<div id="outline-container-orgaa5301e" class="outline-4">
<h4 id="orgaa5301e"><span class="section-number-4">3.4.2.</span> The Bound Tracker</h4>
<div class="outline-text-4" id="text-3-4-2">
<p>
The maximum independent set is an optimization (maximization) problem. CODD needs to track solutions as they get produces and offers the opportunity to execute an arbitrary code fragment when a new solution somes forth. This code fragment can be used, for instance, to check the correctness of the solution. 
</p>

<p>
This task is the responsibility of the <code>Bounds</code> object. Minimally, one simply must declare an instance as follows:
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #6434A3;">Bounds</span> <span style="color: #BA36A5;">bnds</span>;
</pre>
</div>

<div class="attention" id="org18e5306">
<p>
In the MISP example, we illustrate how to respond to incoming solutions. In this case the <code>Bounds</code> instance uses a C++ lambda (a closure) that will be fed a solution <code>inc</code>, i.e., a vector of labels.
</p>

</div>

<p>
Consider the example below:
</p>
<div class="org-src-container">
<pre class="src src-c++">Bounds <span style="color: #6434A3;">bnds</span>([&amp;<span style="color: #BA36A5;">es</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">vector</span>&lt;<span style="color: #6434A3;">int</span>&gt;&amp; <span style="color: #BA36A5;">inc</span>)  {
   <span style="color: #6434A3;">bool</span> <span style="color: #BA36A5;">ok</span> = <span style="color: #D0372D;">true</span>;    
   <span style="color: #0000FF; font-weight: bold;">for</span>(<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span>&amp; <span style="color: #BA36A5;">e</span> : es) {         
      <span style="color: #6434A3;">bool</span> <span style="color: #BA36A5;">v1In</span> = (e.a &lt; (<span style="color: #6434A3;">int</span>)inc.size()) ? inc[e.a] : <span style="color: #D0372D;">false</span>;
      <span style="color: #6434A3;">bool</span> <span style="color: #BA36A5;">v2In</span> = (e.b &lt; (<span style="color: #6434A3;">int</span>)inc.size()) ? inc[e.b] : <span style="color: #D0372D;">false</span>;
      <span style="color: #0000FF; font-weight: bold;">if</span> (<span style="color: #6434A3;">v1In</span> &amp;&amp; <span style="color: #BA36A5;">v2In</span>) {
         <span style="color: #D0372D;">std</span>::cout &lt;&lt; e &lt;&lt; <span style="color: #008000;">" BOTH ep in inc: "</span> &lt;&lt; inc &lt;&lt; <span style="color: #008000;">"\n"</span>;
         assert(<span style="color: #D0372D;">false</span>);
      }
      ok &amp;= !(<span style="color: #6434A3;">v1In</span> &amp;&amp; <span style="color: #BA36A5;">v2In</span>);
   }
   <span style="color: #D0372D;">std</span>::cout &lt;&lt; <span style="color: #008000;">"CHECKER is "</span> &lt;&lt; ok &lt;&lt; <span style="color: #008000;">"\n"</span>;
});
</pre>
</div>
<p>
The closure first <i>captures</i> the set of edges (by reference) as checking the validity of a solution simply entails looping over all edges and making sure that not both endpoints of an edge are included in the solution. The <code>for</code> loop binds <code>e</code> to an edge and, provided that the endpoints are mentioned in the solution, looks up the Boolean associated to the vertex in the solution. Note how the solution <code>inc</code> can be a prefix of the full vertex list (hence the conditional expression). If both endpoints are mentionned in the solution, the computation is aborted as this would indicate a bug in the model. 
</p>
</div>
</div>
<div id="outline-container-org73bff9d" class="outline-4">
<h4 id="org73bff9d"><span class="section-number-4">3.4.3.</span> Defining neighbors</h4>
<div class="outline-text-4" id="text-3-4-3">
<p>
The main model will make use of the adjacency list, so it is advisable to hold into
a variable <code>neighbors</code> the adjacency list for the graph.
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">neighbors</span> = instance.adj;
</pre>
</div>
</div>
</div>
<div id="outline-container-orgb6066fb" class="outline-4">
<h4 id="orgb6066fb"><span class="section-number-4">3.4.4.</span> The actual CODD Model</h4>
<div class="outline-text-4" id="text-3-4-4">
<p>
A CODD model capture a label transition system (LTS). This LTS operates on nodes holding states for the problem. In the case of the maximum independent set, the states are <code>MISP</code> instances. The LTS starts from a <i>source</i> node and forms paths that ultimately target a <i>sink</i> state. A path in the LTS moves from state to state by <i>generating labels</i> and  using a <i>transition</i> function. Each such transition can incur a <i>cost</i>.
</p>

<p>
The CODD solver uses a branch &amp; bound strategy with both a primal and a dual bound. Primal bounds are produced as a matter of course each time an incumbent solution is found, but also through  the used of <b>restricted decision diagrams</b>. Likewise, dual bounds are produced by <b>relaxed decision diagrams</b>. Such relaxed diagrams rely on
<i>merge</i>  operations to collapse state.
</p>

<p>
CODD models all the italicized concepts outlined in the prior paragraphs with C++ closures. The remainder of this section presents them, one at a time.
</p>
</div>
<ol class="org-ol">
<li><a id="org39d0aec"></a>The Start State Closure<br />
<div class="outline-text-5" id="text-3-4-4-1">
<p>
The root, start or source state in the MISP application simly holds in the <code>sel</code> property of the state the indices of all legal vertices and holds in <code>n</code> the value 0 to report that the next decision is to be about vertex 0.  Note how the code below
uses the STL <code>std::views::iota</code> to loop over the closed range [0,top] and insert each value <code>i</code> in the set <code>U</code>  that is then used to create and return the root state.
</p>

<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">myInit</span> = [<span style="color: #D0372D;">top</span>]() {   <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">The root state</span>
    <span style="color: #6434A3;">GNSet</span> <span style="color: #BA36A5;">U</span> = {}; 
    <span style="color: #0000FF; font-weight: bold;">for</span>(<span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">i</span> : <span style="color: #D0372D;">std</span>::<span style="color: #D0372D;">views</span>::iota(0,top))
       U.insert(i);
    <span style="color: #0000FF; font-weight: bold;">return</span> MISP { U , 0};
 };
</pre>
</div>
</div>
</li>
<li><a id="orgb9d85d9"></a>The Sink State Closure<br />
<div class="outline-text-5" id="text-3-4-4-2">
<p>
The sink state is chosen, by convention, to hold an empty set for the remaining legal vertices (so no more decision beyond this point) and <code>top</code> as the next vertex to consider since top is the index of the last vertex plus 1. Note how the closure capture the <code>top</code> local variable.
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">myTarget</span> = [<span style="color: #D0372D;">top</span>]() {    <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">The sink state</span>
   <span style="color: #0000FF; font-weight: bold;">return</span> MISP { GNSet {},top};
};
</pre>
</div>
</div>
</li>
<li><a id="org5720b39"></a>The Label Generation Closure<br />
<div class="outline-text-5" id="text-3-4-4-3">
<p>
Moving from one state to the next involves making a decision about the next vertex to be consider for inclusion. Observe that the identity of that vertex is held in the <code>n</code> property of the state we are departing. The decision, in this case, is a binary choice. Either we include <code>n</code> or we do not. So the label generation function
returns the closed range [0,1] as the valid outgoing labels. Note how the closure takes as input the source state <code>s</code> (yet, for the MISP model, the source state is not used for any purposes.).
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">lgf</span> = [](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s</span>)  {
   <span style="color: #0000FF; font-weight: bold;">return</span> <span style="color: #D0372D;">Range</span>::close(0,1);
}; 
</pre>
</div>
</div>
</li>
<li><a id="org7f4b63e"></a>The State transition Closure<br />
<div class="outline-text-5" id="text-3-4-4-4">
<p>
the state transition closure is the heart of the model. It specifies what state to go to when leaving <code>s</code> through label <code>label</code>. Observe that <code>s</code> dictates which vertex to consider in <code>s.n</code>. Two cases arise:
</p>
<ul class="org-ul">
<li>\(s.n \geq top\) In this situation, we ran out of vertices. If the remaining legal set is empty (\(s.sel = \emptyset\)) then we ought to transition to the sink as we are closing a viable path. Otherwise, this is a "dead-end" and the code return nothing (<code>std::nullopt</code>) as the API uses the C++ optional type to convey the absence of a transition.</li>
<li>\(s.n < top\) In this situation, we can decide to include <code>s.n</code> in the MISP provided that it is still legal (i.e., provided that \(s.n \in s.sel\)).
The first line of the second case therefore commits to not transitioning whenever
\(s.n \notin s.sel \wedge label=True\) and thus return <code>std::nullopt</code>. Otherwise, <code>s.n</code> is eligible (because it is either to be excluded, or it is still legal) and the new state is computed. The new state \(out = s.sel \setminus N(s.n) \setminus \{s.n\}\) where \(N(s.n)\) refers to the neighbors of \(s.n\).  The <code>diffWith</code> method implements the set difference calculation. Finally, the result state holds <code>out</code> and sets the next vertex to consider to be \(top\) if \(out = \emptyset\) or \(s.n + 1\) otherwise.</li>
</ul>

<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">myStf</span> = [<span style="color: #D0372D;">top</span>,&amp;<span style="color: #BA36A5;">neighbors</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">label</span>) -&gt; <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">optional</span>&lt;<span style="color: #6434A3;">MISP</span>&gt; {
    <span style="color: #0000FF; font-weight: bold;">if</span> (s.n &gt;= top) {
       <span style="color: #0000FF; font-weight: bold;">if</span> (s.sel.empty()) 
          <span style="color: #0000FF; font-weight: bold;">return</span> MISP { GNSet {}, top};
       <span style="color: #0000FF; font-weight: bold;">else</span> <span style="color: #0000FF; font-weight: bold;">return</span> <span style="color: #D0372D;">std</span>::nullopt;
    } <span style="color: #0000FF; font-weight: bold;">else</span> {
       <span style="color: #0000FF; font-weight: bold;">if</span> (!s.sel.contains(s.n) &amp;&amp; label) <span style="color: #0000FF; font-weight: bold;">return</span> <span style="color: #D0372D;">std</span>::nullopt; 
       <span style="color: #6434A3;">GNSet</span> <span style="color: #BA36A5;">out</span> = s.sel;
       out.remove(s.n);   <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">remove n from state</span>
       <span style="color: #0000FF; font-weight: bold;">if</span> (label) out.diffWith(neighbors[s.n]); 
       <span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">bool</span> <span style="color: #BA36A5;">empty</span> = out.empty();  <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">find out if we are done!</span>
       <span style="color: #0000FF; font-weight: bold;">return</span> MISP { <span style="color: #D0372D;">std</span>::move(out),empty ? top : s.n + 1}; <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">build state accordingly</span>
    }
 };
</pre>
</div>
</div>
</li>
<li><a id="org6a8257f"></a>The transition Cost Closure<br />
<div class="outline-text-5" id="text-3-4-4-5">
<p>
Each transition from a state to another incurs a cost based on the source state and the label used to transition out. CODD once again relies on a closure to report this cost. In the code fragment below, note how the closure capture a reference to the <code>weight</code> vector and uses the identity of the vertex being labeled <code>s.n</code> as well as the <code>label</code> itself  (a 0/1 value) to compute and return the actual cost.
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">scf</span> = [&amp;<span style="color: #BA36A5;">weight</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s</span>,<span style="color: #6434A3;">int</span> <span style="color: #BA36A5;">label</span>) { <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">cost function </span>
   <span style="color: #0000FF; font-weight: bold;">return</span> label * weight[s.n];
};
</pre>
</div>
</div>
</li>
<li><a id="org46a28b3"></a>The State Merge Closure<br />
<div class="outline-text-5" id="text-3-4-4-6">
<p>
CODD computes its dual bound with a relaxation that <i>merges</i> state. The implementation uses a closure which, given two states \(s_1\) and \(s_2\) determines
whether the two states are mergeable and returns a new state if they are, or the
<code>std::nullopt</code> optional if they are not.
</p>

<p>
In the MISP case, states are always mergeable and the merge result is none other
than the union of the two eligible sets of vertices and the minimum identifier for the next vertex. In the code below the C++ operator <code>|</code> conveys the union of the
two sets.
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">smf</span> = [](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s1</span>,<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s2</span>) -&gt; <span style="color: #D0372D;">std</span>::<span style="color: #6434A3;">optional</span>&lt;<span style="color: #6434A3;">MISP</span>&gt; {
   <span style="color: #0000FF; font-weight: bold;">return</span> MISP {s1.sel | s2.sel,<span style="color: #D0372D;">std</span>::min(s1.n,s2.n)};
};
</pre>
</div>
</div>
</li>
<li><a id="orgced9e87"></a>Local Bound Closure<br />
<div class="outline-text-5" id="text-3-4-4-7">
<div class="caution" id="orgcc7c41b">
<p>
CODD can use an <i>optional</i> closure to quickly compute dual bounds associated to
states of the LTS. The optional <code>local</code> closure is therefore typically lightweight.
</p>

</div>
<p>
In the case of MISP, a simple dual bound consist of summing up the weight of all the vertices that are still eligible. This is clearly an overestimate as some of these vertices will be ruled out. But it's cheap to compute!
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">local</span> = [&amp;<span style="color: #BA36A5;">weight</span>](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s</span>) -&gt; <span style="color: #6434A3;">double</span> {
   <span style="color: #0000FF; font-weight: bold;">return</span> sum(s.sel,[&amp;<span style="color: #BA36A5;">weight</span>](<span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">v</span>) { <span style="color: #0000FF; font-weight: bold;">return</span> weight[v];});
};      
</pre>
</div>
</div>
</li>
<li><a id="orgc3f1ce8"></a>Recognizing the Sink<br />
<div class="outline-text-5" id="text-3-4-4-8">
<p>
CODD uses one last (mandatory) closure to establish equality to the sink. It does not rely on the equality operator as recognizing the sink may not require to test all its attributes for equality, but only a subset of them.
</p>
<div class="org-src-container">
<pre class="src src-c++"><span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #0000FF; font-weight: bold;">auto</span> <span style="color: #BA36A5;">eqs</span> = [](<span style="color: #0000FF; font-weight: bold;">const</span> <span style="color: #6434A3;">MISP</span>&amp; <span style="color: #BA36A5;">s</span>) -&gt; <span style="color: #6434A3;">bool</span> {
   <span style="color: #0000FF; font-weight: bold;">return</span> s.sel.size() == 0;
};
</pre>
</div>
</div>
</li>
<li><a id="org1a5b2a6"></a>Wrapping up<br />
<div class="outline-text-5" id="text-3-4-4-9">
<p>
Now that all the mandatory (and optional) closures are defined, it only remains to
instantiate the generic solver with the closures given above and invoke it.
</p>

<div class="hint" id="orgd8e7765">
<p>
The type <code>Maximize&lt;double&gt;</code> is used to convey that this is a maximization problem
while the nested <code>double</code> type is the type used to track the objective function value and is currently always <code>double</code>. CODD supports <code>Minimize&lt;double&gt;</code> as well.
</p>

</div>

<div class="org-src-container">
<pre class="src src-c++">  <span style="color: #6434A3;">BAndB</span> <span style="color: #006699;">engine</span>(<span style="color: #D0372D;">DD</span>&lt;MISP,<span style="color: #6434A3;">Maximize</span>&lt;<span style="color: #6434A3;">double</span>&gt;, <span style="color: #8D8D84;">// </span><span style="color: #8D8D84; font-style: italic;">to maximize</span>
               <span style="color: #0000FF; font-weight: bold;">decltype</span>(myTarget), 
               <span style="color: #0000FF; font-weight: bold;">decltype</span>(lgf),
               <span style="color: #0000FF; font-weight: bold;">decltype</span>(myStf),
               <span style="color: #0000FF; font-weight: bold;">decltype</span>(scf),
               <span style="color: #0000FF; font-weight: bold;">decltype</span>(smf),
               <span style="color: #0000FF; font-weight: bold;">decltype</span>(eqs),
               <span style="color: #0000FF; font-weight: bold;">decltype</span>(local)
               &gt;::makeDD(myInit,myTarget,lgf,myStf,scf,smf,eqs,labels,local),w);
  engine.search(bnds);
  <span style="color: #0000FF; font-weight: bold;">return</span> 0;
}
</pre>
</div>
</div>
</li>
</ol>
</div>
</div>
</div>
<div id="outline-container-org6476352" class="outline-2">
<h2 id="org6476352"><span class="section-number-2">4.</span> Papers</h2>
<div class="outline-text-2" id="text-4">
</div>
<div id="outline-container-org9d1380f" class="outline-3">
<h3 id="org9d1380f"><span class="section-number-3">4.1.</span> CODD</h3>
<div class="outline-text-3" id="text-4-1">
<p>
CODD: A Decision Diagram-based Solver for Combinatorial Optimization, <a href="https://www.ecai2024.eu/programme/preliminary-schedule">ECAI24</a>, 27TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 19-24 OCTOBER 2024,Santiago de Compostela. L. Michel &amp; W.J. van Hoeve.
</p>
</div>
</div>
</div>
<div id="outline-container-org679490b" class="outline-2">
<h2 id="org679490b"><span class="section-number-2">5.</span> Related Systems</h2>
<div class="outline-text-2" id="text-5">
</div>
<div id="outline-container-org92841f9" class="outline-3">
<h3 id="org92841f9"><span class="section-number-3">5.1.</span> DDO</h3>
<div class="outline-text-3" id="text-5-1">
<p>
<a href="https://github.com/xgillard/ddo">DDO</a> was created by Pierre Schauss and Xavier Gillard.
It is a generic and efficient framework for MDD-based optimization written in Rust.
</p>
</div>
</div>
<div id="outline-container-org7b5ee8f" class="outline-3">
<h3 id="org7b5ee8f"><span class="section-number-3">5.2.</span> Domain Independent DP</h3>
<div class="outline-text-3" id="text-5-2">
<p>
<a href="https://arxiv.org/abs/2401.13883">DIDP</a> is the brainchild of Ryo Kuroiwa, J. Christopher Beck. It can be found <a href="https://didp.ai">here</a> and offers
both a modeling and a solving API for dynamic programming.
</p>
</div>
</div>
<div id="outline-container-org6a6630c" class="outline-3">
<h3 id="org6a6630c"><span class="section-number-3">5.3.</span> Peel &amp; Bound</h3>
<div class="outline-text-3" id="text-5-3">
<ul class="org-ul">
<li>Peel and Bound: Solving Discrete Optimization Problems with Decision Diagrams and Separation
Thesis at Polytechnique Montréal, Accepted August 16th, 2024. Preprint available, (2024)</li>
<li>Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams
28th International Conference on Principles and Practice of Constraint Programming (CP 2022), Volume 235, pp. 35:1-35:20, (2022) Isaac Rudich, Quentin Cappart, Louis-Martin Rousseau.
<a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.35">Peel &amp; Bound</a></li>
</ul>
</div>
</div>
</div>
</div>
<div id="postamble" class="status">
<p class="author">Author: Laurent Michel</p>
<p class="date">Created: 2024-08-19 Mon 11:58</p>
<p class="validation"><a href="https://validator.w3.org/check?uri=referer">Validate</a></p>
</div>
</body>
</html>