Sökning: onr:"swepub:oai:DiVA.org:kth-290612" >
A cardinal improvem...
A cardinal improvement to pseudo-boolean solving
-
Elffers, J. (författare)
-
- Nordström, Jakob, 1972- (författare)
- KTH,Teoretisk datalogi, TCS
-
(creator_code:org_t)
- AAAI press, 2020
- 2020
- Engelska.
-
Ingår i: AAAI 2020 - 34th AAAI Conference on Artificial Intelligence. - : AAAI press. ; , s. 1495-1503
- Relaterad länk:
-
https://urn.kb.se/re...
Abstract
Ämnesord
Stäng
- Pseudo-Boolean solvers hold out the theoretical potential of exponential improvements over conflict-driven clause learning (CDCL) SAT solvers, but in practice perform very poorly if the input is given in the standard conjunctive normal form (CNF) format. We present a technique to remedy this problem by recovering cardinality constraints from CNF on the fly during search. This is done by collecting potential building blocks of cardinality constraints during propagation and combining these blocks during conflict analysis. Our implementation has a non-negligible but manageable overhead when detection is not successful, and yields significant gains for some SAT competition and crafted benchmarks for which pseudo-Boolean reasoning is stronger than CDCL. It also boosts performance for some native pseudo-Boolean formulas where this approach helps to improve learned constraints. Copyright
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Artificial intelligence
- Cardinality constraints
- Clause learning
- Conflict analysis
- Conjunctive normal forms
- On the flies
- Potential building blocks
- Pseudo-Boolean
- SAT solvers
- Boolean algebra
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)