Research map / Learning theory and algorithms / Combinatorial and search optimization
Scalable Knowledge Refactoring Using Constrained Optimisation
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes MaxRefactor, a constraint-optimisation (CP-SAT/MaxSAT) approach to knowledge refactoring of logic programs that uses literal-based decision variables and linear invented rules, scaling far better than Knorf.
Problem
Knowledge refactoring (compressing logic programs by inventing new rules) does not scale: the prior state-of-the-art Knorf enumerates all rule subsets, yielding exponentially many decision variables.
Approach
Encode refactoring with decision variables over predicate-symbol counts in invented rules (rather than over rule subsets), restrict invented rules to linear ones (each variable occurs once in the body), and show this loses no optimality; solve as a COP with CP-SAT or MaxSAT.
Key results
- On Strings with MaxSAT, MaxRefactor improves compression over Knorf on all 196 programs, by 30%-60% (average 53%).
- On Lego, MaxRefactor increases compression rates by at least 27% across all programs (CP-SAT version).
- MaxRefactor scales to programs of size 600 (DrugDrug, Alzheimer) and 1000 (WordNet) with optimal solutions found, while Knorf crashes on other datasets.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Replace rule-subset enumeration with literal-based decision variables, allowing invented rules to combine literals across input rules | MaxRefactor vs. Knorf · Lego programs | compression rate: at least 27% across all programs | Helped |
| Replace rule-subset enumeration with literal-based decision variables, allowing invented rules to combine literals across input rules | MaxRefactor vs. Knorf · Strings programs | compression rate: 172 out of 196 programs; average of 30%; remaining 24 programs ... average 10% lower | Mixed |
| Use MaxSAT instead of CP-SAT | MaxRefactor · Strings programs | compression rate: 30%--60% with an average of 53% | Helped |
| Use linear invented rules rather than unrestricted invented rules | MaxRefactor · Optimal knowledge refactoring | refactored program size | No clear effect |
| Allow invented rules to combine any input literals instead of restricting them to subsets of input rules | MaxRefactor · Example program P1 | program size: 16 vs 18 literals | Helped |
| Use a linear invented rule spanning literals from the input rules | MaxRefactor · Example program Q1 | program size: 30 to 22 | Helped |
Surprising findings
- Knorf crashes on several other datasets during COP modelling due to an input-assumption bug, so only Lego and Strings could be compared.
Limitations
- Does not support recursive invented rules.
- Does not allow invented predicates inside other invented rules.
- Optimality proofs take much longer than finding near-optimal solutions.
Experimental setup
Datasets: Lego Strings DrugDrug Alzheimer WordNet
Benchmarks: Lego Strings DrugDrug Alzheimer WordNet
Metrics: compression rate runtime normalised solution quality
Baselines: Knorf
Builds on: Knorf unfolding
Closest papers by meaning
- Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search (NeurIPS 2026 · similarity 0.85)
- ReGAL: Refactoring Programs to Discover Generalizable Abstractions (ICML 2024 · similarity 0.83)
- Code Repair with LLMs gives an Exploration-Exploitation Tradeoff (NeurIPS 2024 · similarity 0.83)
- Think Smarter not Harder: Adaptive Reasoning with Inference Aware Optimization (ICML 2025 · similarity 0.83)
- PEARL: Solver-in-the-Loop Interactive Optimization Modeling from Natural Language (NeurIPS 2026 · similarity 0.82)
- RE-IMAGINE: Symbolic Benchmark Synthesis for Reasoning Evaluation (ICML 2025 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.