Coverage for sparkle/solver/verifiers.py: 91%

1"""Classes for verifying solutions.""" 

2 

3from __future__ import annotations 

4from pathlib import Path 

5import subprocess 

6 

7from sparkle.types import SolverStatus 

8 

9 

10class SolutionVerifier: 

11 """Solution verifier base class.""" 

12 

13 def verify( 

14 self: SolutionVerifier, instance: Path, output: dict, solver_call: list[str] 

15 ) -> SolverStatus: 

16 """Verify the solution.""" 

17 raise NotImplementedError 

18 

19 

20class SATVerifier(SolutionVerifier): 

21 """Class to handle the SAT verifier.""" 

22 

23 sat_verifier_path = ( 

24 Path(__file__).parent.parent / "Components/Sparkle-SAT-verifier/SAT" 

25 ) 

26 

27 def __str__(self: SATVerifier) -> str: 

28 """Return the name of the SAT verifier.""" 

29 return SATVerifier.__name__ 

30 

31 @staticmethod 

32 def verify(instance: Path, output: dict, solver_call: list[str]) -> SolverStatus: 

33 """Run a SAT verifier and return its status.""" 

34 if SolverStatus(output["status"]) == SolverStatus.TIMEOUT: 

35 return SolverStatus.TIMEOUT 

36 raw_result = Path([s for s in solver_call if s.endswith(".rawres")][0]) 

37 return SATVerifier.call_sat_raw_result(instance, raw_result) 

38 

39 @staticmethod 

40 def sat_verify_output(sat_output: str) -> SolverStatus: 

41 """Return the status of the SAT verifier. 

42 

43 Four statuses are possible: "SAT", "UNSAT", "WRONG", "UNKNOWN" 

44 """ 

45 return_code = int(sat_output.splitlines()[-1]) 

46 if return_code == 11: # SAT code 

47 return SolverStatus.SAT 

48 if return_code == 10: # UNSAT code 

49 return SolverStatus.UNSAT 

50 # Wrong code OR Unknown code 

51 if return_code == 0 and "Wrong solution." in sat_output: 

52 return SolverStatus.WRONG 

53 # Should not occur 

54 return SolverStatus.UNKNOWN 

55 

56 @staticmethod 

57 def call_sat_raw_result(instance: Path, raw_result: Path) -> SolverStatus: 

58 """Run a SAT verifier to determine correctness of a result. 

59 

60 Args: 

61 instance: path to the instance 

62 raw_result: path to the result to verify 

63 

64 Returns: 

65 The status of the solver on the instance 

66 """ 

67 sat_verify = subprocess.run( 

68 [SATVerifier.sat_verifier_path, instance, raw_result], capture_output=True 

69 ) 

70 return SATVerifier.sat_verify_output(sat_verify.stdout.decode()) 

71 

72 

73class SolutionFileVerifier(SolutionVerifier): 

74 """Class to handle the file verifier.""" 

75 

76 def __init__(self: SolutionFileVerifier, csv_file: Path) -> None: 

77 """Initialize the verifier by building dictionary from csv. 

78 

79 Args: 

80 csv_file: path to the csv file. Requires lines to be of the form: 

81 instance,objective,solution 

82 """ 

83 self.csv_file = csv_file 

84 lines = [ 

85 line.split(",", maxsplit=2) 

86 for line in self.csv_file.read_text().splitlines() 

87 ] 

88 self.solutions = { 

89 instance: (objective, solution) for instance, objective, solution in lines 

90 } 

91 

92 def __str__(self: SATVerifier) -> str: 

93 """Return the name of the SAT verifier.""" 

94 return SolutionFileVerifier.__name__ 

95 

96 def verify( 

97 self: SolutionFileVerifier, 

98 instance: Path, 

99 solver_output: dict[str, object], 

100 solver_call: list[str], 

101 ) -> SolverStatus: 

102 """Verify the solution. 

103 

104 Args: 

105 instance: instance to verify, solution found by instance name as key 

106 solver_output: outcome of the solver to verify 

107 solver_call: list of solver calls 

108 

109 Returns: 

110 The status of the solver on the instance 

111 """ 

112 # If the solver ran out of time, we cannot verify a solution 

113 if SolverStatus(solver_output["status"]) == SolverStatus.TIMEOUT: 

114 return SolverStatus.TIMEOUT 

115 instance = instance.name 

116 if instance not in self.solutions: 

117 return SolverStatus.UNKNOWN 

118 

119 objective, solution = self.solutions[instance] 

120 if objective not in solver_output: 

121 return SolverStatus.UNKNOWN 

122 

123 outcome = solver_output[objective] 

124 if solution in SolverStatus._value2member_map_: # SAT type status 

125 solution, outcome = SolverStatus(solution), SolverStatus(outcome) 

126 if solution == SolverStatus.UNKNOWN or solution == outcome: 

127 # Verify that the presented solution is correct 

128 return SATVerifier.verify(instance, solver_output, solver_call) 

129 else: 

130 return SolverStatus.WRONG 

131 

132 if solution != outcome: 

133 return SolverStatus.WRONG 

134 return SolverStatus.SUCCESS 

135 

136 

137# Define a mapping so we can translate between names and classes 

138mapping = { 

139 SATVerifier.__name__: SATVerifier, 

140 SolutionFileVerifier.__name__: SolutionFileVerifier, 

141}