Satisfiability and systematicity

Abstract

We introduce a new notion of systematicity for satisfiability algorithms with restarts, saying that an algorithm is strongly systematic if it is systematic independent of restart policy but weakly systematic if it is systematic for some restart policies but not others. We show that existing satisfiability engines are generally only weakly systematic, and describe flex, a strongly systematic algorithm that uses an amount of memory polynomial in the size of the problem. On large number factoring problems, flex appears to outperform weakly systematic approaches.