Improving abcdSAT by At-Least-One Recently Used Clause Management Strategy

TL;DR

This paper enhances the abcdSAT solver with new heuristics like at-least-one recently used clause management, and develops three versions for different SAT Competition 2016 tracks, improving performance across various scenarios.

Contribution

It introduces a novel at-least-one recently used clause management heuristic and develops three specialized abcdSAT versions for different competition tracks.

Findings

Improved SAT solver performance with new heuristics.

Three abcdSAT versions tailored for specific competition tracks.

Enhanced clause management strategies contribute to better solving efficiency.

Abstract

We improve further the 2015 version of abcdSAT by various heuristics such as at-least-one recently used strategy, learnt clause database approximation reduction etc. Based on the requirement of different tracks at the SAT Competition 2016, we develop three versions of abcdSAT: drup, inc and lim, which participate in the competition of main (agile), incremental library and no-limit track, respectively.