Watched Propagation of$$0$$ -$$1$$ Integer Linear Constraints
(2020) 26th International Conference on Principles and Practice of Constraint Programming, CP 2020 In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 12333 LNCS. p.160-176- Abstract
Efficient unit propagation for clausal constraints is a core building block of conflict-driven clause learning (CDCL) Boolean satisfiability (SAT) and lazy clause generation constraint programming (CP) solvers. Conflict-driven pseudo-Boolean (PB) solvers extend the CDCL paradigm from clausal constraints to integer linear constraints, also known as (linear) PB constraints. For PB solvers, many different propagation techniques have been proposed, including a counter technique which watches all literals of a PB constraint. While CDCL solvers have moved away from counter propagation and have converged on a two watched literals scheme, PB solvers often simultaneously implement different propagation algorithms, including the counter one. The... (More)
Efficient unit propagation for clausal constraints is a core building block of conflict-driven clause learning (CDCL) Boolean satisfiability (SAT) and lazy clause generation constraint programming (CP) solvers. Conflict-driven pseudo-Boolean (PB) solvers extend the CDCL paradigm from clausal constraints to integer linear constraints, also known as (linear) PB constraints. For PB solvers, many different propagation techniques have been proposed, including a counter technique which watches all literals of a PB constraint. While CDCL solvers have moved away from counter propagation and have converged on a two watched literals scheme, PB solvers often simultaneously implement different propagation algorithms, including the counter one. The question whether watched propagation for PB constraints is more efficient than counter propagation, is still open. Watched propagation is inherently more complex for PB constraints than for clauses, and several sensible variations on the idea exist. We propose a new variant of watched propagation for PB constraints and provide extensive experimental results to verify its effectiveness. These results indicate that our watched propagation algorithm is superior to counter propagation, but when paired with specialized propagation algorithms for clauses and cardinality constraints, the difference is fairly small.
(Less)
- author
- Devriendt, Jo LU
- organization
- publishing date
- 2020
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Proceedings
- series title
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
- editor
- Simonis, Helmut
- volume
- 12333 LNCS
- pages
- 17 pages
- publisher
- Springer Science and Business Media B.V.
- conference name
- 26th International Conference on Principles and Practice of Constraint Programming, CP 2020
- conference location
- Louvain-la-Neuve, Belgium
- conference dates
- 2020-09-07 - 2020-09-11
- external identifiers
-
- scopus:85091299056
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783030584740
- DOI
- 10.1007/978-3-030-58475-7_10
- language
- English
- LU publication?
- yes
- id
- 1f73ac4c-ea48-43ef-bf79-1626560b124d
- date added to LUP
- 2020-10-28 10:29:59
- date last changed
- 2024-05-29 21:32:16
@inproceedings{1f73ac4c-ea48-43ef-bf79-1626560b124d,
abstract = {{<p>Efficient unit propagation for clausal constraints is a core building block of conflict-driven clause learning (CDCL) Boolean satisfiability (SAT) and lazy clause generation constraint programming (CP) solvers. Conflict-driven pseudo-Boolean (PB) solvers extend the CDCL paradigm from clausal constraints to integer linear constraints, also known as (linear) PB constraints. For PB solvers, many different propagation techniques have been proposed, including a counter technique which watches all literals of a PB constraint. While CDCL solvers have moved away from counter propagation and have converged on a two watched literals scheme, PB solvers often simultaneously implement different propagation algorithms, including the counter one. The question whether watched propagation for PB constraints is more efficient than counter propagation, is still open. Watched propagation is inherently more complex for PB constraints than for clauses, and several sensible variations on the idea exist. We propose a new variant of watched propagation for PB constraints and provide extensive experimental results to verify its effectiveness. These results indicate that our watched propagation algorithm is superior to counter propagation, but when paired with specialized propagation algorithms for clauses and cardinality constraints, the difference is fairly small.</p>}},
author = {{Devriendt, Jo}},
booktitle = {{Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Proceedings}},
editor = {{Simonis, Helmut}},
isbn = {{9783030584740}},
issn = {{0302-9743}},
language = {{eng}},
pages = {{160--176}},
publisher = {{Springer Science and Business Media B.V.}},
series = {{Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}},
title = {{Watched Propagation of$$0$$ -$$1$$ Integer Linear Constraints}},
url = {{http://dx.doi.org/10.1007/978-3-030-58475-7_10}},
doi = {{10.1007/978-3-030-58475-7_10}},
volume = {{12333 LNCS}},
year = {{2020}},
}