Untitled

from pysat.formula import CNF
from pysat.solvers import Solver

def add_transition(cnf, current, bit, next, var_map, positive_bit=True):
    """ Helper function to add transition clauses. """
    if positive_bit:
        cnf.append([-var_map[current], var_map[bit], var_map[next]])
    else:
        cnf.append([-var_map[current], -var_map[bit], var_map[next]])

def encode_dfa(t=6):
    """ Function to encode the DFA into CNF using PySAT. """
    cnf = CNF()
    var_map = {}
    count = 1

    # Create variables for each state at each time step and input bits
    for step in range(t + 1):  # 0 to t (inclusive), where t = 6
        for state in ['q0', 'q1', 'q2', 'q3']:
            var_map[f'{state}_{step}'] = count
            count += 1
        if step < t:
            var_map[f'bit_{step}'] = count
            count += 1

    # Initial state configuration
    cnf.append([var_map['q0_0']])
    for state in ['q1', 'q2', 'q3']:
        cnf.append([-var_map[f'{state}_0']])

    # Transitions based on the DFA rules
    for step in range(t):
        add_transition(cnf, 'q0_' + str(step), 'bit_' + str(step), 'q1_' + str(step + 1), var_map)
        add_transition(cnf, 'q0_' + str(step), 'bit_' + str(step), 'q0_' + str(step + 1), var_map, False)
        add_transition(cnf, 'q1_' + str(step), 'bit_' + str(step), 'q2_' + str(step + 1), var_map)
        add_transition(cnf, 'q1_' + str(step), 'bit_' + str(step), 'q1_' + str(step + 1), var_map, False)
        add_transition(cnf, 'q2_' + str(step), 'bit_' + str(step), 'q3_' + str(step + 1), var_map)
        add_transition(cnf, 'q2_' + str(step), 'bit_' + str(step), 'q2_' + str(step + 1), var_map, False)
        add_transition(cnf, 'q3_' + str(step), 'bit_' + str(step), 'q3_' + str(step + 1), var_map)
        add_transition(cnf, 'q3_' + str(step), 'bit_' + str(step), 'q3_' + str(step + 1), var_map, False)

    # Ensure the accepting state is reached
    cnf.append([var_map['q3_' + str(t)]])

    return cnf, var_map

def solve_dfa(cnf, var_map, t=6):
    """ Solving the SAT problem to find accepted strings of length t. """
    with Solver(bootstrap_with=cnf.clauses) as solver:
        if solver.solve():
            model = solver.get_model()
            result = ''.join(['1' if model[var_map[f'bit_{i}']] > 0 else '0' for i in range(t)])
            print(f"Accepted string by DFA: {result}")
        else:
            print("No solution found, which is unexpected.")

def main():
    cnf, var_map = encode_dfa()
    solve_dfa(cnf, var_map)

if __name__ == "__main__":
    main()