-
Notifications
You must be signed in to change notification settings - Fork 562
feat(resolver): don't build new clauses for weights #1563
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(resolver): don't build new clauses for weights #1563
Conversation
[APPROVALNOTIFIER] This PR is APPROVED This pull-request has been approved by: ecordell The full list of commands accepted by this bot can be found here. The pull request process is described here
Needs approval from an approver in each of these files:
Approvers can indicate their approval by writing |
/lgtm |
/retest Please review the full test history for this PR and help us cut down flakes. |
8 similar comments
/retest Please review the full test history for this PR and help us cut down flakes. |
/retest Please review the full test history for this PR and help us cut down flakes. |
/retest Please review the full test history for this PR and help us cut down flakes. |
/retest Please review the full test history for this PR and help us cut down flakes. |
/retest Please review the full test history for this PR and help us cut down flakes. |
/retest Please review the full test history for this PR and help us cut down flakes. |
/retest Please review the full test history for this PR and help us cut down flakes. |
/retest Please review the full test history for this PR and help us cut down flakes. |
Description of the change:
This builds a sorting network with multiple entries to signal weight, instead of explicit weight literals and constraints on them.
For example:
Prior to this change:
Installable x of weight 3 and y of weight 2 would give:
(x, w0, w1, w2, y, wy0, wy1) literals (cardinality is minimized)
(x -> w0, x -> w1, x-> w2, y -> wy0, y -> wy1) constraints
so the cardinality of picking x is 3 and the cardinality of picking y is 2
Benchmarks:
After this change:
Installable x of weight 3 and y of weight 2 would give:
(x, x, x, y, y) literals (cardinality is minimized)
no constraints
so the cardinality of picking x is 3 and the cardinality of picking y is 2
Benchmarks:
Motivation for the change:
Speed up resolution.
Source: page 13 of Translating Pseudo-Boolean Constraints into SAT
Reviewer Checklist
/docs