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

refactor: simplify watchmap traversal #98

Merged
merged 8 commits into from
Jan 9, 2025

Conversation

baszalmstra
Copy link
Contributor

@baszalmstra baszalmstra commented Jan 8, 2025

This PR cleans up the code by adding a new type for traversing and modifying the watchmap. The propagation loop contained a number of bookkeeping locals which distract from the actual propagation algorithm. There were also methods to manipulate the watches and the watchmap in different places, they are now all consolidated in the WatchMapCursor struct.

Using the cursor is very simple: WatchMap::cursor is used to create a cursor to iterate the linked list of watches. WatchMapCursor::next moves the cursor to the next clause watching a certain literal. WatchMapCursor::update modifies the current clause/watch to watch a different literal. This method performs all the bookkeeping of the linked lists to ensure consistency.

Hopefully this makes the code easier to understand.

@baszalmstra baszalmstra requested review from wolfv and tdejager January 8, 2025 21:23
src/internal/id.rs Outdated Show resolved Hide resolved
src/internal/id.rs Outdated Show resolved Hide resolved
src/solver/clause.rs Show resolved Hide resolved
src/solver/clause.rs Show resolved Hide resolved
src/solver/clause.rs Show resolved Hide resolved
src/solver/clause.rs Outdated Show resolved Hide resolved
@baszalmstra
Copy link
Contributor Author

Mm the benchmarks are not favorable:

main_timings.csv: 1000 records
timings.csv: 1000 records

Summary for main_timings.csv:
- Average Solve Time: 0.83 seconds (mean of all durations)
- Median Solve Time: 0.35 seconds (middle value when sorted)
- Standard Deviation: 2.95 seconds (spread of durations around the mean)
- Minimum Solve Time: 0.00 seconds (shortest solve duration)
- Maximum Solve Time: 50.00 seconds (longest solve duration, capped at 50s)
- 25th Percentile: 0.11 seconds (25% of solves were faster than this)
- 75th Percentile: 0.89 seconds (75% of solves were faster than this)
- Number of Outliers: 3 (solves capped at 50s)

Summary for timings.csv:
- Average Solve Time: 0.94 seconds (mean of all durations)
- Median Solve Time: 0.40 seconds (middle value when sorted)
- Standard Deviation: 3.06 seconds (spread of durations around the mean)
- Minimum Solve Time: 0.00 seconds (shortest solve duration)
- Maximum Solve Time: 50.00 seconds (longest solve duration, capped at 50s)
- 25th Percentile: 0.12 seconds (25% of solves were faster than this)
- 75th Percentile: 0.98 seconds (75% of solves were faster than this)
- Number of Outliers: 3 (solves capped at 50s)

Comparison between the datasets:
- Average Solve Time: 'timings.csv' was 0.88 times faster than 'main_timings.csv'
- Median Solve Time: 'timings.csv' was 0.88 times faster than 'main_timings.csv'
- 25th Percentile: 'timings.csv' was 0.93 times faster than 'main_timings.csv'
- 75th Percentile: 'timings.csv' was 0.91 times faster than 'main_timings.csv'
- Outliers: 'timings.csv' had 0 fewer solves capped at 50s

Untitled

@baszalmstra
Copy link
Contributor Author

I simplified the code even further and added a little bit of unsafe magic and the benchmarks look much better now:

main_timings.csv: 1000 records
timings.csv: 1000 records

Summary for main_timings.csv:
- Average Solve Time: 0.83 seconds (mean of all durations)
- Median Solve Time: 0.35 seconds (middle value when sorted)
- Standard Deviation: 2.95 seconds (spread of durations around the mean)
- Minimum Solve Time: 0.00 seconds (shortest solve duration)
- Maximum Solve Time: 50.00 seconds (longest solve duration, capped at 50s)
- 25th Percentile: 0.11 seconds (25% of solves were faster than this)
- 75th Percentile: 0.89 seconds (75% of solves were faster than this)
- Number of Outliers: 3 (solves capped at 50s)

Summary for timings.csv:
- Average Solve Time: 0.86 seconds (mean of all durations)
- Median Solve Time: 0.37 seconds (middle value when sorted)
- Standard Deviation: 3.00 seconds (spread of durations around the mean)
- Minimum Solve Time: 0.00 seconds (shortest solve duration)
- Maximum Solve Time: 50.00 seconds (longest solve duration, capped at 50s)
- 25th Percentile: 0.11 seconds (25% of solves were faster than this)
- 75th Percentile: 0.89 seconds (75% of solves were faster than this)
- Number of Outliers: 3 (solves capped at 50s)

Comparison between the datasets:
- Average Solve Time: 'timings.csv' was 0.96 times faster than 'main_timings.csv'
- Median Solve Time: 'timings.csv' was 0.95 times faster than 'main_timings.csv'
- 25th Percentile: 'timings.csv' was 1.01 times faster than 'main_timings.csv'
- 75th Percentile: 'timings.csv' was 0.99 times faster than 'main_timings.csv'
- Outliers: 'timings.csv' had 0 fewer solves capped at 50s

Untitled

I feel this is good enough to merge.

@wolfv wolfv merged commit 7b5aa29 into prefix-dev:main Jan 9, 2025
13 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.

3 participants