@@ -66,7 +66,7 @@ class TwoSatisfiability:
6666 Kosaraju's algorithm for finding strongly connected components
6767 """
6868
69- def __init__ (self , number_of_variables : int ):
69+ def __init__ (self , number_of_variables : int ) -> None :
7070 """
7171 Initializes the TwoSat solver with the given number of variables.
7272
@@ -97,15 +97,21 @@ def __init__(self, number_of_variables: int):
9797 # Tracks whether the solve() method has been called
9898 self .__is_solved : bool = False
9999
100- def add_clause (self , a : int , is_negate_a : bool , b : int , is_negate_b : bool ) -> None :
100+ def add_clause (
101+ self ,
102+ first_var : int ,
103+ is_negate_first_var : bool ,
104+ second_var : int ,
105+ is_negate_second_var : bool ,
106+ ) -> None :
101107 """
102108 Adds a clause of the form (a v b) to the boolean expression.
103109
104110 Args:
105- a (int): The first variable (1 ≤ a ≤ number_of_variables)
106- is_negate_a (bool): True if variable a is negated
107- b (int): The second variable (1 ≤ b ≤ number_of_variables)
108- is_negate_b (bool): True if variable b is negated
111+ first_var (int): The first variable (1 ≤ a ≤ number_of_variables)
112+ is_negate_first_var (bool): True if variable a is negated
113+ second_var (int): The second variable (1 ≤ b ≤ number_of_variables)
114+ is_negate_second_var (bool): True if variable b is negated
109115
110116 For example::
111117
@@ -117,23 +123,23 @@ def add_clause(self, a: int, is_negate_a: bool, b: int, is_negate_b: bool) -> No
117123 """
118124 exception_message = f"Variable number must be \
119125 between 1 and { self .__number_of_variables } "
120- if a <= 0 or a > self .__number_of_variables :
126+ if first_var <= 0 or first_var > self .__number_of_variables :
121127 raise ValueError (exception_message )
122- if b <= 0 or b > self .__number_of_variables :
128+ if second_var <= 0 or second_var > self .__number_of_variables :
123129 raise ValueError (exception_message )
124130
125- a = self .__negate (a ) if is_negate_a else a
126- b = self .__negate (b ) if is_negate_b else b
127- not_a = self .__negate (a )
128- not_b = self .__negate (b )
131+ first_var = self .__negate (first_var ) if is_negate_first_var else first_var
132+ second_var = self .__negate (second_var ) if is_negate_second_var else second_var
133+ not_of_first_var = self .__negate (first_var )
134+ not_of_second_var = self .__negate (second_var )
129135
130- # Add implications: (¬a → b ) and (¬b → a )
131- self .__graph [not_a ].append (b )
132- self .__graph [not_b ].append (a )
136+ # Add implications: (¬first_var → second_var ) and (¬second_var → first_var )
137+ self .__graph [not_of_first_var ].append (second_var )
138+ self .__graph [not_of_second_var ].append (first_var )
133139
134140 # Build transpose graph
135- self .__graph_transpose [b ].append (not_a )
136- self .__graph_transpose [a ].append (not_b )
141+ self .__graph_transpose [second_var ].append (not_of_first_var )
142+ self .__graph_transpose [first_var ].append (not_of_second_var )
137143
138144 def solve (self ) -> None :
139145 """
@@ -207,48 +213,50 @@ def get_solutions(self) -> list[bool]:
207213 return self .__variable_assignments .copy ()
208214
209215 def __depth_first_search_for_topological_order (
210- self , u : int , visited : list [bool ], topological_order : list [int ]
216+ self , node : int , visited : list [bool ], topological_order : list [int ]
211217 ) -> None :
212218 """
213219 Performs DFS to compute topological order.
214220
215221 Args:
216- u (int): Current node
222+ node (int): Current node
217223 visited (list[bool]): Visited array
218224 topological_order (list[int]): list to store topological order
219225 """
220- visited [u ] = True
221- for v in self .__graph [u ]:
222- if not visited [v ]:
226+ visited [node ] = True
227+ for neighbour_node in self .__graph [node ]:
228+ if not visited [neighbour_node ]:
223229 self .__depth_first_search_for_topological_order (
224- v , visited , topological_order
230+ neighbour_node , visited , topological_order
225231 )
226- topological_order .append (u )
232+ topological_order .append (node )
227233
228234 def __depth_first_search_for_scc (
229- self , u : int , visited : list [bool ], component : list [int ], scc_id : int
235+ self , node : int , visited : list [bool ], component : list [int ], scc_id : int
230236 ) -> None :
231237 """
232238 Performs DFS on the transposed graph to identify SCCs.
233239
234240 Args:
235- u (int): Current node
241+ node (int): Current node
236242 visited (list[bool]): Visited array
237243 component (list[int]): Array to store component IDs
238244 scc_id (int): Current SCC identifier
239245 """
240- visited [u ] = True
241- component [u ] = scc_id
242- for v in self .__graph_transpose [u ]:
243- if not visited [v ]:
244- self .__depth_first_search_for_scc (v , visited , component , scc_id )
246+ visited [node ] = True
247+ component [node ] = scc_id
248+ for neighbour_node in self .__graph_transpose [node ]:
249+ if not visited [neighbour_node ]:
250+ self .__depth_first_search_for_scc (
251+ neighbour_node , visited , component , scc_id
252+ )
245253
246- def __negate (self , a : int ) -> int :
254+ def __negate (self , variable_index : int ) -> int :
247255 """
248- Returns the index representing the negation of the given variable.
256+ Returns the index representing the negation of the given variable index .
249257
250258 Args:
251- a (int): The variable index
259+ variable_index (int): The variable index
252260
253261 Mapping rule:
254262 -------------
@@ -264,7 +272,7 @@ def __negate(self, a: int) -> int:
264272 The index representing its negation
265273 """
266274 return (
267- a + self .__number_of_variables
268- if a <= self .__number_of_variables
269- else a - self .__number_of_variables
275+ variable_index + self .__number_of_variables
276+ if variable_index <= self .__number_of_variables
277+ else variable_index - self .__number_of_variables
270278 )
0 commit comments