Solving SAT Puzzles

Given a puzzle with switches (variables) and rules (clauses) in DIMACS-like format:

-1309 725 -958 0
1200 -44 0
...

1. Parse into standard DIMACS CNF format
2. Feed to a fast SAT solver (don't hand-solve — with 1,500+ vars and 6,900+ rules, this requires an actual solver algorithm)
3. Extract the satisfying assignment
4. Convert back to the puzzle's on/off format and submit before the time limit

Python
def parse_rules_to_dimacs(raw_text, num_vars):
    clauses = []
    for line in raw_text.strip().splitlines():
        lits = [int(x) for x in line.split()]
        assert lits[-1] == 0, "each line must end with 0"
        clauses.append(lits[:-1])
    return clauses

def write_dimacs(clauses, num_vars, path="puzzle.cnf"):
    with open(path, "w") as f:
        f.write(f"p cnf {num_vars} {len(clauses)}\n")
        for c in clauses:
            f.write(" ".join(map(str, c)) + " 0\n")

Then solve with a SAT solver (e.g., pysat, minisat, or z3):

Python
from pysat.solvers import Glucose3

def solve(clauses):
    with Glucose3(bootstrap_with=clauses) as solver:
        if solver.solve():
            model = solver.get_model()
            return model  # list of signed ints: positive = True, negative = False
        return None

Progress:

• Step 1: Scrape/copy the puzzle rules from the web page (Hark.com or similar)
• Step 2: Parse rule count and switch count; validate every line ends in 0
• Step 3: Convert to DIMACS CNF format
• Step 4: Run a SAT solver (Glucose/MiniSat via python-sat, or z3-solver as fallback)
• Step 5: Verify the returned model satisfies ALL original clauses (self-check before submitting)
• Step 6: Map the solution back to switch numbers → on/off states
• Step 7: Submit the answer in the format the puzzle site expects
• Step 8: If no solution is found within the time budget, report UNSAT or retry with a different solver/config

Time budget rule of thumb: For ~1,500 vars / ~7,000 clauses (3-SAT-like), a modern solver finishes in well under a second to a few seconds — the 10-minute limit is generous. Reserve most of the window as safety margin, not solving time. If a solve attempt stalls past ~30 seconds, something is likely wrong with parsing, not the solver — stop and re-check input.