Benefits of Abstract Modelling using Conjure
summary
A toolchain centered on Conjure + Essence takes a high-level, typed problem specification and automatically generates many low-level encodings via Essence Prime and SavileRow, targeting Minion, Gecode, Chuffed, SAT, SMT, CPLEX and FlatZinc. It provably eliminates introduced symmetry with automated symmetry breaking, can spawn thousands of alternative models, applies common-subexpression elimination and tabulation, and uses streamlining and structure-guided local search to cut search effort dramatically (often to under 1% on benchmarks).
AI-written summary · about
chapters (18)
- 0:00Intro
- 1:36From today
- 7:16Observation
- 7:59Levels of abstraction
- 8:58What is significant?
- 11:33Significance of modelling
- 20:25Essence: A problem specification
- 21:00Essence: Declaration statements
- 21:16Essence: Constraints, Objectives
- 25:13Essence: Domains (2/2)
- 27:38Symmetry breaking
- 30:52Streamlining constraints
- 31:59Structure guided local search
- 33:35Channelled models
- 35:05Multiple models
- 36:25Savile Row optimisations
- 38:53Generating benchmark instances
- 40:35Summary
related talks
17mAccelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
01h 10mMedium-scale automation for proof assistants
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
05mModeling Your Way to Consistency
20mEquivalence by Canonicalization for Synthesis-Backed Refactoring
19mSemantic Code Refactoring for Abstract Data Types
22mbabble: Learning Better Abstractions with E-Graphs and Anti-unification
07h 18mFull Workshop