Research map / Learning theory and algorithms / Combinatorial and search optimization

The Impact of Literal Sorting on Cardinality Constraint Encodings

AAAI 2025 · Learning theory and algorithms › Combinatorial and search optimization · approach: SAT and model counting solvers · 0 citations (OpenAlex)

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 literal sorting heuristics (Occur, Proximity/PAMO, Graph community-based) that reorder literals inside cardinality constraints before CNF encoding, improving CaDiCaL performance on MaxSAT-derived SAT instances across encoding types.

Problem

Cardinality constraint encodings for SAT solving depend on the order of data literals, which determines the meaning of auxiliary variables, yet encoding research has focused on size and propagation rather than literal ordering.

Approach

Instead of changing encoding structure, reorder the literals within cardinality constraints using structural properties of the formula (occurrence counts, clause/AMO proximity, variable-incidence-graph communities) so auxiliary variables summarize related groups, without changing encoding size.

Key results

• With the kmtotalizer encoding, PAMO+Occur ordering solves more instances than the Natural ordering (Table 2: 670 vs 635 solved in Table 1 setup), and literal ordering outperforms the choice of encoding type.
• Under the PAMO+Occur ordering, the mtotalizer, cardinality network, and sorting network each solve more instances than the Natural kmtotalizer.
• Virtual best solver across literal sortings solves 363 SAT and 332 UNSAT instances versus 334 and 301 for Natural (Table 2).

Measured effects reported in the paper

Surprising findings

• A cheap Occur ordering performs worse than Natural, showing structure-agnostic sorting is insufficient.
• The simplified cardinality network underperforms the sorting network under good orderings, suggesting size reductions can limit learning.

Limitations

• Proximity and Graph orderings incur substantial preprocessing overhead on large formulas.
• No single ordering is best across all instances; a large gap remains between PAMO+Occur and the virtual best solver.
• Evaluation limited to MaxSAT-derived cardinality constraints with one large constraint and CaDiCaL solver.

Experimental setup

Datasets: MaxSAT Evaluation 2023 unweighted benchmarks

Benchmarks: MaxSAT 2023 unweighted track derived SAT problems (398 SAT, 398 UNSAT)

Metrics: number solved PAR-2 score clause coverage

Baselines: Natural ordering Random ordering Occur ordering Graph ordering Proximity ordering

Builds on: totalizer sequential counter sorting network cardinality network Louvain community detection

Closest papers by meaning

• A Cardinal Improvement to Pseudo-Boolean Solving (AAAI 2020 · similarity 0.89)
• Using Symmetries to Lift Satisfiability Checking (AAAI 2024 · similarity 0.87)
• Hardness of Random Reordered Encodings of Parity for Resolution and CDCL (AAAI 2024 · similarity 0.86)
• SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.85)
• Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.85)
• Exploiting Symmetries in MUS Computation (AAAI 2025 · similarity 0.85)