1+ //! A 2-SAT Solver.
2+ //!
3+ //! For variables $x_0, x_1, \ldots, x_{N - 1}$ and clauses with from
4+ //!
5+ //! \\[
6+ //! (x_i = f) \lor (x_j = g)
7+ //! \\]
8+ //!
9+ //! it decides whether there is a truth assignment that satisfies all clauses.
10+ //!
11+ //! Initialize with `init`.
12+ //! Is owned by the caller and should be freed with `deinit`.
13+
114const std = @import ("std" );
215const SccGraph = @import ("internal_scc.zig" );
3- const TwoSat = @This ();
416const Allocator = std .mem .Allocator ;
517const assert = std .debug .assert ;
618
19+ const TwoSat = @This ();
20+
721allocator : Allocator ,
22+ /// Number of variables
823n : usize ,
924scc : SccGraph ,
25+ /// A truth assignment that satisfies all clauses **of the last call of `satisfiable`**.
1026answer : []bool ,
1127
28+ /// Create a new `TwoSat` of `n` variables and 0 clauses.
29+ /// Deinitialize with `deinit`.
30+ ///
31+ /// # Complexity
32+ ///
33+ /// - $O(n)$
1234pub fn init (allocator : Allocator , n : usize ) Allocator.Error ! TwoSat {
1335 return TwoSat {
1436 .allocator = allocator ,
@@ -18,17 +40,37 @@ pub fn init(allocator: Allocator, n: usize) Allocator.Error!TwoSat {
1840 };
1941}
2042
43+ /// Release all allocated memory.
2144pub fn deinit (self : * TwoSat ) void {
2245 self .scc .deinit ();
2346 self .allocator .free (self .answer );
2447}
2548
49+ /// Adds a clause $(x_i = f) \lor (x_j = g)$.
50+ ///
51+ /// # Constraints
52+ ///
53+ /// - $0 \leq i < n$
54+ /// - $0 \leq j < n$
55+ ///
56+ /// # Panics
57+ ///
58+ /// Panics if the above constraints are not satisfied.
59+ ///
60+ /// # Complexity
61+ ///
62+ /// - $O(1)$ amortized
2663pub fn addClause (self : * TwoSat , i : usize , f : bool , j : usize , g : bool ) Allocator.Error ! void {
2764 assert (i < self .n and j < self .n );
2865 try self .scc .addEdge (2 * i + @intFromBool (! f ), 2 * j + @intFromBool (g ));
2966 try self .scc .addEdge (2 * j + @intFromBool (! g ), 2 * i + @intFromBool (f ));
3067}
3168
69+ /// Returns whether there is a truth assignment that satisfies all clauses.
70+ ///
71+ /// # Complexity
72+ ///
73+ /// - $O(n + m)$ where $m$ is the number of added clauses
3274pub fn satisfiable (self : * TwoSat ) Allocator.Error ! bool {
3375 const id = (try self .scc .sccIds ()).@"1" ;
3476 defer self .allocator .free (id );
0 commit comments