다항 공간(Polynomial Space) 클래스

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

def alpha_beta_minimax(position, depth, alpha, beta, maximizing_player):
    if depth == 0 or position.is_terminal():
        return position.evaluate()
    
    if maximizing_player:
        max_eval = float('-inf')
        for move in position.get_legal_moves():
            new_position = position.make_move(move)
            eval = alpha_beta_minimax(new_position, depth - 1, alpha, beta, False)
            max_eval = max(max_eval, eval)
            alpha = max(alpha, eval)
            if beta <= alpha:
                break  # 베타 컷오프
        return max_eval
    else:
        min_eval = float('inf')
        for move in position.get_legal_moves():
            new_position = position.make_move(move)
            eval = alpha_beta_minimax(new_position, depth - 1, alpha, beta, True)
            min_eval = min(min_eval, eval)
            beta = min(beta, eval)
            if beta <= alpha:
                break  # 알파 컷오프
        return min_eval

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

def model_check(system, specification):
    # 시스템의 모든 가능한 상태 집합
    states = system.get_initial_states()
    visited = set()
    
    # BFS로 모든 도달 가능한 상태 탐색
    while states:
        state = states.pop(0)
        
        if state in visited:
            continue
        
        visited.add(state)
        
        # 현재 상태에서 명세를 위반하는지 확인
        if not specification.check(state):
            return False, state  # 반례 반환
        
        # 다음 상태 탐색
        for next_state in system.get_next_states(state):
            if next_state not in visited:
                states.append(next_state)
    
    # 모든 상태가 명세를 만족
    return True, None

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

def cyk_parsing(grammar, sentence):
    words = sentence.split()
    n = len(words)
    
    # DP 테이블 초기화: table[i][j]는 i부터 시작하여 길이 j인 부분 문자열이 유도 가능한 비단말 기호 집합
    table = [[set() for _ in range(n + 1)] for _ in range(n)]
    
    # 길이 1인 부분 문자열 처리
    for i in range(n):
        for rule in grammar:
            if rule[0] == words[i]:  # A -> word
                table[i][1].add(rule[1])
    
    # 길이 2 이상인 부분 문자열 처리
    for length in range(2, n + 1):
        for start in range(n - length + 1):
            for split in range(1, length):
                for rule in grammar:
                    if len(rule) == 3:  # A -> BC
                        B, C = rule[1], rule[2]
                        if B in table[start][split] and C in table[start + split][length - split]:
                            table[start][length].add(rule[0])
    
    # 전체 문장이 시작 기호로부터 유도 가능한지 확인
    return "S" in table[0][n]

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

class ChessEngine:
    def __init__(self, max_depth=4):
        self.max_depth = max_depth
        self.transposition_table = {}  # 이전에 평가된 위치 캐싱
    
    def get_best_move(self, position):
        """알파-베타 가지치기를 사용하여 최선의 수 찾기"""
        best_score = float('-inf')
        best_move = None
        
        for move in position.legal_moves():
            new_position = position.make_move(move)
            score = -self.negamax_alpha_beta(new_position, self.max_depth - 1, float('-inf'), float('inf'), -1)
            
            if score > best_score:
                best_score = score
                best_move = move
        
        return best_move
    
    def negamax_alpha_beta(self, position, depth, alpha, beta, color):
        """Negamax 알고리즘과 알파-베타 가지치기"""
        # 트랜스포지션 테이블 조회
        position_hash = position.get_hash()
        if position_hash in self.transposition_table and self.transposition_table[position_hash]['depth'] >= depth:
            return self.transposition_table[position_hash]['score']
        
        # 종료 조건: 게임 종료 또는 최대 깊이 도달
        if depth == 0 or position.is_game_over():
            return color * position.evaluate()
        
        max_score = float('-inf')
        
        for move in position.legal_moves():
            new_position = position.make_move(move)
            score = -self.negamax_alpha_beta(new_position, depth - 1, -beta, -alpha, -color)
            
            max_score = max(max_score, score)
            alpha = max(alpha, score)
            
            if alpha >= beta:
                break  # 베타 컷오프
        
        # 결과를 트랜스포지션 테이블에 저장
        self.transposition_table[position_hash] = {'score': max_score, 'depth': depth}
        
        return max_score

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

class CircuitVerifier:
    def __init__(self):
        self.seen_states = set()
    
    def verify_circuit(self, circuit, specification):
        """BDD(Binary Decision Diagram)를 사용한 회로 검증"""
        # 회로의 초기 상태와 명세의 초기 상태 가져오기
        circuit_init = circuit.get_initial_state()
        spec_init = specification.get_initial_state()
        
        # 초기 상태가 명세를 만족하는지 확인
        if not self.states_compatible(circuit_init, spec_init):
            return False, "Initial state violation"
        
        # BFS로 모든 도달 가능한 상태 탐색
        queue = [(circuit_init, spec_init)]
        
        while queue:
            circuit_state, spec_state = queue.pop(0)
            
            # 상태 쌍을 문자열로 변환하여 캐싱
            state_pair = (str(circuit_state), str(spec_state))
            if state_pair in self.seen_states:
                continue
            
            self.seen_states.add(state_pair)
            
            # 모든 가능한 입력에 대해
            for input_values in self.get_all_possible_inputs(circuit):
                # 회로와 명세의 다음 상태 계산
                next_circuit_state = circuit.next_state(circuit_state, input_values)
                next_spec_state = specification.next_state(spec_state, input_values)
                
                # 다음 상태가 명세를 만족하는지 확인
                if not self.states_compatible(next_circuit_state, next_spec_state):
                    return False, f"Specification violation with input {input_values}"
                
                # 아직 보지 않은 상태 쌍이면 큐에 추가
                next_state_pair = (str(next_circuit_state), str(next_spec_state))
                if next_state_pair not in self.seen_states:
                    queue.append((next_circuit_state, next_spec_state))
        
        # 모든 도달 가능한 상태가 명세를 만족
        return True, "Circuit satisfies specification"
    
    def states_compatible(self, circuit_state, spec_state):
        """회로 상태가 명세 상태와 호환되는지 확인"""
        # 출력 변수 추출
        circuit_outputs = circuit_state.get_outputs()
        spec_outputs = spec_state.get_outputs()
        
        # 모든 출력 변수가 일치하는지 확인
        for var in spec_outputs:
            if var in circuit_outputs and circuit_outputs[var] != spec_outputs[var]:
                return False
        
        return True
    
    def get_all_possible_inputs(self, circuit):
        """회로의 모든 가능한 입력 조합 생성"""
        input_vars = circuit.get_input_variables()
        n = len(input_vars)
        
        # 2^n개의 가능한 입력 조합
        for i in range(2**n):
            input_values = {}
            for j, var in enumerate(input_vars):
                # i의 j번째 비트가 1이면 True, 아니면 False
                input_values[var] = bool(i & (1 << j))
            
            yield input_values