Nikhil Shukla

Kenneth M. Zick, Nikhil Shukla, Alexander Marakov

We introduce Collective Switched Motion (Cosm), a heuristic algorithm for solving sparse Ising-type optimization problems. Cosm combines locally interacting continuous circular variables with global coordination rules that facilitate collective dynamics. Pairwise interactions occur sequentially over a set of conflict-free edge partitions, resulting in an interaction network that switches periodically. Unlike conventional gradient-based approaches, Cosm enables structured, non-gradient dynamics that promote exploration beyond local minima. A correlated perturbation mechanism helps enable collective variable rotations. On the three largest Gset instances, which have 10,000-20,000 variables and represent 2D spin glasses, Cosm attains improved solutions that are verified as optimal using an exact solver. On two large bounded-degree Gset instances, a CPU-based implementation of Cosm reduces the state-of-the-art times-to-target from hundreds of hours to 36-303 s, reductions of 2-4 orders of magnitude. Additional tests on planted-solution benchmark instances show a lower scaling exponent than previous dynamical systems heuristics. These results highlight the effectiveness of Cosm in harnessing collective computation for improved sparse combinatorial optimization.

Feng Shi, Chonghan Lee, Mohammad Khairul Bashar et al.

CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. The increasing popularity of these constraint problems in electronic design automation encourages studies on different SAT problems and their properties for further computational efficiency. There has been both theoretical and practical success of modern Conflict-driven clause learning SAT solvers, which allows solving very large industrial instances in a relatively short amount of time. Recently, machine learning approaches provide a new dimension to solving this challenging problem. Neural symbolic models could serve as generic solvers that can be specialized for specific domains based on data without any changes to the structure of the model. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem, which is the optimization version of SAT where the goal is to satisfy the maximum number of clauses. Our model has a scale-free structure which could process varying size of instances. We use meta-path and self-attention mechanism to capture interactions among homogeneous nodes. We adopt cross-attention mechanisms on the bipartite graph to capture interactions among heterogeneous nodes. We further apply an iterative algorithm to our model to satisfy additional clauses, enabling a solution approaching that of an exact-SAT problem. The attention mechanisms leverage the parallelism for speedup. Our evaluation indicates improved speedup compared to heuristic approaches and improved completion rate compared to machine learning approaches.