Smart Cubing for Graph Search: A Comparative Study
Parallel solving via cube-and-conquer is a key method for scaling SAT solvers to hard instances. While cube-and-conquer has proven successful for pure SAT problems, notably the Pythagorean triples conjecture, its application to SAT solvers extended with propagators presents unique challenges, as these propagators learn constraints dynamically during the search. We study this problem using SAT Modulo Symmetries (SMS) as our primary test case, where a symmetry-breaking propagator reduces the search space by learning constraints that eliminate isomorphic graphs. Through extensive experimentation comprising over 10,000 CPU hours, we systematically evaluate different cube-and-conquer variants on three well-studied combinatorial problems. Our methodology combines prerun phases to collect learned constraints, various cubing strategies, and parameter tuning via algorithm configuration and LLM-generated design suggestions. The comprehensive empirical evaluation provides new insights into effective cubing strategies for propagator-based SAT solving, with our best method achieving speedups of 2-3x from improved cubing and parameter tuning, providing an additional 1.5-2x improvement on harder instances.
Code (0)
등록된 구현이 없습니다.
Tasks
CPUSimilar Papers 제목 키워드 기반
AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems
This paper introduces AlphaMapleSAT, a novel Monte Carlo Tree Search (MCTS) based Cube-and-Conquer (CnC) SAT solving method aimed at efficiently solving challenging combinatorial problems. Despite the tremendous success …
Heuristic SearchExperimental comparison of graph-based approximate nearest neighbor search algorithms on edge devices
In this paper, we present an experimental comparison of various graph-based approximate nearest neighbor (ANN) search algorithms deployed on edge devices for real-time nearest neighbor search applications, such as smart …
Autonomous VehiclesTRACE: A Time-Relational Approximate Cubing Engine for Fast Data Insights
A large class of data questions can be modeled as identifying important slices of data driven by user defined metrics. This paper presents TRACE, a Time-Relational Approximate Cubing Engine that enables interactive analy…
Sentiment Analysis on Customer Responses
Sentiment analysis is one of the fastest spreading research areas in computer science, making it challenging to keep track of all the activities in the area. We present a customer feedback reviews on product, where we ut…
Opinion MiningSentiment AnalysisDistributed Software-Defined Network Architecture for Smart Grid Resilience to Denial-of-Service Attacks
An important challenge for smart grid security is designing a secure and robust smart grid communications architecture to protect against cyber-threats, such as Denial-of-Service (DoS) attacks, that can adversely impact …
Benchmarking