Improving abcdSAT by At-Least-One Recently Used Clause Management Strategy
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.
Code (0)
등록된 구현이 없습니다.
Tasks
ManagementSimilar Papers 제목 키워드 기반
Improving SAT Solvers via Blocked Clause Decomposition
The decision variable selection policy used by the most competitive CDCL (Conflict-Driven Clause Learning) SAT solvers is either VSIDS (Variable State Independent Decaying Sum) or its variants such as exponential version…
Variable SelectionRecognizing and Splitting Conditional Sentences for Automation of Business Processes Management
Business Process Management (BPM) is the discipline which is responsible for management of discovering, analyzing, redesigning, monitoring, and controlling business processes. One of the most crucial tasks of BPM is disc…
ManagementSentenceRevisiting the Learned Clauses Database Reduction Strategies
In this paper, we revisit an important issue of CDCL-based SAT solvers, namely the learned clauses database management policies. Our motivation takes its source from a simple observation on the remarkable performances of…
ManagementCharacterization of Glue Variables in CDCL SAT Solving
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 in a given learned clause. The lower the …
Learning Theorem Proving Components
Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selection heuristics in such systems are, howeve…
Automated Theorem ProvingGraph Neural Network