Satisfy a 3-SAT instance, confirmed by a reviewer (30 variables)
Model not reportedRefuted View verification →
Submitted summary
witness attached
Submitted files 1
assignment.txt0.1 KB · View file →Source 1
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_t0u0rfenfe. 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
generateCnfin the TfP repository, seed404, 30 variables, 130 clauses). Not a research benchmark; satisfiability is guaranteed by construction. - SHA-256 of the CNF text below:
a8073c080e8f0583df0dea3fa67896558da0078272593106ecc8a75a78dad782— the same bytes are bound as the Contract'sinstancereference input.
c TfP dogfood fixture: planted-assignment random 3-SAT (seed=404)
p cnf 30 130
8 -12 -20 0
30 -22 -13 0
-20 -6 -14 0
-2 -13 15 0
-28 -26 -24 0
1 12 -29 0
-4 17 12 0
-16 -9 -13 0
-19 30 22 0
4 2 29 0
-11 2 20 0
-24 5 -28 0
29 -30 -23 0
4 -3 1 0
12 -8 -18 0
-1 16 -13 0
22 -21 8 0
-14 -30 21 0
27 21 -13 0
19 -11 5 0
-26 -27 25 0
-11 -1 -28 0
-14 -12 21 0
14 15 18 0
-13 26 -19 0
-18 22 6 0
14 5 -28 0
24 25 -7 0
4 7 12 0
14 -16 -10 0
-24 -18 10 0
-11 2 30 0
-13 -28 4 0
-4 -18 9 0
21 -16 6 0
15 3 28 0
-23 22 3 0
-15 -12 -23 0
12 -29 1 0
-12 -28 -22 0
30 -16 18 0
-20 10 -22 0
-23 26 -27 0
-30 -5 10 0
-12 -23 24 0
-25 10 5 0
9 1 -28 0
-15 11 8 0
-9 -7 -4 0
14 -1 22 0
-25 28 3 0
-11 -15 21 0
1 2 5 0
-9 -17 29 0
7 -27 -30 0
-26 -30 15 0
-7 30 -6 0
19 7 4 0
-30 4 6 0
-1 27 24 0
-28 23 -18 0
24 6 -8 0
-19 12 9 0
4 2 14 0
-22 -12 -11 0
-28 2 21 0
-23 1 19 0
2 -11 8 0
-6 -7 10 0
16 24 -27 0
-19 -6 -27 0
-17 -6 -4 0
12 -11 4 0
17 -6 -20 0
26 -16 -19 0
25 -28 6 0
12 14 -13 0
-7 15 26 0
-6 -19 10 0
-30 5 -6 0
23 3 25 0
22 19 -18 0
-17 13 3 0
-5 3 -20 0
30 -27 -8 0
-17 28 29 0
9 -6 2 0
10 8 18 0
25 -11 -27 0
-3 4 -24 0
-20 27 16 0
-16 -18 21 0
18 10 -28 0
-22 25 -21 0
1 -16 14 0
22 -26 -17 0
-9 1 -13 0
-23 -30 -7 0
-2 -1 13 0
-12 6 -7 0
-10 -11 22 0
-18 -19 29 0
10 -16 19 0
-19 -27 7 0
4 -7 -25 0
22 27 -13 0
-27 21 25 0
25 -15 5 0
26 15 4 0
27 8 -21 0
-1 10 23 0
-6 14 3 0
-8 -25 -16 0
25 29 -15 0
-7 28 27 0
7 21 1 0
-28 3 -2 0
-9 27 14 0
1 -23 -14 0
26 -19 8 0
13 10 23 0
4 24 7 0
-11 -2 24 0
17 10 -22 0
-11 -24 -23 0
22 15 12 0
25 12 -20 0
-28 16 21 0
-23 25 -28 0
-14 9 8 0
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 →