Skip to content

Fixes recursion exception in davisb_putnamb_logemann_loveland #5647

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.

Sign up for GitHub

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

Jump to bottom
Closed
wants to merge 6 commits into from
Closed

Fixes recursion exception in davisb_putnamb_logemann_loveland #5647

wants to merge 6 commits into from

Conversation

spazm
Copy link
Contributor

@spazm spazm commented Oct 28, 2021 •
edited
Loading

Describe your change:

  • Fixes the recursion exception bug in dpll. Removes a case where recursion is called with unmodified symbols.
  • Fixes recursion branch bug where both left and right actually evaluating right. Python arrays are copied by value, so both calls received the same modified model.
  • Adds step comments
  • renames vars to better semantic values
  • pythonic clean-up around arrays.
  • Add an algorithm?
  • Fix a bug or typo in an existing algorithm?
  • Documentation change?

Checklist:

  • I have read CONTRIBUTING.md.
  • This pull request is all my own work -- I have not plagiarized.
  • I know that pull requests will not be merged if they fail the automated tests.
  • This PR only changes one algorithm file. To ease review, please open separate PRs for separate algorithms.
  • All new Python files are placed inside an existing directory.
  • All filenames are in all lowercase characters with no spaces or dashes.
  • All functions and variable names follow Python naming conventions.
  • All function parameters and return values are annotated with Python type hints.
  • All functions have doctests that pass the automated testing.
  • All new algorithms have a URL in its comments that points to Wikipedia or other similar explanation.
  • If this pull request resolves one or more open issues then the commit message contains Fixes: #{$ISSUE_NO}.

spazm added 6 commits October 28, 2021 12:18
@spazm
dpll: add example case for recursion bug
92e83cf 
The formula {{A3' , A1} , {A3} , {A4}} is satisfiable with the
assignment {'A1': True, 'A4': True, 'A3': True}.

The formula {{A3' , A1} , {A4} , {A3}} is raises a RecursionError and is
not satisfiable.

The formula {{A2' , A3} , {A2 , A3 , A5' , A1} , {A3} , {A5 , A1'}} is
raises a RecursionError and is
not satisfiable.
@spazm
dpll: add comment for each step
809ec7c
@spazm
dpll: python check on array length
a6ab187
@spazm
dpll: fixes algo bug, recursion both went down False arm
fe86ce0 
+ copies model to allow independent mutation.
+ python assigns by reference.  both tmp models mutated the original
model and the second over wrote the first.  Recursion was going down
the same branch each time.
@spazm
dpll: Fixes recursion problem by checking if unit_symbol remains in u…
6197fc7 
…nevaluated symbols
@spazm
dpll: uses descriptive var names to show intent. pythonic copy
a42c6a4 
+ filter out P during the copy rather than removing after the copy
  is both clearer and marginally more efficient.  1.5n -> n
@ghost ghost added awaiting reviews This PR is ready to be reviewed enhancement This PR modified some existing files labels Oct 28, 2021
This was referenced Oct 28, 2021
Closed
Closed
Closed
@poyea
Copy link
Member

poyea commented Oct 29, 2021

davisb_putnamb_logemann_loveland.py looks weird

l3str4nge
l3str4nge requested changes Oct 30, 2021
View reviewed changes
other/davisb_putnamb_logemannb_loveland.py
print(f"satisfiable with the assignment {model}.")
else:
print("not satisfiable.")
# recursion example:
Copy link
Member

Choose a reason for hiding this comment

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

I would remove this block of code

other/davisb_putnamb_logemannb_loveland.py
@@ -292,6 +299,9 @@ def dpll_algorithm(
>>> model
{'A4': True}
"""

# 2. Check any False
Copy link
Member

Choose a reason for hiding this comment

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

2 and then 1?

@ghost ghost added awaiting changes A maintainer has requested changes to this PR and removed awaiting reviews This PR is ready to be reviewed labels Oct 30, 2021
@spazm spazm mentioned this pull request Nov 3, 2021
Merged
14 tasks
@stale
Copy link

stale bot commented Apr 25, 2022

This pull request has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Thank you for your contributions.

@stale stale bot added the stale Used to mark an issue or pull request stale. label Apr 25, 2022
@cclauss cclauss closed this Sep 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@l3str4nge l3str4nge l3str4nge requested changes

Assignees
No one assigned
Labels
awaiting changes A maintainer has requested changes to this PR enhancement This PR modified some existing files stale Used to mark an issue or pull request stale.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@spazm @poyea @l3str4nge @cclauss