TL;DR
This paper introduces a novel approach to optimizing Boolean satisfiability (SAT) solvers by strategically reordering literals within cardinality constraints. By doing so, they demonstrate that the "meaning" of auxiliary variables can be significantly improved, leading to better solver performance, often more so than choosing a different encoding technique.
What Problem Does This Paper Address?
Boolean satisfiability (SAT) solvers are powerful tools used across many domains, from planning to hardware verification. These solvers work by reducing complex problems into a standardized format called Conjunctive Normal Form (CNF). A key challenge in this process is representing high-level constraints, such as cardinality constraints (e.g., "at most k of these variables are true"), efficiently. Traditional methods focus on optimizing the structure of these encodings (number of clauses, auxiliary variables, propagation power). However, this paper highlights that the order of literals within these constraints, which is often overlooked, can have a profound impact on how effectively a SAT solver can learn and reason about the problem. The gap addressed is the lack of systematic methods for optimizing this literal ordering to improve SAT solver performance.
Methods
The core contribution of this paper is the exploration and development of various literal sorting methods for cardinality constraints. Instead of changing the encoding itself (e.g., totalizer vs. sorting network), they modify the input to these encodings by reordering the data literals. The proposed methods range in complexity:
- Natural: Simple ordering based on variable names.
- Random: Random permutation of variables.
- Occur: Orders variables by their frequency of appearance in clauses.
- Proximity: A more sophisticated method that considers both occurrence and proximity within clauses and at-most-one (AMO) constraints, using a BFS-like search and scoring mechanism.
- Graph-based Ordering: Leverages graph theory, specifically community detection algorithms (Louvain), to group related variables and create an ordering based on these communities.
These methods are applied to existing cardinality constraint encodings (like totalizers, sorting networks, sequential counters) to see how literal ordering impacts their effectiveness.
Datasets
The experiments were conducted using benchmarks from the MaxSAT Competition 2023 (unweighted track). These benchmarks were adapted into SAT problems by creating a large cardinality constraint representing the optimum bound. This approach provides a diverse set of 30 benchmark families, offering a robust evaluation.
Key Insights and Ideas
- Literal order matters, a lot: The paper strongly suggests that the order of literals within a cardinality constraint can be more impactful than the choice of encoding technique itself. This is a significant shift in perspective, moving beyond purely structural optimizations.
- Auxiliary variables gain meaning: By sorting related literals together, the auxiliary variables introduced by the encoding gain a more coherent and interpretable meaning. This allows the SAT solver to reason more effectively about groups of related literals, leading to better clause learning.
- Non-intuitive orderings can be best: The paper shows that simple orderings like "natural" (based on variable names) are often outperformed by more complex, sometimes non-intuitive, orderings like Proximity or Graph-based methods.
- Preprocessing overhead is often worth it: While sophisticated sorting methods like Proximity and Graph have higher preprocessing costs, the improved solving times often justify this overhead, especially for difficult instances.
- Encoding asymmetry matters: The sequential counter encoding, due to its asymmetric nature, showed less improvement from literal sorting compared to more symmetric encodings like totalizers or sorting networks.
Key Results
- The PAMO+Occur literal sorting method (a combination of Proximity with AMO detection and the Occur heuristic) significantly improved performance across various encoding types, often allowing simpler encodings to outperform more complex ones when combined with the right ordering.
- On MaxSAT benchmarks, the best literal sorting methods (like PAMO+Occur) solved more instances than the Natural ordering across different encodings. For example, with the mtotalizer encoding, PAMO+Occur allowed it to solve more instances than the Natural kmtotalizer.
- The Proximity and Graph ordering methods showed consistent improvements, particularly on specific benchmark families, demonstrating their ability to create more balanced clause coverage.
- The paper quantifies the preprocessing time, showing that while methods like Proximity and Graph have higher overheads, they can lead to substantial gains in solving time.
Limitations and Future Work
- Preprocessing Cost: Sophisticated ordering methods like Graph can have significant preprocessing times, which might be prohibitive for very large formulas or time-constrained environments. The paper notes that the Graph approach can be slow to compute community structures.
- "Virtual Best Solver" Gap: While PAMO+Occur performed very well, there was still a gap between its performance and the "Virtual Best Solver" (VBS), which represents the absolute best performance achievable by picking the optimal literal sorting for each individual formula. This suggests that a single "best" ordering might not exist for all problems, and more adaptive or problem-specific approaches could be beneficial.
- Future Work: The authors suggest exploring more adaptive methods for selecting literal orderings, potentially dynamically during the solving process. Further investigation into how different encodings interact with specific literal ordering strategies could also yield valuable insights.