# Core First Unit Propagation

## TL;DR

This paper introduces core first unit propagation, a new technique that prioritizes core clauses to generate shorter learnt clauses, improving SAT solver performance.

## Contribution

It proposes a novel core first unit propagation method that enhances clause learning efficiency in SAT solvers.

## Key findings

- Improves performance of MapleLCMDistChronoBT solver
- Prioritizing core clauses reduces learnt clause size
- Empirical results show performance gains

## Abstract

Unit propagation (which is called also Boolean Constraint Propagation) has been an important component of every modern CDCL SAT solver since the CDCL solver was developed. In general, unit propagation is implemented by scanning sequentially every clause over a linear watch-list. This paper presents a new unit propagation technique called core first unit propagation. The main idea is to prefer core clauses over non-core ones during unit propagation, trying to generate a shorter learnt clause. Here, the core clause is defined as one with literal block distance less than or equal to 7. Empirical results show that core first unit propagation improves the performance of the winner of the SAT Competition 2018, MapleLCMDistChronoBT.