arXiv:2611.15091v1 Announce Type: new
Abstract: We present a GPU-CPU hybrid framework for Weighted Partial MaxSAT (WPMAX-SAT) that complements state-of-the-art CPU solvers with differentiable GPU optimization. The GPU stage directly optimizes instance-specific categorical decision parameters without a training dataset or a pretrained predictive model. The central challenge in extending differentiable optimization to WPMAX-SAT is the hard/soft clause asymmetry: hard clauses represent inviolable feasibility constraints while soft clauses carry weights. We introduce a hierarchical differentiable loss that prioritizes hard clause satisfaction before optimizing the weighted soft objective, ensuring that GPU gradient descent leans towards the constraint structure of WPMAX-SAT. Our framework transforms the GPU-optimized variable logits to high-confidence assignments and transfers them to CPU solvers via two complementary modes: partial guidance, which injects the most confident perturbed partial variable assignments as soft clauses into $N$ parallel solver instances, and phase initialization, which guides the CDCL solver's internal branching polarity with the full GPU assignment as a warm start to preserve the problem's originality. We evaluate on all 229 instances of the MSE 2024 (most recent due to cancellation in 2025) anytime weighted benchmark with the top 2 winners as baselines; our hybrid framework improves the average solution score by up to 4.9% over tt-open-wbo-inc-Glucose and 4.8% over SPB-MaxSAT-c-FPS at a 300-second time limit, with the potential to obtain better solutions surpassing the best known solution recorded in the competition evaluation.
Abstract: We present a GPU-CPU hybrid framework for Weighted Partial MaxSAT (WPMAX-SAT) that complements state-of-the-art CPU solvers with differentiable GPU optimization. The GPU stage directly optimizes instance-specific categorical decision parameters without a training dataset or a pretrained predictive model. The central challenge in extending differentiable optimization to WPMAX-SAT is the hard/soft clause asymmetry: hard clauses represent inviolable feasibility constraints while soft clauses carry weights. We introduce a hierarchical differentiable loss that prioritizes hard clause satisfaction before optimizing the weighted soft objective, ensuring that GPU gradient descent leans towards the constraint structure of WPMAX-SAT. Our framework transforms the GPU-optimized variable logits to high-confidence assignments and transfers them to CPU solvers via two complementary modes: partial guidance, which injects the most confident perturbed partial variable assignments as soft clauses into $N$ parallel solver instances, and phase initialization, which guides the CDCL solver's internal branching polarity with the full GPU assignment as a warm start to preserve the problem's originality. We evaluate on all 229 instances of the MSE 2024 (most recent due to cancellation in 2025) anytime weighted benchmark with the top 2 winners as baselines; our hybrid framework improves the average solution score by up to 4.9% over tt-open-wbo-inc-Glucose and 4.8% over SPB-MaxSAT-c-FPS at a 300-second time limit, with the potential to obtain better solutions surpassing the best known solution recorded in the competition evaluation.
This article has been indexed from cs.AI updates on arXiv.org
Read the original article:
Advancing Weighted Partial MaxSAT Solving via Differentiable GPU Guidance