Local-search techniques for propositional logic extended with cardinality constraints

Lengning Liu; Miroslaw Truszczyński

doi:10.1007/978-3-540-45193-8_34

Local-search techniques for propositional logic extended with cardinality constraints

Lengning Liu, Miroslaw Truszczyński

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-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 language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Francesca Rossi
Pages	495-509
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-540-45193-8_34
State	Published - 2003

Publication series

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

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-45193-8_34

Cite this

Liu, L., & Truszczyński, M. (2003). Local-search techniques for propositional logic extended with cardinality constraints. In F. Rossi (Ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 495-509). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2833). https://doi.org/10.1007/978-3-540-45193-8_34

Liu, Lengning ; Truszczyński, Miroslaw. / Local-search techniques for propositional logic extended with cardinality constraints. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Francesca Rossi. 2003. pp. 495-509 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{02e523d6a4f04f0fa9ae99c8e2118168,

title = "Local-search techniques for propositional logic extended with cardinality constraints",

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.",

author = "Lengning Liu and Miroslaw Truszczy{\'n}ski",

year = "2003",

doi = "10.1007/978-3-540-45193-8_34",

language = "English",

isbn = "3540202021",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "495--509",

editor = "Francesca Rossi",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

Liu, L & Truszczyński, M 2003, Local-search techniques for propositional logic extended with cardinality constraints. in F Rossi (ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2833, pp. 495-509. https://doi.org/10.1007/978-3-540-45193-8_34

Local-search techniques for propositional logic extended with cardinality constraints. / Liu, Lengning; Truszczyński, Miroslaw.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Francesca Rossi. 2003. p. 495-509 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2833).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - Local-search techniques for propositional logic extended with cardinality constraints

AU - Liu, Lengning

AU - Truszczyński, Miroslaw

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=35248881454&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35248881454&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-45193-8_34

DO - 10.1007/978-3-540-45193-8_34

M3 - Chapter

AN - SCOPUS:35248881454

SN - 3540202021

SN - 9783540202028

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 495

EP - 509

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Rossi, Francesca

ER -

Liu L, Truszczyński M. Local-search techniques for propositional logic extended with cardinality constraints. In Rossi F, editor, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2003. p. 495-509. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-45193-8_34

Local-search techniques for propositional logic extended with cardinality constraints

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this