The Impact of Literal Sorting on Cardinality Constraint Encodings
Authors: Joseph E. Reeves, João Filipe, Min-Chien Hsu, Ruben Martins, Marijn J. H. Heule
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The experimental evaluation on benchmarks from the maximum satisfiability competition demonstrates that literal orderings can be more influential than the choice of the encoding type. Our literal ordering technique improves solver performance across various encoding techniques, underscoring the robustness of our approach. We ran experiments on Star Exec (Stump, Sutcliffe, and Tinelli 2014). The specs can be found online (Star Exec 2024). Each experiment had 32 GB of memory and an 1,800 second timeout. |
| Researcher Affiliation | Academia | 1Carnegie Mellon University, Pittsburgh, Pennsylvania, United States 2University of Amsterdam, The Netherlands EMAIL, EMAIL |
| Pseudocode | Yes | The Proximity algorithm is presented below: 1. Select the unprocessed variable v (i.e., not part of the ordering yet) with the highest score. If the highest score is 0, select the most occurring unprocessed variable. 2. Append v to the ordering. 3. If AMO detection is enabled, for each AMO constraint K that contains v, increment the scores of unprocessed variables occurring in K by len(K)2, where the length of an AMO constraint is the number of variables it contains. 4. For each clause C that contains v, increment the scores of unprocessed variables occurring in C by 1/len(C) if len(C) 3 or len(C)2 = 4 for a binary clause. 5. If all variables in cardinality constraints are processed, return the ordering; otherwise, return to step 1. |
| Open Source Code | Yes | Code https://github.com/jreeves3/Literal Sorting |
| Open Datasets | Yes | Our evaluation uses Max SAT benchmarks from the 2023 competition unweighted track (J arvisalo et al. 2023). Each Max SAT formula contains a set of hard clauses and soft units. The goal is to find the optimum (minimum) number of soft units that must be falsified while satisfying all hard clauses. Max SAT problems can be converted to SAT by combining the hard clauses with one, often large, cardinality constraint stating at most k soft units are falsified. We can generate a satisfiable SAT problem by making the cardinality constraint s bound the optimum, and an unsatisfiable SAT problem by making the bound the optimum minus one. We consider problems with known optimums and bounds greater than 1 and less than one minus the number of soft units, ensuring that the resulting cardinality constraint is not a clause. This gives 398 satisfiable and 398 unsatisfiable SAT problems. |
| Dataset Splits | Yes | This gives 398 satisfiable and 398 unsatisfiable SAT problems. |
| Hardware Specification | Yes | We ran experiments on Star Exec (Stump, Sutcliffe, and Tinelli 2014). The specs can be found online (Star Exec 2024). Each experiment had 32 GB of memory and an 1,800 second timeout. |
| Software Dependencies | Yes | Given a problem represented as a set of clauses and cardinality constraints, the tool chain sorts literals in the cardinality constraints, encodes the cardinality constraints into CNF using Py SAT (Ignatiev, Morgado, and Marques-Silva 2018), then runs the CDCL SAT solver Ca Di Ca L (Biere et al. 2020) on the resulting CNF formula. |
| Experiment Setup | Yes | Each experiment had 32 GB of memory and an 1,800 second timeout. The main literal sorting configurations are the following: Natural, Random (from 5 random permutations we reported the best (Best Random) and worst (Worst Random) times for each formula), Occur, Proximity, and Graph (computing communities up to 50 times with a 300 second timeout). Proximity can be extended with the AMO detection (PAMO) restricted by a 50 second timeout. Additionally, we ran Natural for 100 seconds then restarted with PAMO if the formula was unsolved (Natural+PAMO) and ran PAMO for formulas with fewer than one million clauses and occurrence otherwise (PAMO+Occur). |