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

fix: disjunctive_scheduling example had incorrect negation constraint #114

Merged

Conversation

tiptenbrink
Copy link

Hi, another tiny fix while getting everything running.

I'm pretty sure the negation of literal => s_y - s_x <= -p_y is as follows:

$$l => s_y - s_x <= -p_y$$ $$\neg l => s_y - s_x > -p_y$$ $$\neg l => s_y - s_x >= -p_y + 1$$ $$\neg l => -s_y + s_x <= p_y - 1$$

Also the literal was not actually negated in the second case, so I added that as well in the way I think you're supposed to do it.

@maartenflippo
Copy link
Contributor

maartenflippo commented Dec 6, 2024

So what we are really after, is the following:

$$ \displaylines{ l_1 \rightarrow s_x + p_x \leq s_y \\ l_2 \rightarrow s_y + p_y \leq s_x } $$

Moving the variables to the left-hand side of the $\leq$, we have:

$$ \displaylines{ l_1 \rightarrow s_x - s_y \leq -p_x \\ l_2 \rightarrow s_y - s_x \leq -p_y } $$

Then we post the clause

$$ l_1 \lor l_2 $$

@tiptenbrink do you want to make these changes?

@tiptenbrink tiptenbrink force-pushed the disjunctive-example-fix branch 2 times, most recently from c435a51 to 2d9af42 Compare December 19, 2024 09:56
@tiptenbrink tiptenbrink changed the base branch from main to develop December 19, 2024 09:57
@tiptenbrink tiptenbrink changed the title fix: disjunctive_scheduling example had incorrect negation constraint DRAFT: fix: disjunctive_scheduling example had incorrect negation constraint Dec 19, 2024
@tiptenbrink tiptenbrink force-pushed the disjunctive-example-fix branch from 2d9af42 to 3a0d66a Compare December 19, 2024 11:26
@tiptenbrink tiptenbrink force-pushed the disjunctive-example-fix branch from 3a0d66a to 956000d Compare December 19, 2024 11:27
@tiptenbrink tiptenbrink changed the title DRAFT: fix: disjunctive_scheduling example had incorrect negation constraint fix: disjunctive_scheduling example had incorrect negation constraint Dec 19, 2024
@tiptenbrink
Copy link
Author

@maartenflippo this one was also ready

@maartenflippo maartenflippo self-requested a review February 3, 2025 15:08
@maartenflippo maartenflippo merged commit 6c04461 into ConSol-Lab:develop Feb 3, 2025
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants