Local-Search Satisfaction Solvers for Propositional Logic Extended with Cardinality Constraints

Title: Local-Search Satisfaction Solvers for Propositional Logic Extended with Cardinality Constraints

Abstract: This research focuses on developing local-search satisfaction solvers for an extension of propositional logic that includes cardinality constraints. This extension facilitates modeling search problems and often results in concise encodings. The study proposes two native solvers designed specifically for the extended language and techniques to reduce the problem to standard propositional satisfaction and use off-the-shelf SAT solvers. The experimental results show that native solvers designed specifically for the extended language perform better than indirect methods relying on SAT solvers.

Research Question: How can local-search satisfaction solvers be designed to effectively handle the extended syntax of propositional logic with cardinality constraints?

Methodology: The study develops local-search satisfaction solvers for the extended propositional logic. It describes two native solvers and techniques to reduce the problem to standard propositional satisfaction. The solvers operate by executing a specified number of tries, each starting with a random truth assignment and consisting of a sequence of local modification steps called flips. The flips are determined by selecting an atom from an unsatisfied clause. The choice of an atom is based on the unsatisfied clause and the current truth assignment.

Results: The experimental results show that the native solvers designed specifically for the extended language perform better than indirect methods relying on SAT solvers. This suggests that the native solvers are more efficient and effective in handling the extended syntax of the logic.

Implications: The research has implications for the development of efficient and effective local-search satisfaction solvers for propositional logic extended with cardinality constraints. It provides a framework for designing such solvers and demonstrates their superior performance compared to indirect methods relying on SAT solvers. This can lead to improved performance in solving search problems represented in the extended logic.

Link to Article: https://arxiv.org/abs/0310061v1 Authors: arXiv ID: 0310061v1