Local-search techniques for propositional logic extended with cardinality constraints

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

14 Scopus citations

Abstract

We study local-search satisfiability solvers for prepositional 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 prepositional 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 prepositional 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.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsFrancesca Rossi
Pages495-509
Number of pages15
DOIs
StatePublished - 2003

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2833
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science (all)

Fingerprint

Dive into the research topics of 'Local-search techniques for propositional logic extended with cardinality constraints'. Together they form a unique fingerprint.

Cite this