1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
//! # reachability_solver //! //! A linear reachability solver for directional edges //! //! WARNING: This is called "linear solver" in the sense of linear logic, //! because it uses linear solver under the hood. //! This is intended as an example for logic study. //! Do not use in production, as the runtime and memory complexity of this algorithm is //! far from optimal. //! //! This solver takes a list of pair of numbers and produces a new list of pair of numbers. //! //! For example: //! //! ```text //! [1, 2], [2, 3] => [1, 3] //! ``` //! //! With other words, it is an algorithm that tells whether a //! [maze](https://en.wikipedia.org/wiki/Maze) is solvable. //! It does this by reducing the maze to an equivalent maze that is easier to solve. //! //! ### Harry Potter and Higher Order Maze Solving //! //! *SPOILER ALERT* //! //! Such transformed mazes are interesting because they contain the "same information" //! as the more complex maze with respect to start and end positions. //! //! This transformation can be used to pre-process mazes for higher order maze solving. //! It is called "pre-language semantics" since any reasoning problem using Boolean algebra //! on the original maze can be solved using Boolean algebra on transformed maze. //! //! This idea is best illustrated using an example from the book //! [Harry Potter and the Goblet of Fire](https://en.wikipedia.org/wiki/Harry_Potter_and_the_Goblet_of_Fire). //! //! The maze in the book is very complex and changes over time (a static maze in space-time, btw), //! so I will use a much simpler example instead. //! //! In the final round of the Triwizard Tournament, Harry starts at `1` and Cedric starts at `2`. //! Both Harry and Cedric try to reach Triwizard Cup at `5`. //! We want to know whether Harry and Cedric can reach The Triwizard Cup at the same time. //! It turns out that they can, because it is reachable for both Harry and Cedric: //! //! ```text //! [1, 4], [2, 3], [3, 4], [4, 5] => [1, 5], [2, 5] //! ``` //! //! The pair `[3, 4]` represents the moment when Harry helps Cedric. //! In an alternative timeline where Harry does not help Cedric, the transformed maze becomes: //! //! ```text //! [1, 4], [2, 3], [4, 5] => [1, 5], [2, 3] //! ``` //! //! So, Cedric gets stuck in a dead end of the maze. //! //! This is a higher order maze problem, which can be expressed as following: //! //! ```text //! (Harry -> TriwizardCup) ∧ (Cedric -> TriwizardCup) //! ``` //! //! Here, the `∧` operator means logical AND. //! //! From any maze problem, one can construct a "higher order maze problem" using //! Boolean algebra on any sub-problem of the kind `A -> B`. //! These kinds of problems are harder to solve directly on the non-transformed maze, //! without knowing the details of the higher order problem. //! //! Assume that some manipulative person (I won't tell you who) //! wants Harry to reach Triwizard Cup, but not Cedric. //! One can express this goal as: //! //! ```text //! (Harry -> TriwizardCup) ∧ ¬(Cedric -> TriwizardCup) //! ``` //! //! It is possible to determine whether this is true from a transformed maze, //! without knowing the internal configurations of how space-time positions are connected. //! //! However, if the person places a magical gate that only lets the first person through in the only //! path toward the goal, then it is not possible to determine whether Harry will reach Triwizard Cup. //! One must analyze this problem using the original maze and some extra information, //! such as which path takes shorter time and how fast each wizard champion runs. //! This problem is undecidable with respect to the solver algorithm. //! //! ### Graph Theory //! //! The pair of numbers represents edges in a graph. //! The output produces a pair for every end node reachable from a start node. //! All other edges are removed, including circular edges. //! //! For more information about reachability, see the //! [Wikipedia article](https://en.wikipedia.org/wiki/Reachability). //! //! This can be used to: //! //! - Learn about maze-solving algorithms //! - Learn about linear solving through studying a simple example //! - Learn about category theory by studying a simple example //! - Study pre-language semantics (invariant inference over Boolean algebra interpretations) //! //! ### Introduction to Category Theory and Reachability //! //! A category can be thought of as a kind of graph/network with nodes and edges. //! //! - Nodes in category theory is called "objects" //! - Edges in category theory are directional and called "morphisms" //! //! Category theory is a branch of mathematics that abstracts over //! problems with similar structure, such that reasoning about these //! problems can be formulated in a common language. //! //! The following requirements holds for all categories: //! //! - Every object (node) has at least one morphism (arrow) to itself //! - If there is a morphism (arrow) `A -> B` and `B -> C`, then //! there is a morphism (arrow) `A -> C` //! //! There is no information about the nodes and edges themselves, //! only how the nodes and edges are connected. //! //! An edge `[A, B]` can be thought of as a proof that there exists //! at least one morphism `A -> B`. //! //! Every object `A` has at least one morphism `A -> A`. //! Therefore, the edge `[A, A]` is trivial. //! //! In a category there are initial and terminal objects: //! //! - An initial object has no incoming morphisms //! - A terminal object has no outgoing morphisms //! //! An edge of type `[<initial>, <terminal>]` describes the reachability //! from an initial object to a terminal object. #![deny(missing_docs)] extern crate linear_solver; use linear_solver::{solve_minimum, Inference}; use linear_solver::Inference::*; use std::collections::HashSet; /// Returns a list of edges that describes reachability /// from initial objects to terminal objects. pub fn solve(edges: Vec<[usize; 2]>) -> Vec<[usize; 2]> { solve_minimum(edges, infer) } fn infer(cache: &HashSet<[usize; 2]>, facts: &[[usize; 2]]) -> Option<Inference<[usize; 2]>> { for ea in facts { let [a, b] = ea; for eb in facts { let [c, d] = eb; if b == c { let p = [*a, *d]; if !cache.contains(&p) { return Some(Propagate(p)); } } } } let mut r = vec![]; for ea in facts { let [a, b] = ea; for eb in facts { let [c, d] = eb; if c == b || a == d { r.push(ea.clone()); } } } return Some(ManyTrue {from: r}); }