5.1. sdzkp.max2sat
Classes
- class sdzkp.max2sat.Max2SAT(num_variables=None, num_clauses=None)[source]
A class to represent a MAX-2-SAT problem instance.
Attributes: num_variables (int): Number of variables in the SAT instance. num_clauses (int): Number of clauses in the SAT instance. clauses (set): Set of clauses, where each clause is a tuple of two literals. solution (list): A list representing the boolean assignment to variables.
Initializes a Max2SAT instance with the given number of variables and clauses.
Args: num_variables (int): The number of variables in the SAT instance. num_clauses (int): The number of clauses in the SAT instance.
- generate_instance_motoki()[source]
Generates a random instance of a MAX-2-SAT problem using a specific method.
- Algorithm:
Initialize an empty formula F.
Randomly choose four distinct variables:
x_r1, x_r2, x_r3, x_r4
Add initial clauses to F:
Add the clause (x_r1, x_r2) to F.
Add the clause (-x_r3, -x_r4) to F.
Iteratively add clauses until F becomes unsatisfiable
- While F is satisfiable:
Randomly choose a pair of distinct variables (x1, x2).
Add the clause (x1, -x2) to F.
Randomly choose a truth assignment t from {0, 1}^n.
Negate literals in F whose underlying variables are assigned 0 in t.
Return the formula F and the truth assignment t.
Explanation:
This algorithm begins by initializing an empty formula F.
Four distinct variables are randomly selected from the set of available variables.
The algorithm adds two initial clauses to F using these variables.
It then iteratively adds more clauses to F until it becomes unsatisfiable, ensuring that the generated instance is challenging.
A random truth assignment t is selected, and the literals in F are adjusted to make t the optimal solution.
The resulting formula F and truth assignment t are returned as the outputs.
Returns: tuple: A tuple containing the set of clauses and the solution assignment.
- is_satisfiable(formula)[source]
Checks if a given formula (set of clauses) is satisfiable using Kosaraju’s algorithm for finding SCCs.
Args: formula (set): A set of clauses.
Returns: bool: True if the formula is satisfiable, False otherwise.
- negate_literals()[source]
Negates the literals in the clauses based on the solution, where the underlying variable is assigned False.
- add_clause(var1, neg1, var2, neg2)[source]
Adds a clause to the set of clauses.
Args: var1 (int): The index of the first variable. neg1 (bool): Whether the first literal is negated. var2 (int): The index of the second variable. neg2 (bool): Whether the second literal is negated.
- read_filenames_in_folder(folder_path)[source]
Reads all filenames in the specified folder.
Args: folder_path (str): The path to the folder.
Returns: list: A list of filenames in the folder.
- read_dimacs_file(filepath)[source]
Reads a DIMACS formatted file and initializes the SAT instance.
Args: filepath (str): The path to the DIMACS file.
- write_solution_to_file(filepath, solution, num_satisfied_clauses)[source]
Writes the solution and the number of satisfied clauses to a file.
Args: filepath (str): The path to the file where the solution will be written. solution (list): The solution assignment for the variables. num_satisfied_clauses (int): The number of satisfied clauses.
- read_solution_from_file(filepath)[source]
Reads the solution and the number of satisfied clauses from a file.
Args: filepath (str): The path to the file to be read.
Returns: tuple: A tuple containing the solution (list of bool) and the number of satisfied clauses (int).
- generate_satisfiable_clause(assignment)[source]
Generates a satisfiable clause given an assignment.
Args: assignment (list): The boolean assignment for the variables.
Returns: tuple: A satisfiable clause based on the assignment.
- generate_unsatisfiable_specific_clause(var1, var2, assignment)[source]
Generates an unsatisfiable clause given specific variables and an assignment.
Args: var1 (int): The index of the first variable. var2 (int): The index of the second variable. assignment (list): The boolean assignment for the variables.
Returns: tuple: An unsatisfiable clause based on the assignment.
- generate_unsatisfiable_clause(assignment)[source]
Generates an unsatisfiable clause given an assignment.
Args: assignment (list): The boolean assignment for the variables.
Returns: tuple: An unsatisfiable clause based on the assignment.
- is_clause_satisfied(clause, assignment)[source]
Checks if a clause is satisfied under a given assignment.
Args: clause (tuple): The clause to check. assignment (list): The boolean assignment for the variables.
Returns: bool: True if the clause is satisfied, False otherwise.
- check_instance(solution=None)[source]
Checks how many clauses are satisfied by a given solution.
Args: solution (list): The boolean assignment for the variables (optional).
Returns: int: The number of satisfied clauses.
- print_clause(clause)[source]
Prints a clause in a human-readable format.
Args: clause (tuple): The clause to print.
- print_instance()[source]
Prints the entire SAT instance, including all clauses and the current solution.