Research map / Learning theory and algorithms / Combinatorial and search optimization
DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem
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 DiverSAT, a local search algorithm for the Diverse SAT problem that finds k mutually diverse satisfying assignments using three new heuristics and an adaptive perturbation mechanism.
Problem
Finding a set of k satisfying assignments of a CNF formula that are maximally diverse (sum of pairwise Hamming distances), since existing SAT solvers return similar solutions.
Approach
A local search over solution sets that generates diverse initial models via variable-decision and polarity heuristics from the current solution's statistics, uses a strengthened configuration-checking heuristic (SCCA) biased by flipping preference, scores models by their average distance to the rest of the set, and adds an adaptive perturbation when diversity stagnates.
Key results
- DiverSAT achieves higher diversity quality than DiversekSet and randAllSAT on all benchmark families reported for k=10, 50, 100 (e.g., hardware at k=100: 270,244,214 vs 210,916,530 for DiversekSet), at the cost of more runtime.
- Ablation: removing the three initialization heuristics (DiverSAT\H) or the adaptive perturbation (DiverSAT\M) lowers diversity quality on all instances in Table 3.
- DiverSAT runs faster than both ablated versions on most instances while maintaining higher diversity.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use DiverSAT instead of the strongest reported baseline | Diverse SAT solvers · hardware, k=100 | diversity quality: 210916530 -> 270244214 | Helped |
| use DiverSAT instead of the strongest reported baseline | Diverse SAT solvers · bmc, k=100 | diversity quality: 2510458 -> 2714649 | Helped |
| use DiverSAT instead of the strongest reported baseline | Diverse SAT solvers · flat30-60, k=100 | diversity quality: 191367 -> 199954 | Helped |
| add the adaptive perturbation mechanism (ablation) | DiverSAT · hardware, k=100 | diversity quality: 251325612 -> 270244214 | Helped |
| add the variable decision, polarity selection, and SCCA heuristics (ablation) | DiverSAT · hardware, k=100 | diversity quality: 254196325 -> 270244214 | Helped |
| add the adaptive perturbation mechanism (ablation) | DiverSAT · flat30-60, k=100 | diversity quality: 199942 -> 199954 | No clear effect |
| add the variable decision, polarity selection, and SCCA heuristics (ablation) | DiverSAT · flat30-60, k=100 | diversity quality: 198836 -> 199954 | Helped |
Surprising findings
- DiverSAT obtains higher diversity but consumes more runtime than competitors on most instances.
- The ablated variant DiverSAT\H does not uniformly underperform DiverSAT\M, suggesting the two components complement each other across problem types.
Limitations
- Runtime is higher than competitors on most instances
- DiversekSet re-implemented on Maple LCM because source code was unavailable
- Tuned parameters on preliminary experiments only; no pairing of hardware with memory beyond 10 GB stated
Experimental setup
Datasets: Nadel 2011 semiformal hardware verification benchmark (66 instances) SATLIB application instances (2670 instances)
Benchmarks: semiformal hardware verification benchmark (Nadel 2011) SATLIB flat graph coloring SATLIB logistics SATLIB bmc SATLIB ssa SATLIB GCP SATLIB qg SATLIB II SATLIB SW100-8 SATLIB ais
Metrics: diversity quality DQ (sum of pairwise Hamming distances) runtime (seconds)
Baselines: DiversekSet randAllSAT
Builds on: CCA (configuration checking with aspiration) VSIDS relaxed CDCL DiversekSet (Nadel 2011)
Closest papers by meaning
- On Continuous Local BDD-Based Search for Hybrid SAT Solving (AAAI 2021 · similarity 0.88)
- Ordered Objectives in Maximum Satisfiability (AAAI 2026 · similarity 0.87)
- SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.87)
- FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints (AAAI 2020 · similarity 0.86)
- Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs (AAAI 2025 · similarity 0.86)
- Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph (AAAI 2024 · similarity 0.85)
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.