Local-search techniques for propositional logic extended with cardinality constraints

TL;DR

This paper introduces native local-search solvers for propositional logic with cardinality constraints, demonstrating their superior performance over reduction-based methods using standard SAT solvers.

Contribution

The paper presents two native local-search algorithms specifically designed for propositional logic extended with cardinality atoms, along with reduction techniques to standard SAT.

Findings

Native solvers outperform reduction-based methods

Techniques effectively reduce extended logic to standard SAT

Experimental results confirm the efficiency of native solvers

Abstract

We study local-search satisfiability solvers for propositional logic extended with cardinality atoms, that is, expressions that provide explicit ways to model constraints on cardinalities of sets. Adding cardinality atoms to the language of propositional logic facilitates modeling search problems and often results in concise encodings. We propose two ``native'' local-search solvers for theories in the extended language. We also describe techniques to reduce the problem to standard propositional satisfiability and allow us to use off-the-shelf SAT solvers. We study these methods experimentally. Our general finding is that native solvers designed specifically for the extended language perform better than indirect methods relying on SAT solvers.