Revisiting the Learned Clauses Database Reduction Strategies

2014/02/09 by Said Jabbour, Jerry Lonlac, Jabbour, Said +5
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #cs.AI

paper · pdf · doi:10.48550/arxiv.1402.1956

arxiv created 2014/02/09 · arxiv updated 2014/02/11

Abstract

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 both random and size-bounded reduction strategies. We first derive a simple reduction strategy, called Size-Bounded Randomized strategy (in short SBR), that combines maintaing short clauses (of size bounded by k), while deleting randomly clauses of size greater than k. The resulting strategy outperform the state-of-the-art, namely the LBD based one, on SAT instances taken from the last SAT competition. Reinforced by the interest of keeping short clauses, we propose several new dynamic variants, and we discuss their performances.

Related

• An Experimental Study of Permanently Stored Learned Clauses
• Towards Learned Clauses Database Reduction Strategies Based on Dominance Relationship
• On the Effect of Learned Clauses on Stochastic Local Search
• Learned Clause Minimization in Parallel SAT Solvers
• Clause Vivification by Unit Propagation in CDCL SAT Solvers