personal_site/_thesis/6_Appendices/A.3_Lattice_Generation.html
2023-01-25 16:04:40 +00:00

126 lines
12 KiB
HTML
Raw Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

---
title: Lattice Generation
excerpt:
layout: none
image:
---
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
<head>
<meta charset="utf-8" />
<meta name="generator" content="pandoc" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<title>Lattice Generation</title>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
"HTML-CSS": {
linebreaks: { automatic: true, width: "container" }
}
});
</script>
<script src="/assets/mathjax/tex-mml-svg.js" id="MathJax-script" async></script>
<script src="/assets/js/thesis_scrollspy.js"></script>
<script src="https://d3js.org/d3.v5.min.js" defer></script>
<link rel="stylesheet" href="/assets/css/styles.css">
<script src="/assets/js/index.js"></script>
</head>
<body>
<!--Capture the table of contents from pandoc as a jekyll variable -->
{% capture tableOfContents %}
<br>
<nav aria-label="Table of Contents" class="page-table-of-contents">
<ul>
<li><a href="#app-lattice-generation" id="toc-app-lattice-generation">Lattice Generation</a>
<ul>
<li><a href="#graph-representation" id="toc-graph-representation">Graph Representation</a></li>
<li><a href="#encoding-edge-colouring-problems-as-sat-instances" id="toc-encoding-edge-colouring-problems-as-sat-instances">Encoding edge-colouring problems as SAT instances</a></li>
</ul></li>
<li><a href="#bibliography" id="toc-bibliography">Bibliography</a></li>
</ul>
</nav>
{% endcapture %}
<!-- Give the table of contents to header as a variable so it can be put into the sidebar-->
{% include header.html extra=tableOfContents %}
<main>
<!-- Table of Contents -->
<!-- <nav id="TOC" role="doc-toc">
<ul>
<li><a href="#app-lattice-generation" id="toc-app-lattice-generation">Lattice Generation</a>
<ul>
<li><a href="#graph-representation" id="toc-graph-representation">Graph Representation</a></li>
<li><a href="#encoding-edge-colouring-problems-as-sat-instances" id="toc-encoding-edge-colouring-problems-as-sat-instances">Encoding edge-colouring problems as SAT instances</a></li>
</ul></li>
<li><a href="#bibliography" id="toc-bibliography">Bibliography</a></li>
</ul>
</nav>
-->
<!-- Main Page Body -->
<div id="page-header">
<p>Appendices</p>
<hr />
</div>
<section id="app-lattice-generation" class="level1">
<h1>Lattice Generation</h1>
<section id="graph-representation" class="level2">
<h2>Graph Representation</h2>
<p>Three key pieces of information allow us to represent amorphous lattices. The majority of the graph connectivity is encoded by an ordered list of edges <span class="math inline">\((i,j)\)</span>. These are ordered to represent both directed and undirected graphs. This is useful for defining the sign of bond operators <span class="math inline">\(u_{ij} = - u_{ji}\)</span>.</p>
<p>Information about the embedding of the lattice onto the torus is encoded into a point on the unit square associated with each vertex. The torus is unwrapped onto the square by defining an arbitrary pair of cuts along the major and minor axes. For simplicity, we take these axes to be the lines <span class="math inline">\(x = 0\)</span> and <span class="math inline">\(y = 0\)</span>. We can wrap the unit square back up into a torus by identifying the lines <span class="math inline">\(x = 0\)</span> with <span class="math inline">\(x = 1\)</span> and <span class="math inline">\(y = 0\)</span> with <span class="math inline">\(y = 1\)</span>.</p>
<p>Finally, we need to encode the topology of the graph. This is necessary because, if we are simply given an edge <span class="math inline">\((i, j)\)</span> we do not know how the edge gets from vertex i to vertex j. One method would be taking the shortest path, but it could also go the long way around by crossing one of the cuts. To encode this information, we store an additional vector <span class="math inline">\(\vec{r}\)</span> associated with each edge. <span class="math inline">\(r_i^x = 0\)</span> means that edge i does not cross the x. <span class="math inline">\(r_i^x = +1\)</span> (<span class="math inline">\(-1\)</span>) means it crossed the cut in a positive (negative) sense.</p>
<p>This description of the lattice has a very nice relationship to Blochs theorem. Applying Blochs theorem to a periodic lattice essentially means wrapping the unit cell onto a torus. Variations that happen at longer length scales than the size of the unit cell are captured by the crystal momentum. The crystal momentum inserts a phase factor <span class="math inline">\(e^{i \vec{q}\cdot\vec{r}}\)</span> onto bonds that cross to adjacent unit cells. The vector <span class="math inline">\(\vec{r}\)</span> is exactly what we use to encode the topology of our lattices.</p>
<figure>
<img src="/assets/thesis/amk_chapter/methods/bloch.png" id="fig-bloch" data-short-caption="Bloch&#39;s Theorem and the Torus" style="width:100.0%" alt="Figure 1: Blochs theorem can be thought of as transforming from a periodic Hamiltonian on the plane to the unit cell defined on a torus. In addition we get some phase factors e^{i\vec{k}\cdot\vec{r}} associated with bonds that cross unit cells that depend on the sense in which they do so \vec{r} = (\pm1, \pm1). Representing graphs on the torus turns out to require a similar idea, we unwrap the torus to one unit cell and keep track of which bonds cross the cell boundaries." />
<figcaption aria-hidden="true">Figure 1: Blochs theorem can be thought of as transforming from a periodic Hamiltonian on the plane to the unit cell defined on a torus. In addition we get some phase factors <span class="math inline">\(e^{i\vec{k}\cdot\vec{r}}\)</span> associated with bonds that cross unit cells that depend on the sense in which they do so <span class="math inline">\(\vec{r} = (\pm1, \pm1)\)</span>. Representing graphs on the torus turns out to require a similar idea, we unwrap the torus to one unit cell and keep track of which bonds cross the cell boundaries.</figcaption>
</figure>
</section>
<section id="encoding-edge-colouring-problems-as-sat-instances" class="level2">
<h2>Encoding edge-colouring problems as SAT instances</h2>
<figure>
<img src="/assets/thesis/amk_chapter/methods/times/times.svg" id="fig-times" data-short-caption="Computation Time Spent on Different Procedures." style="width:100.0%" alt="Figure 2: The proportion of computation time taken up by the four longest running steps when generating a lattice. For larger systems, the time taken to perform the diagonalisation dominates." />
<figcaption aria-hidden="true">Figure 2: The proportion of computation time taken up by the four longest running steps when generating a lattice. For larger systems, the time taken to perform the diagonalisation dominates.</figcaption>
</figure>
<p>In the main text we discuss the problem of three-edge-colouring, assigning one of three labels to each edge of a graph such that no edges of the same label meet at a vertex. To solve this in practice I use a solver called <code>MiniSAT</code> <span class="citation" data-cites="imms-sat18"> [<a href="#ref-imms-sat18" role="doc-biblioref">1</a>]</span>. Like most modern SAT solvers, <code>MiniSAT</code> requires the input problem to be specified in Conjunctive Normal Form (CNF). CNF requires that the constraints be encoded as a set of <em>clauses</em> of the form</p>
<p><span class="math display">\[x_1 \;\textrm{or}\; -x_3 \;\textrm{or}\; x_5,\]</span></p>
<p>that contain logical ORs of some subset of the variables where any of the variables may also be logically NOTd, which we represent by negation here. A solution of the problem is one that makes all the clauses simultaneously true.</p>
<p>I encode the edge colouring problem by assigning <span class="math inline">\(3B\)</span> boolean variables to each of the <span class="math inline">\(B\)</span> edges of the graph, <span class="math inline">\(x_{i\alpha}\)</span> where <span class="math inline">\(x_{i\alpha} = 1\)</span> indicates that edge <span class="math inline">\(i\)</span> has colour <span class="math inline">\(\alpha\)</span>. For edge colouring graphs we need two types of constraints: 1. Each edge is exactly one colour. 2. No neighbouring edges are the same colour.</p>
<p>The first constraint is a product of doing this mapping to boolean variables. The solver does not know anything about the structure of the problem unless it is encoded into the variables. Lets say we have three variables that correspond to particular edge being red <span class="math inline">\(r\)</span>, green <span class="math inline">\(g\)</span> or blue <span class="math inline">\(b\)</span>. To require that exactly one of the variables be true, we can enforce that no pair of variables be true: <code>-(r and b) -(r and g) -(b and g)</code></p>
<p>However, these clauses are not in CNF form. Therefore, we also have to use the fact that <code>-(a and b) = (-a OR -b)</code>. To enforce that at least one of these is true we simply OR them all together <code>(r or b or g)</code></p>
<p>To encode the fact that no adjacent edges can have the same colour, we emit a clause that, for each pair of adjacent edges, they cannot be both red, both green or both blue.</p>
<p>We get a solution or set of solutions from the solver, which we can map back to a labelling of the edges.</p>
<p>The solution presented here works well enough for our purposes. It does not take up a substantial fraction of the overall computation time, see +fig:times but other approaches could likely work.</p>
<p>When translating problems to CNF form, there is often some flexibility. For instance, we used three boolean variables to encode the colour of each edge and then additional constraints to require that only one of these variables be true. An alternative method which we did not try would be to encode the label of each edge using two variables, yielding four states per edge, and then add a constraint that one of the states, say (true, true) is disallowed. This would, however, have added some complexity to the encoding of the constraint that no adjacent edges can have the same colour.</p>
<p>The popular <em>Networkx</em> Python library uses a greedy graph colouring algorithm. It simply iterates over the vertices/edges/faces of a graph and assigns them a colour that is not already disallowed. This does not work for our purposes because it is not designed to look for a particular n-colouring. However, it does include the option of using a heuristic function that determine the order in which vertices will be coloured <span class="citation" data-cites="kosowski2004classical matulaSmallestlastOrderingClustering1983"> [<a href="#ref-kosowski2004classical" role="doc-biblioref">2</a>,<a href="#ref-matulaSmallestlastOrderingClustering1983" role="doc-biblioref">3</a>]</span>. Perhaps</p>
<p>Next Section: <a href="../6_Appendices/A.4_Lattice_Colouring.html">Lattice Colouring</a></p>
</section>
</section>
<section id="bibliography" class="level1 unnumbered">
<h1 class="unnumbered">Bibliography</h1>
<div id="refs" class="references csl-bib-body" role="doc-bibliography">
<div id="ref-imms-sat18" class="csl-entry" role="doc-biblioentry">
<div class="csl-left-margin">[1] </div><div class="csl-right-inline">A. Ignatiev, A. Morgado, and J. Marques-Silva, <em><a href="https://doi.org/10.1007/978-3-319-94144-8_26">PySAT: A Python Toolkit for Prototyping with SAT Oracles</a></em>, in <em>SAT</em> (2018), pp. 428437.</div>
</div>
<div id="ref-kosowski2004classical" class="csl-entry" role="doc-biblioentry">
<div class="csl-left-margin">[2] </div><div class="csl-right-inline">A. Kosowski and K. Manuszewski, <em>Classical Coloring of Graphs</em>, Contemporary Mathematics <strong>352</strong>, 1 (2004).</div>
</div>
<div id="ref-matulaSmallestlastOrderingClustering1983" class="csl-entry" role="doc-biblioentry">
<div class="csl-left-margin">[3] </div><div class="csl-right-inline">D. W. Matula and L. L. Beck, <em><a href="https://doi.org/10.1145/2402.322385">Smallest-Last Ordering and Clustering and Graph Coloring Algorithms</a></em>, J. ACM <strong>30</strong>, 417 (1983).</div>
</div>
</div>
</section>
</main>
</body>
</html>