refactor: binary encoding of at most one clauses by baszalmstra · Pull Request #37 · prefix-dev/resolvo

baszalmstra · 2024-05-30T21:51:01Z

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.

Eh2406 · 2024-05-31T14:27:19Z

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

…oding

baszalmstra · 2024-06-10T14:34:30Z

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:

This is what the graph looks like with this branch:

jjerphan · 2024-07-26T08:18:46Z

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)

…oding

baszalmstra · 2024-08-15T07:06:34Z

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

As we already know this PR is a clear win.

jjerphan · 2024-08-19T13:24:12Z

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

jjerphan

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.

jjerphan · 2024-08-21T07:16:10Z

 pub(crate) enum ConflictNode {
    /// Node corresponding to a solvable
    Solvable(InternalSolvableId),
+    /// Node corresponding to a solvable


Suggested change

/// Node corresponding to a solvable

/// Node corresponding to a variable

jjerphan · 2024-08-21T07:25:33Z

+/// A variable in the SAT problem. A variable either references a solvable, or
+/// an intermediate variable.


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.

jjerphan · 2024-08-21T07:56:25Z

+    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),


Must ExpandedVar::Variable also implement to_usize?

jjerphan · 2024-08-21T08:03:14Z

    /// In SAT terms: (¬A ∨ ¬B)
-    ForbidMultipleInstances(InternalSolvableId, InternalSolvableId, NameId),
+    ForbidMultipleInstances(InternalSolvableId, Literal, NameId),
+


Julien nitpicking: is this required?

Suggested change

jjerphan · 2024-08-21T08:06:46Z

 #[derive(Copy, Clone, Eq, PartialEq, Hash, Debug, Ord, PartialOrd)]
 pub(crate) struct InternalSolvableId(u32);

-const INTERNAL_SOLVABLE_NULL: u32 = u32::MAX;


How about keeping this value and using it in implementations?

jjerphan · 2024-08-21T08:07:01Z

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


Suggested change

VarId(u32::MAX)

VarId(INTERNAL_SOLVABLE_NULL)

jjerphan · 2024-08-21T08:07:13Z

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


Suggested change

self.0 == u32::MAX

self.0 == INTERNAL_SOLVABLE_NULL

jjerphan · 2024-08-21T08:23:22Z

+                        // 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


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

jjerphan · 2024-08-21T08:27:21Z

+                    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,
+                            ));


Are those special cases of a particular encoding?

baszalmstra · 2025-01-01T08:31:07Z

superseded by #91

baszalmstra added 2 commits May 30, 2024 22:25

refactor: variable ids

c57e642

refactor: binary encoding

37e87c1

baszalmstra changed the title ~~refactor: variable ids~~ refactor: binary encoding of at most one clauses May 30, 2024

baszalmstra and others added 5 commits May 30, 2024 23:54

fix: fmt

5ac362b

fix: clippy

5290eab

fix: problems

0f483a0

fix: problem merging

7e80cf5

wip

a64894c

baszalmstra added 3 commits June 7, 2024 20:41

Merge remote-tracking branch 'upstream/main' into refactor/binary_enc…

7b66a1e

…oding

fix: doctest

7b248ca

fix: doctest

4c8c6e5

Merge branch 'main' into refactor/binary_encoding

12ffa47

jjerphan mentioned this pull request Jul 26, 2024

Sync with main + potential suggestions / rest of implementation (if any) baszalmstra/resolvo#1

Merged

Merge pull request #1 from jjerphan/refactor/binary_encoding

1ba5ecf

Sync with `main` + potential suggestions / rest of implementation (if any)

jjerphan mentioned this pull request Aug 2, 2024

RFC — Towards a new solver for libmamba mamba-org/mamba#3387

Open

25 tasks

Merge remote-tracking branch 'upstream/main' into refactor/binary_enc…

e42b8b1

…oding

baszalmstra force-pushed the refactor/binary_encoding branch from 1d1a903 to e42b8b1 Compare August 14, 2024 20:58

jjerphan reviewed Aug 21, 2024

View reviewed changes

baszalmstra mentioned this pull request Sep 9, 2024

feat!: decide on explicit requirements first #61

Merged

1 task

baszalmstra mentioned this pull request Nov 28, 2024

High memory usage #86

Closed

ruben-arts mentioned this pull request Dec 2, 2024

Make pixi easy to use prefix-dev/pixi#2549

Closed

baszalmstra mentioned this pull request Dec 31, 2024

perf: reintroduce binary encoding of forbid clauses #91

Merged

baszalmstra closed this Jan 1, 2025

	/// Node corresponding to a solvable
	/// Node corresponding to a variable

		/// A variable in the SAT problem. A variable either references a solvable, or
		/// an intermediate variable.

		// 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" 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

Conversation

baszalmstra commented May 30, 2024

Uh oh!

Eh2406 commented May 31, 2024

Uh oh!

baszalmstra commented Jun 10, 2024

Uh oh!

jjerphan commented Jul 26, 2024

Uh oh!

baszalmstra commented Aug 15, 2024

Uh oh!

jjerphan commented Aug 19, 2024

Uh oh!

jjerphan left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

baszalmstra commented Jan 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants