Introduction

This web page is dedicated to our CDCL-Based SAT solver, named Topk-LC-Glucose. It is based on Glucose 3.0 enhanced by a learned clauses database deletion strategy using Topk (unsigned int) undominated learned clauses. Our goal is to take advantage of several relevant learned clauses deletion strategies by seeking a compromise between them through a dominance relationship. In [JE'2017] , we proposed to search at each reduction step of the learned clauses database, the current reference learned clause according to a set of relevant measures and to delete all the learned clauses dominated by this clause. In this approach, we extend this idea by considering instead k current reference learned clauses i.e the Topk undominated learned clauses at each cleaning step and delete all the learned clauses dominated by at least one of the Topk undominated learned clauses.