|
| 1 | +#import "theme.typ": * |
| 2 | + |
| 3 | +#import "@preview/numbly:0.1.0": numbly |
| 4 | + |
| 5 | +#let target_date = datetime(year: 2025, month: 8, day: 8) |
| 6 | +#show: lmu-theme.with( |
| 7 | + aspect-ratio: "16-9", |
| 8 | + footer: self => self.info.author, |
| 9 | + header-right: none, |
| 10 | + footer-progress: false, |
| 11 | + config-info( |
| 12 | + title: [Q - A Superposition Prover], |
| 13 | + subtitle: [Master Practical: Automated Theorem Provers], |
| 14 | + author: [Henrik Böving, Daniel Soukup], |
| 15 | + date: target_date.display("[day].[month].[year]"), |
| 16 | + institution: text(14pt, smallcaps("Ludwig-Maximilians-Universität München")), |
| 17 | + logo: image("lmu-sigillium.svg", height: 25%), |
| 18 | + ), |
| 19 | +) |
| 20 | + |
| 21 | +#title-slide() |
| 22 | + |
| 23 | += Q |
| 24 | +- A superposition prover based on @braniac with: |
| 25 | + - TPTP FOF support |
| 26 | + - basic literal selection |
| 27 | + - a few simplification rules |
| 28 | + - efficient term orderings |
| 29 | + - efficient subsumption |
| 30 | + - graphic proof display |
| 31 | +- Written in Rust |
| 32 | +- Focus on getting a high performance implementation of the basic calculus |
| 33 | + |
| 34 | += Logic |
| 35 | +We implement a basic first order logic with equality with the reductions: |
| 36 | +- $p(x) arrow.r.squiggly p(x) = top$ |
| 37 | +- $not p(x) arrow.r.squiggly p(x) != top$ |
| 38 | +Crucially to avoid: |
| 39 | +$ (forall x, y: x = y) and not p(a) "vs" (forall x, y: x = y) and p(a) != top $ |
| 40 | +we implement a 2-sorted logic with booleans and individuals |
| 41 | + |
| 42 | += Core Data Structures |
| 43 | +- Logical: |
| 44 | + - Terms |
| 45 | + - Literals |
| 46 | + - Clauses |
| 47 | +- Indexing: |
| 48 | + - Discrimination Trees |
| 49 | + - Feature Vector Index |
| 50 | + - Clause Queue |
| 51 | + |
| 52 | +== Terms |
| 53 | + |
| 54 | +#slide[ |
| 55 | +```rs |
| 56 | +enum RawTerm { |
| 57 | + Var { |
| 58 | + id: VariableIdentifier, |
| 59 | + data: TermData, |
| 60 | + }, |
| 61 | + App { |
| 62 | + id: FunctionIdentifier, |
| 63 | + args: Vec<Term>, |
| 64 | + data: TermData, |
| 65 | + }, |
| 66 | +} |
| 67 | +
|
| 68 | +type Term = HashConsed<RawTerm>; |
| 69 | +``` |
| 70 | +][ |
| 71 | +Similar to @terms: |
| 72 | +- fully shared with a term bank for meta data |
| 73 | +- RC for memory management |
| 74 | +- pre-computed values: |
| 75 | + - hash for $O(1)$ hashing $->$ $O(1)$ term caches |
| 76 | + - symbol/variable counts for weights |
| 77 | + - bloom filter for substitution |
| 78 | +] |
| 79 | +== Literals |
| 80 | + |
| 81 | +#slide[ |
| 82 | +```rs |
| 83 | +struct Literal { |
| 84 | + lhs: Term, |
| 85 | + rhs: Term, |
| 86 | + pol: Polarity, |
| 87 | + orient: Rc<OnceCell<Orient>>, |
| 88 | +} |
| 89 | +``` |
| 90 | +][ |
| 91 | +Similar to E's implementation: |
| 92 | +- not (yet) fully shared |
| 93 | +- identified up to symmetry: |
| 94 | + - equality check symmetries |
| 95 | + - hashing orders lhs/rhs by their pointer |
| 96 | +- orientation gets lazily computed and cached: |
| 97 | + - in particular also carried over to copies |
| 98 | +] |
| 99 | + |
| 100 | +== Clauses |
| 101 | +#slide[ |
| 102 | +```rs |
| 103 | +struct Clause { |
| 104 | + id: ClauseId, |
| 105 | + info: ClauseInfo, |
| 106 | + literals: Vec<Literal>, |
| 107 | + selected: Rc<OnceCell<BitVec>>, |
| 108 | +} |
| 109 | +``` |
| 110 | +][ |
| 111 | +Similar to E's implementation: |
| 112 | +- unique id to easily reference them: |
| 113 | + - could use pointers but annoying due to life times |
| 114 | +- meta data for given clause selection |
| 115 | +- selection gets lazily computed and cached |
| 116 | +] |
| 117 | + |
| 118 | +== Discrimination Tree |
| 119 | +#slide[ |
| 120 | +```rs |
| 121 | +enum DiscrTreeKey { |
| 122 | + Star, |
| 123 | + App { |
| 124 | + id: FunctionIdentifier, |
| 125 | + arity: usize, |
| 126 | + }, |
| 127 | +} |
| 128 | +
|
| 129 | +struct DiscriminationTree<V> { |
| 130 | + trie: Trie<DiscrTreeKey, V>, |
| 131 | +} |
| 132 | +``` |
| 133 | +][ |
| 134 | +Based on @handbooktwo: |
| 135 | +- basic imperfect tree |
| 136 | +- no optimization on the tree: never shows up in profiles |
| 137 | +- no other index tried: profile almost always dominated by: |
| 138 | + - subsumption check |
| 139 | + - maximality check |
| 140 | +] |
| 141 | + |
| 142 | +== Feature Vector Index |
| 143 | +#slide[ |
| 144 | +```rs |
| 145 | +const FV_SIZE: usize = 16; |
| 146 | +
|
| 147 | +struct FeatureVector { |
| 148 | + vec: [usize; FV_SIZE], |
| 149 | +} |
| 150 | +
|
| 151 | +struct FeatureVectorIndex { |
| 152 | + trie: Trie<usize, ClauseId>, |
| 153 | +} |
| 154 | +``` |
| 155 | +][ |
| 156 | +Based on @fvi: |
| 157 | +- supports forward + backward subsumption |
| 158 | +- uses the DRT-AC config: |
| 159 | + - counting pos/neg literals |
| 160 | + - counting a few symbols pos/neg |
| 161 | + - catch all for other symbols pos/neg |
| 162 | +] |
| 163 | + |
| 164 | +== Clause Queue |
| 165 | +#slide[ |
| 166 | +```rs |
| 167 | +const WEIGHTED_RATIO: usize = 10; |
| 168 | +
|
| 169 | +pub struct ClauseQueue { |
| 170 | + weighted: BinaryHeap<Clause>, |
| 171 | + fifo: VecDeque<Clause>, |
| 172 | + used: FxHashSet<ClauseId>, |
| 173 | + step: usize, |
| 174 | +} |
| 175 | +``` |
| 176 | +][ |
| 177 | +Based on @queue, uses `10SC11/FIFO-PI`: |
| 178 | +- select ratio of 10:1 between: |
| 179 | + - symbol weight queue with weight 1 for functions and terms |
| 180 | + - FIFO queue |
| 181 | +- both with bias for initial clauses |
| 182 | +] |
| 183 | + |
| 184 | += Reasoning Engine |
| 185 | +Basic DISCOUNT loop from @braniac: |
| 186 | ++ select given clause |
| 187 | ++ forward simplification |
| 188 | ++ forward subsumption |
| 189 | ++ backward subsumption |
| 190 | ++ backward simplification |
| 191 | ++ generating inferences |
| 192 | ++ tautology check |
| 193 | + |
| 194 | +== Term Ordering and Unification |
| 195 | +Knuth Bendix Order: |
| 196 | +- efficient version based on @kbo |
| 197 | +- efficiently extended to literals like duper |
| 198 | +- function symbol precende like in @braniac: |
| 199 | + - higher arity wins |
| 200 | + - same arity use arbitrary order from term bank |
| 201 | + |
| 202 | +Unification: |
| 203 | +- the naive algorithm from the lecture |
| 204 | +- key component for enforcing well sortedness |
| 205 | + |
| 206 | +== Generating Inferences |
| 207 | +Uses the rules and side conditions from @braniac: |
| 208 | +- two discrimination trees: |
| 209 | + - one with all subterms for paramodulating into |
| 210 | + - one with all equational literals for paramodulating from |
| 211 | + - pruned by orientation |
| 212 | +- particular care in the maximality check as it often dominates the profiles |
| 213 | +- configurable literal selection: |
| 214 | + - none |
| 215 | + - first negative literal |
| 216 | + - all positive literals and first negative maximal literal (zipperposition default) |
| 217 | + |
| 218 | +== Simplifications and Tautology Check |
| 219 | +For simplification rules: |
| 220 | +- rewriting in pos/neg literals (RN, RP) |
| 221 | + - cache per simplifier invocation but not globally |
| 222 | + - has a discrimination tree with all unit equational clauses |
| 223 | + pruned by orientation |
| 224 | +- Deletion of duplicated literals (DD) |
| 225 | +- Deletion of resolved literals (DR) |
| 226 | + |
| 227 | +For tautology checking: |
| 228 | +- Detecting reflexive literals (TD1) |
| 229 | +- Detecting complementary literals (TD2) |
| 230 | + |
| 231 | +== Subsumption |
| 232 | +Heuristic based on @subsume: |
| 233 | +- order literals to work likely harder ones earlier |
| 234 | +- afterwards bruteforce using an efficient backtracking |
| 235 | + scheme like in zipperposition |
| 236 | +- uses a feature vector index for forward/backward substitution |
| 237 | + |
| 238 | += Performance |
| 239 | +todo |
| 240 | + |
| 241 | += Bibliography |
| 242 | +#bibliography("literature.bib", title: none) |
0 commit comments