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

[WIP] Improve satask() performance #11789

Open
wants to merge 15 commits into
base: master
from

Conversation

Projects
None yet
4 participants
@rlamy
Copy link
Member

commented Oct 31, 2016

This branch makes satask() about 20 times faster. There are no real algorithmic changes, this simply uses explicit data structures to avoid expensive operations such as And instantiations, to_cnf() or known_facts.rcall(). The bottleneck now appears to be converting the "relevant facts" to CNF.

To do:

  • Stabilise and clean up the new APIs
  • Add unit tests for them
  • Fix test failures
  • Worry about backwards compatibility
@asmeurer

This comment has been minimized.

Copy link
Member

commented Nov 1, 2016

The changes look fine at a glance. I can't comment much on the changes to the DPLL code. I guess the sorting in And makes instantiating And very slow.

I don't think any of the APIs that you changed are public, so I wouldn't worry about backwards compatibility. This whole code is supposed to be experimental anyway, so we should feel free to change it and its API as much as is needed.

@asmeurer

This comment has been minimized.

Copy link
Member

commented Nov 1, 2016

Re: bottleneck in converting to CNF.

I haven't done any benchmarking, but I suspect we should abstract better in sathandlers.py to always return CNF clauses. We may want to "compile" them somehow. I do want to keep the facts themselves (the big for loop at the bottom) as readable as possible (it could be even potentially more readable, e.g., a pattern matching API had been suggested), but there are also opportunities to avoid duplicate computation. Pure compilation is more difficult than what the old assumptions do because of the generality of the facts (e.g., they apply to n argument functions like Mul where n is any integer).

@asmeurer

This comment has been minimized.

Copy link
Member

commented Nov 1, 2016

The test failures here definitely need to be fixed. I do seem to recall adding sufficient test cases for this code that I'd be fairly confident that it still works correctly once the tests are passing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.