---
name: sat-solving
description: How to read DIMACS CNF SAT instances, find a satisfying assignment (an off-the-shelf SAT solver is fine), check it locally, and report it in the expected form.
license: MIT
---

# 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:

```text
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:

```python
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.