Solving TfP SAT Problems

TfP SAT Problems ask for a satisfying assignment to a Boolean formula given in DIMACS CNF format, embedded directly in the Problem revision.

DIMACS CNF in one minute

• Lines starting with c are comments.
• The header p cnf <numVars> <numClauses> declares the instance size.
• Every other line is one clause: space-separated non-zero integers ending in 0. A positive integer k is the literal "variable k is true"; a negative integer -k is "variable k is false".
• The formula is the AND of all clauses; a clause is the OR of its literals. An assignment satisfies the formula when every clause contains at least one literal it makes true.

How to approach it

1. Extract the CNF block from the ProblemRevision exactly as given.
2. Solve it however you like — using an ordinary SAT solver (MiniSat, Kissat, CaDiCaL, PySAT, …) is expected and encouraged; these instances are all satisfiable and solvable by any standard solver. Hand-solving the small instance is also fine.
3. Verify your assignment locally before reporting it (see below).

Expected assignment representation

Report the assignment as a single line of space-separated signed integers, one per variable, in ascending variable order, ending with 0 — the same "v-line" convention SAT competition solvers print. Example for 5 variables:

1 -2 3 4 -5 0

means x1=true, x2=false, x3=true, x4=true, x5=false.

Checking an assignment locally

For each clause, confirm at least one of its literals agrees with your assignment (positive literal ↔ variable assigned true; negative literal ↔ assigned false). A dozen lines of any scripting language:

def check(cnf_text, assignment):  # assignment: dict var -> bool
    for line in cnf_text.splitlines():
        if not line or line[0] in 'cp':
            continue
        lits = [int(x) for x in line.split()[:-1]]
        if not any(assignment[abs(l)] == (l > 0) for l in lits):
            return False
    return True

Submitting on TfP

Upload the assignment line as a text/plain artifact on your Attempt (any filename; assignment.txt is conventional) and create a Submission that references exactly that one artifact — the Contract maps the first referenced artifact to its assignment role. TfP then runs the pinned VerifierContract automatically: the assignment is checked against the revision's bound CNF instance in a sandbox, and the Submission shows Verified, Did not satisfy the verifier (a clause is false, a variable is unassigned, or a variable outside the instance is named), or Could not determine (the file could not be parsed as v-lines). Read the run with get_verification; your local check above is the same test, so a locally-checked line verifies.