# Learned Clause Minimization in Parallel SAT Solvers

## TL;DR

This paper investigates learned clause minimization (LCM) in parallel SAT solvers, revealing that while LCM can improve performance on some instances, it often decreases performance, and only specific approaches are beneficial.

## Contribution

The paper introduces multiple LCM approaches for parallel SAT solvers, compares their effectiveness, and analyzes conditions under which LCM improves solver performance.

## Key findings

- LCM boosts performance on a subset of SAT instances
- Applying LCM often decreases solver performance
- Certain LCM methods can enhance overall parallel SAT solver efficiency

## Abstract

Learned clauses minimization (LCM) let to performance improvements of modern SAT solvers especially in solving hard SAT instances. Despite the success of LCM approaches in sequential solvers, they are not widely incorporated in parallel SAT solvers. In this paper we explore the potential of LCM for parallel SAT solvers by defining multiple LCM approaches based on clause vivification, comparing their runtime in different SAT solvers and discussing reasons for performance gains and losses. Results show that LCM only boosts performance of parallel SAT solvers on a fraction of SAT instances. More commonly applying LCM decreases performance. Only certain LCM approaches are able to improve the overall performance of parallel SAT solvers.