4 papers · 1 filter
A Linear Weight Transfer Rule for Local Search
Md Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
The Divide and Distribute Fixed Weights algorithm (ddfw) is a dynamic local search SAT-solving algorithm that transfers weight from satisfied to falsified clauses in local minima.…
A Deep Dive into Conflict Generating Decisions
Md Solimul Chowdhury, Martin Müller, Jia You
Boolean Satisfiability (SAT) is a well-known NP-complete problem. Despite this theoretical hardness, SAT solvers based on Conflict Driven Clause Learning (CDCL) can solve large SAT…
Characterization of Glue Variables in CDCL SAT Solving
Md Solimul Chowdhury, Martin Müller, Jia-Huai You
A state-of-the-art criterion to evaluate the importance of a given learned clause is called Literal Block Distance (LBD) score. It measures the number of distinct decision levels i…
Evolving Real-Time Heuristics Search Algorithms with Building Blocks
Md Solimul Chowdhury, Victor Silva
The research area of real-time heuristics search has produced quite many algorithms. In the landscape of real-time heuristics search research, it is not rare to find that an algori…