Research map / Label-efficient and robust learning / Recognition and long-tail
Using Symmetries to Lift Satisfiability Checking
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 lifting satisfiability problems in typed FO with aggregates to a compressed domain via multiplicity functions, solving the lifted sentence iteratively and expanding models back, with speedups on generative configuration problems.
Problem
Satisfiability checking is slow on problems with many interchangeable domain elements (symmetries), and generative configuration problems require iteratively guessing domain sizes; traditional symmetry breaking is limited.
Approach
Compress structures onto a smaller lifted domain using symmetry backbones and per-element multiplicity functions, translate a typed FO(Aggregate) sentence into an equisatisfiable lifted sentence with regularity constraints, and grow the lifted domain iteratively until a model is found that expands to a concrete model.
Key results
- On generative configuration problems the lifted method solves most instances in under 1 second where the original sentence times out or takes minutes (e.g., Monkey1 0.28s vs 184.66s with Z3).
- On Rack ABCD problems lifted solving stays near constant time (1.55s to 3.31s for sizes 4 to 20) while the original method times out.
- For the pigeonhole problem with 10,000 pigeons the lifted sentence is solved in 0.05 s, versus 4 s for the original sentence with 30 pigeons.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use the lifted translation and compressed-domain search instead of the original sentence | HCP1 · HCP1 | wall-clock time (seconds): 0.2 -> 0.2 | No clear effect |
| Use the lifted translation and compressed-domain search instead of the original sentence | HCP3 · HCP3 | wall-clock time (seconds): 1.5 -> 0.22 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | HRP1 · HRP1 | wall-clock time (seconds): 0.23 -> 0.27 | Hurt |
| Use the lifted translation and compressed-domain search instead of the original sentence | HRP3 · HRP3 | wall-clock time (seconds): 6.41 -> 0.30 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | Monkey1 · Monkey1 | wall-clock time (seconds): 184.66 -> 0.28 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | Monkey4 · Monkey4 | wall-clock time (seconds): T -> 0.27 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | Rack2011 · Rack2011 | wall-clock time (seconds): 8.82 -> 0.24 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | RackA10 · RackA10 | wall-clock time (seconds): 37.52 -> 0.41 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | RackA1000 · RackA1000 | wall-clock time (seconds): T -> 0.54 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | RackABCD20 · RackABCD20 | wall-clock time (seconds): T -> 3.31 | Helped |
| Use the lifted translation and compressed-domain search instead of the original sentence | RackA4 · RackA4 | wall-clock time (seconds): 36.9 -> 0.65 | Helped |
Surprising findings
- The lifted pigeonhole problem is solved in essentially constant time with respect to domain size, unlike traditional symmetry breaking which scales at least linearly.
Limitations
- The method cannot prove unsatisfiability and does not terminate for unsatisfiable sentences unless a size limit is imposed.
- The translation for binary predicates with lcm uses an interpretation table yielding quadratic complexity.
- The regularity constraints restrict compression for sentences with n-ary predicates; the translation is not optimal.
Experimental setup
Datasets: House Configuration problems Organized Monkey Village Rack problem pigeonhole problem
Benchmarks: House Configuration and Reconfiguration (HCP, HRP) Organized Monkey Village (Monkey) Rack problems
Metrics: wall clock time (s) number of domain elements used
Baselines: Traditional iterative methods (m1, m2, t1, t2) in FO(.)/Z3 OR-tools via CPMpy ASP solver results from prior Rack ABCD work
Builds on: IDP-Z3 FO(.) BAPA
Closest papers by meaning
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.87)
- Breaking Symmetries in Quantified Graph Search: A Comparative Study (AAAI 2025 · similarity 0.85)
- Exploiting Symmetries in MUS Computation (AAAI 2025 · similarity 0.85)
- SAT-Based Techniques for Lexicographically Smallest Finite Models (AAAI 2024 · similarity 0.84)
- Hardness of Random Reordered Encodings of Parity for Resolution and CDCL (AAAI 2024 · similarity 0.84)
- Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning (ICLR 2025 · similarity 0.84)
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.