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 Bug: General SAT to Independent Set #71

Merged
merged 4 commits into from
Aug 14, 2024
Merged

Fix Bug: General SAT to Independent Set #71

merged 4 commits into from
Aug 14, 2024

Conversation

SciCodePhy
Copy link
Collaborator

@SciCodePhy SciCodePhy commented Aug 13, 2024

Conclusion: Previous update of "SAT => Independent Set" (#69 ) is problematic. For single input, it is impossible to avoid returning multiple degenerate solutions. Therefore, I go back to the initial method to construct the independent set graph (#65 ), which is consistent with the references.

Achieved:

  • Choose the correct reduction;
  • Give warnings when return multiple degenerate solutions for single input;
  • Modify the way to construct the set of solutions;
  • Add more tests for single input and multiple inputs;

Reason and Example
There are two cases when the single input returns multiple degenerate solutions.
Assuming that the literals are x, y and z:

  • Case01 (satisfiable SAT): Independent Set might give solutions with repeated literals such as "x=0, y=1, x=0, y=1". This case means that z can take arbitary value (truse or false, 1 or 0).
  • Case02 (unsatisfiable SAT): Independent Set will give solutions which don't cover all the literals, such as "x=0, y=1", because whenever z is true or false the whole SAT is unsatisfiable.

Copy link

codecov bot commented Aug 14, 2024

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 93.76%. Comparing base (edb2cdb) to head (b279101).

Additional details and impacted files
@@            Coverage Diff             @@
##             main      #71      +/-   ##
==========================================
+ Coverage   90.55%   93.76%   +3.21%     
==========================================
  Files          28       28              
  Lines        1217     1203      -14     
==========================================
+ Hits         1102     1128      +26     
+ Misses        115       75      -40     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

Copy link
Owner

@GiggleLiu GiggleLiu left a comment

Choose a reason for hiding this comment

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

Looks good to me.

@SciCodePhy SciCodePhy merged commit d23a743 into main Aug 14, 2024
5 checks passed
@SciCodePhy SciCodePhy linked an issue Aug 14, 2024 that may be closed by this pull request
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.

Reduce general SAT to independent problems
2 participants