Skip to content
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

Use Open WBO totalizer encoding for At Most One constraints #26

Open
wants to merge 34 commits into
base: master
Choose a base branch
from

Conversation

sukrutrao
Copy link
Owner

@sukrutrao sukrutrao commented Oct 27, 2018

Currently, binomial encoding is used for at most one constraints. This PR replaces it with the totalizer encoding based off Open WBO.

To be merged after #40

@prateekkumarweb prateekkumarweb added this to the v0.4.0 milestone Nov 2, 2018
prateekkumarweb and others added 20 commits November 3, 2018 01:29
Signed-off-by: Prateek Kumar <[email protected]>
Signed-off-by: Prateek Kumar <[email protected]>
minorInMinorTime
programAtMostOneOfCoreOrElective
exactlyOneFieldValuePerCourse

Signed-off-by: Prateek Kumar <[email protected]>
Now the class list will not be cluttered in doxygen as all
the relevant classes for custom constraint grammar are
put in a namespace

Signed-off-by: Prateek Kumar <[email protected]>
Signed-off-by: Prateek Kumar <[email protected]>
Signed-off-by: Prateek Kumar <[email protected]>
@@ -219,6 +220,8 @@ void TTotalizer::build(MaxSATFormula *formula, vec<Lit> &lits, int64_t rhs) {
assert(rhs >= 1 && rhs <= lits.size());

if (incremental_strategy == _INCREMENTAL_NONE_ && rhs == lits.size()) {
DEBUG() << "Totalizer (Not incremental): Rhs is equal to lits.size()";
hasEncoding = true;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@GoodDeeds please check if this change is appropriate.

The issue was that when RHS is equal to lits.size(), hasEncoding was false and update step failed(Line 179).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants