Skip to content

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

Merged
merged 1 commit into from
Jun 3, 2020

Conversation

ecordell
Copy link
Member

@ecordell ecordell commented Jun 2, 2020

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:

BenchmarkCompileDict-12    	      18	  55723828 ns/op
BenchmarkDictSolve-12      	       1	1656260078 ns/op
PASS

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:

BenchmarkCompileDict-12    	   12636	     90925 ns/op
BenchmarkDictSolve-12      	      22	  52780348 ns/op
PASS

Motivation for the change:
Speed up resolution.

Source: page 13 of Translating Pseudo-Boolean Constraints into SAT

Reviewer Checklist

  • Implementation matches the proposed design, or proposal is updated to match implementation
  • Sufficient unit test coverage
  • Sufficient end-to-end test coverage
  • Docs updated or added to /docs
  • Commit messages sensible and descriptive

@openshift-ci-robot
Copy link
Collaborator

[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 /approve in a comment
Approvers can cancel approval by writing /approve cancel in a comment

@openshift-ci-robot openshift-ci-robot added the approved Indicates a PR has been approved by an approver from all required OWNERS files. label Jun 2, 2020
@benluddy
Copy link
Contributor

benluddy commented Jun 2, 2020

/lgtm

@openshift-ci-robot openshift-ci-robot added the lgtm Indicates that a PR is ready to be merged. label Jun 2, 2020
@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

8 similar comments
@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-bot
Copy link
Contributor

/retest

Please review the full test history for this PR and help us cut down flakes.

@openshift-merge-robot openshift-merge-robot merged commit 0aaab9d into operator-framework:master Jun 3, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
approved Indicates a PR has been approved by an approver from all required OWNERS files. lgtm Indicates that a PR is ready to be merged.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants