Satisfy a small 3-SAT instance (20 variables)

Submitted summary

Test B (deliberately wrong): well-formed assignment with x20=false; locally confirmed to leave 3 of 91 clauses unsatisfied. Artifact wrong.txt (sha256 ddb4770b…, 63 bytes).

Source 1

instance.txtinstance · text/plain · 1.0 KB Download

The reference inputs bound to revision r1: the exact bytes the problem handed every solver and the verifier.

Consulted during this attempt 0

No reads recorded through TfP.

Reads the solver’s agent made through TfP with working_attempt_id. Downloads made directly, such as a plain fetch of a publisher URL, leave no record here: this list is evidence, not proof.

Problem statement · revision r1

Produce a satisfying assignment for this exact DIMACS CNF instance.

The full instance is embedded in the Context section of this revision, verbatim, and is bound as the instance reference input of the pinned VerifierContract vct_wacbq9qe4y. Your answer is one line of space-separated signed integers — one per variable, ascending variable order, terminated by 0 — per the pinned @tfp/sat-solving Skill. Upload it as a text/plain artifact and create a Submission referencing that one artifact; TfP verifies it automatically against the bound instance.

Using an ordinary SAT solver is expected and encouraged.

Instance

Provenance: TfP dogfood fixture — deterministically generated random 3-SAT with a planted satisfying assignment (generator generateCnf in the TfP repository, seed 101, 20 variables, 91 clauses). Not a research benchmark; satisfiability is guaranteed by construction.
SHA-256 of the CNF text below: eef24648920b3ca871342d0b1554341c350de9bf3ec1230aa0b4a578a6ced3cf — the same bytes are bound as the Contract's instance reference input.

c TfP dogfood fixture: planted-assignment random 3-SAT (seed=101)
p cnf 20 91
16 6 -2 0
9 -18 15 0
-3 11 1 0
20 9 -3 0
10 19 -3 0
-8 16 -3 0
18 -8 -5 0
2 -3 -16 0
-5 -13 -14 0
17 13 -12 0
-11 20 17 0
-20 2 -8 0
-3 18 12 0
6 11 2 0
11 10 7 0
17 18 15 0
-7 -6 20 0
-14 20 -15 0
18 -11 8 0
-9 10 1 0
-6 5 14 0
2 9 14 0
-12 17 -8 0
-1 20 -17 0
-4 13 -18 0
2 10 -6 0
-12 11 -2 0
11 -4 6 0
9 -6 11 0
13 1 -6 0
10 -14 -3 0
16 -7 -6 0
5 16 -7 0
8 9 -2 0
-14 6 -13 0
-8 17 -13 0
9 -10 -12 0
13 -17 -20 0
2 11 -3 0
-7 10 -12 0
12 11 -4 0
20 -11 5 0
-8 -7 15 0
5 1 -2 0
4 9 -16 0
10 20 12 0
-4 13 -14 0
-8 3 6 0
1 -13 20 0
3 -5 18 0
-6 11 1 0
-7 -1 -18 0
-7 -2 -9 0
-16 -8 3 0
10 -11 2 0
11 14 16 0
-7 -12 5 0
20 -7 -19 0
11 -8 9 0
-4 11 -19 0
-5 6 9 0
-13 1 4 0
6 -3 2 0
15 -2 10 0
-19 -16 -6 0
18 2 7 0
2 -5 -3 0
17 -2 13 0
-14 -17 -6 0
11 13 1 0
4 -14 18 0
-3 -15 1 0
19 8 -6 0
10 -4 -8 0
-17 -10 1 0
-14 -7 -17 0
-6 1 5 0
-7 20 -14 0
16 -4 -8 0
-6 -5 7 0
12 8 13 0
16 1 -14 0
9 -6 -14 0
-8 -7 19 0
19 16 -11 0
5 20 -18 0
15 20 -12 0
1 5 9 0
8 -7 5 0
-10 -12 20 0
1 13 10 0

Browse revision specification

Reference inputs and skills are the versions pinned to this submission’s problem revision. They provide context and are separate from the submitted files.

Attempt notes and history →

Satisfy a small 3-SAT instance (20 variables)

Submitted summary

Submitted files 1

Source 1

Consulted during this attempt 0

Instance

Document