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: binary encoding of at most one clauses #37

Draft
wants to merge 13 commits into
base: main
Choose a base branch
from

Conversation

baszalmstra
Copy link
Contributor

This PR uses binary encoding to reduce the number of clauses added by a significant factor. My benchmarks show a performance improvement of at least 50%!

I did break unsat reports, that is something I have to look into.

@baszalmstra baszalmstra changed the title refactor: variable ids refactor: binary encoding of at most one clauses May 30, 2024
@Eh2406
Copy link

Eh2406 commented May 31, 2024

This is really good work. I'm excited to see such a positive impact!

@baszalmstra
Copy link
Contributor Author

Use the snapshots from #44 I can confirm that at least for the conda ecosystem this is a huge win.

I used the solve-snapshot tool from #44 to measure the solve times for a large number of solves. This is what the histogram of solve times looks like on the main branch:

image

This is what the graph looks like with this branch:

image

@jjerphan
Copy link
Member

I also can confirm that this implementation helps with the resolution — that's neat!

I am looking at what needs to be fixed on the unsat reports so that it can be integrated.

Sync with `main` + potential suggestions / rest of implementation (if any)
@baszalmstra baszalmstra force-pushed the refactor/binary_encoding branch from 1d1a903 to e42b8b1 Compare August 14, 2024 20:58
@baszalmstra
Copy link
Contributor Author

I computed timing comparisons similar using the tools from #64:

Untitled
Untitled-1

As we already know this PR is a clear win.

@jjerphan
Copy link
Member

Those also are greatly encouraging results, I will block some time to review it this week.

Copy link
Member

@jjerphan jjerphan left a comment

Choose a reason for hiding this comment

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

A first naive pass.

I still need to have a look at the core of collapse_variable_nodes and to compare memory footprint and runtime from main's.

/// A node in the graph representation of a [`Conflict`]
#[derive(Copy, Clone, Eq, PartialEq)]
pub(crate) enum ConflictNode {
/// Node corresponding to a solvable
Solvable(InternalSolvableId),
/// Node corresponding to a solvable
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
/// Node corresponding to a solvable
/// Node corresponding to a variable

Comment on lines +241 to +242
/// A variable in the SAT problem. A variable either references a solvable, or
/// an intermediate variable.
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
/// A variable in the SAT problem. A variable either references a solvable, or
/// an intermediate variable.
/// A variable in the SAT problem. A variable either references a solvable, or
/// an intermediate variable which are generally introduced by the encoding of clauses.

pub fn reset(&mut self, variable: VarId) {
let (map, idx) = match variable.expand() {
ExpandedVar::Solvable(s) => (&mut self.solvables, s.to_usize()),
ExpandedVar::Variable(v) => (&mut self.variables, v as usize),
Copy link
Member

Choose a reason for hiding this comment

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

Must ExpandedVar::Variable also implement to_usize?

@@ -59,7 +60,8 @@ pub(crate) enum Clause {
/// itself forbids two solvables from being installed at the same time.
///
/// In SAT terms: (¬A ∨ ¬B)
ForbidMultipleInstances(InternalSolvableId, InternalSolvableId, NameId),
ForbidMultipleInstances(InternalSolvableId, Literal, NameId),

Copy link
Member

Choose a reason for hiding this comment

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

Julien nitpicking: is this required?

Suggested change

@@ -82,7 +82,6 @@ pub struct SolvableId(pub u32);
#[derive(Copy, Clone, Eq, PartialEq, Hash, Debug, Ord, PartialOrd)]
pub(crate) struct InternalSolvableId(u32);

const INTERNAL_SOLVABLE_NULL: u32 = u32::MAX;
Copy link
Member

Choose a reason for hiding this comment

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

How about keeping this value and using it in implementations?

/// Returns the null variable id. This is used to represent the absence
/// of a variable.
pub fn null() -> VarId {
VarId(u32::MAX)
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
VarId(u32::MAX)
VarId(INTERNAL_SOLVABLE_NULL)


/// Returns true if this variable id is null.
pub fn is_null(self) -> bool {
self.0 == u32::MAX
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
self.0 == u32::MAX
self.0 == INTERNAL_SOLVABLE_NULL

Comment on lines +567 to +568
// use the "Binary Encoding" from
// https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
// use the "Binary Encoding" from
// https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf
// Use the "Binary Encoding" of the At-Most-One (AMO) clause
// from Frisch, A.M., & Giannaros, P.A. (2010).
// SAT Encodings of the At-Most-k Constraint Some Old,
// Some New, Some Fast, Some Slow.
// See: https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf

Comment on lines +540 to +561
if candidates.len() == 2 {
let clause_id = clauses.alloc(ClauseState::forbid_multiple(
candidates[0].into(),
Literal {
var_id: candidates[1].into(),
negate: true,
},
name_id,
));

debug_assert!(clauses[clause_id].has_watches());
output.clauses_to_watch.push(clause_id);
} else if candidates.len() == 3 {
for (a, b) in [(0, 1), (0, 2), (1, 2)] {
let clause_id = clauses.alloc(ClauseState::forbid_multiple(
candidates[a].into(),
Literal {
var_id: candidates[b].into(),
negate: true,
},
name_id,
));
Copy link
Member

Choose a reason for hiding this comment

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

Are those special cases of a particular encoding?

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