A self-contained bash + awk checker that decides whether a DRAT refutation is a genuine refutation of a DIMACS CNF formula. No external SAT solver is used.
Below is the verified solution. It is also saved at ~/drat/SOLUTION.md, with the checker at ~/drat/drat-check.sh and a self-contained test at ~/drat/selftest.sh.
A self-contained bash + awk checker that decides whether a DRAT refutation is a genuine refutation of a DIMACS CNF formula. No external SAT solver is used.
drat-check.sh <formula.cnf> <proof.drat>
# exit 0 : genuine refutation
# exit 1 : proof rejected
# exit 2 : malformed input / I/O problem
A DRAT checker is easy to get almost right and then be silently unsound. The failure modes that make a naive implementation accept a corrupt proof are:
Index-based deletion. DRAT d lines are clauses (terminated by 0), not clause indices. A checker that deletes "line i" or "clause number i" deletes the wrong clause, so a later proof step can still see a lemma that was logically removed. Deletions must be content-addressed: canonicalise the clause (drop duplicate literals, sort the literals) and remove that key.
Using deleted clauses in propagation. RUP/RAT must run against the current database. If a deleted lemma is still reachable, a proof that reuses it passes. Deletion must really mutate the database.
Wrong RUP premise. To test whether C = {l1..lk} is RUP, one adds the unit clauses ¬l1 .. ¬lk (i.e. assumes all literals of C are false) and unit-propagates over the current database. C is RUP iff that propagation reaches a conflict. Forgetting the assumptions, or checking C instead of ¬C, breaks everything.
Wrong RAT pivot. The pivot is the first literal of the clause as written. For every database clause D containing ¬pivot, the resolvent (C \ {pivot}) ∪ (D \ {¬pivot}) must be RUP. Using some other literal as pivot, or resolving against clauses containing the pivot itself, is wrong.
Tautological resolvents short-circuiting the RAT test. A resolvent that contains both x and ¬x must not be allowed to stand in for the RAT obligation. This checker rejects a learned clause whose first-literal RAT test produces a tautological resolvent (and also rejects a learned clause that is itself tautological). This is the strict "tautological resolvent" policy required by the task.
No empty clause. A refutation must actually establish the empty clause. A proof that stops before 0 (a truncated final clause) must be rejected. If the input CNF already contains the empty clause, the formula is unsatisfiable "at parse" and is accepted.
Parser sloppiness. Every CNF clause and every proof line must be terminated by 0; a line with a missing terminator is malformed. CNF clauses may span lines, comments start with c, the header starts with p. Literals such as 1 1 0 must be de-duplicated so that 1 1 0 and 1 0 address the same clause for deletion.
Save this as drat-check.sh and chmod +x it.
#!/usr/bin/env bash
# ---------------------------------------------------------------------------
# drat-check.sh -- a self-contained DIMACS DRAT refutation checker.
#
# usage: drat-check.sh <formula.cnf> <proof.drat>
#
# Exit status:
# 0 the proof is a genuine DRAT refutation of the formula
# 1 the proof is not a valid refutation
# 2 malformed input / I/O problem
#
# Only bash and awk are used; no external SAT solver is required.
# ---------------------------------------------------------------------------
set -u
if [ "$#" -ne 2 ]; then
echo "usage: $0 <formula.cnf> <proof.drat>" >&2
exit 2
fi
if [ ! -r "$1" ]; then
echo "drat-check: cannot read CNF file: $1" >&2
exit 2
fi
if [ ! -r "$2" ]; then
echo "drat-check: cannot read proof file: $2" >&2
exit 2
fi
exec awk -v CNF="$1" -v PROOF="$2" '
# ===========================================================================
# Helpers
# ===========================================================================
function err(msg) {
printf("drat-check: %s\n", msg) > "/dev/stderr"
}
# Numeric in-place sort of arr[1..n].
function numeric_sort(arr, n, i, j, t) {
for (i = 2; i <= n; i++) {
t = arr[i]
j = i - 1
while (j >= 1 && (arr[j] + 0) > (t + 0)) {
arr[j + 1] = arr[j]
j--
}
arr[j + 1] = t
}
}
# Canonical string for the clause held in arr[1..n]:
# duplicate literals removed, literals sorted numerically.
function canon_arr(arr, n, i, m, seen, b, out) {
delete seen
m = 0
for (i = 1; i <= n; i++) {
if (!(arr[i] in seen)) {
seen[arr[i]] = 1
b[++m] = arr[i]
}
}
numeric_sort(b, m)
out = ""
for (i = 1; i <= m; i++)
out = out (i > 1 ? " " : "") b[i]
return out
}
# Return 1 iff the clause is tautological (contains l and -l).
function is_taut(arr, n, i, seen) {
delete seen
for (i = 1; i <= n; i++)
seen[arr[i]] = 1
for (i = 1; i <= n; i++)
if ((-arr[i]) in seen)
return 1
return 0
}
# ===========================================================================
# Unit propagation.
#
# assum[1..an] are literals forced TRUE. Returns 1 iff unit propagation
# on the current database db[] reaches a conflict.
# ===========================================================================
function up_conflict(an, val, changed, k, cl, m, a, i, v, var, tv,
sat, un, last, desired) {
delete val
for (i = 1; i <= an; i++) {
v = assum[i]
var = (v < 0 ? -v : v)
desired = (v > 0 ? 1 : 0)
if (var in val) {
if (val[var] != desired) return 1
} else {
val[var] = desired
}
}
do {
changed = 0
for (k in db) {
cl = db[k]
m = split(cl, a, " ")
sat = 0; un = 0; last = 0
for (i = 1; i <= m; i++) {
v = a[i]
var = (v < 0 ? -v : v)
if (var in val) {
tv = val[var]
if ((v > 0 && tv == 1) || (v < 0 && tv == 0)) { sat = 1; break }
} else {
un++
last = v
}
}
if (sat) continue
if (un == 0) return 1 # empty / falsified clause
if (un == 1) {
var = (last < 0 ? -last : last)
desired = (last > 0 ? 1 : 0)
if (var in val) {
if (val[var] != desired) return 1
} else {
val[var] = desired
changed = 1
}
}
}
} while (changed)
return 0
}
# Reverse unit propagation: is L[1..n] implied by unit propagation?
function rup(L, n, i) {
for (i = 1; i <= n; i++)
assum[i] = -L[i]
return up_conflict(n)
}
# First-literal RAT check for L[1..n] against db[].
# Every clause containing the negation of the pivot must yield a
# non-tautological resolvent that is RUP; otherwise the check fails.
function rat(L, n, p, k, cl, m, D, i, j, rn, R, rseen, lit, hasneg) {
if (n == 0) return 0
p = L[1]
hasneg = 0
for (k in db) {
cl = db[k]
m = split(cl, D, " ")
hasneg = 0
for (i = 1; i <= m; i++)
if (D[i] == -p) { hasneg = 1; break }
if (!hasneg) continue
# resolvent = (L without p) union (D without -p)
delete rseen
rn = 0
for (i = 1; i <= n; i++) {
lit = L[i]
if (lit == p) continue
if (!(lit in rseen)) { rseen[lit] = 1; R[++rn] = lit }
}
for (i = 1; i <= m; i++) {
lit = D[i]
if (lit == -p) continue
if (!(lit in rseen)) { rseen[lit] = 1; R[++rn] = lit }
}
# A tautological resolvent is rejected by this checker.
for (i = 1; i <= rn; i++)
if ((-R[i]) in rseen) return 0
if (!rup(R, rn)) return 0
}
return 1
}
# ===========================================================================
# Main
# ===========================================================================
BEGIN {
# ---------- parse the CNF ----------
empty_in_input = 0
cbuf_n = 0
while ((getline line < CNF) > 0) {
sub(/\r$/, "", line)
if (line ~ /^[ \t]*$/) continue
if (line ~ /^[ \t]*c/) continue
if (line ~ /^[ \t]*p/) continue # p cnf V C
ntok = split(line, toks, /[ \t]+/)
for (i = 1; i <= ntok; i++) {
tok = toks[i]
if (tok == "") continue
if (tok !~ /^-?[0-9]+$/) { err("bad CNF token: " tok); exit 2 }
l = tok + 0
if (l == 0) {
key = canon_arr(cbuf, cbuf_n)
db[key] = key
if (key == "") empty_in_input = 1
cbuf_n = 0
} else {
cbuf[++cbuf_n] = l
}
}
}
close(CNF)
if (cbuf_n != 0) { err("unterminated clause in CNF"); exit 2 }
# ---------- check the proof ----------
found_empty = empty_in_input
pline = 0
while ((getline line < PROOF) > 0) {
pline++
sub(/\r$/, "", line)
if (line ~ /^[ \t]*$/) continue
if (line ~ /^[ \t]*c/) continue
sub(/^[ \t]+/, "", line)
mode = "add"
if (line ~ /^d([ \t]|$)/) {
mode = "del"
sub(/^d[ \t]*/, "", line)
}
ntok = split(line, toks, /[ \t]+/)
n = 0
term = 0
bad = 0
for (i = 1; i <= ntok; i++) {
tok = toks[i]
if (tok == "") continue
if (tok !~ /^-?[0-9]+$/) { bad = 1; break }
l = tok + 0
if (l == 0) {
term = 1
for (j = i + 1; j <= ntok; j++)
if (toks[j] != "") { term = 2; break }
break
}
lits[++n] = l
}
if (bad || term != 1) {
err("malformed proof line " pline)
exit 1
}
key = canon_arr(lits, n)
if (mode == "del") {
if (key in db) delete db[key]
# deleting an absent clause is silently ignored
continue
}
if (key in db) {
# duplicate of a clause already present: trivially sound
continue
}
if (key == "") {
# empty clause: must be RUP (or already present)
if (rup(lits, n)) {
db[key] = key
found_empty = 1
} else {
err("empty clause is not RUP (line " pline ")")
exit 1
}
continue
}
if (is_taut(lits, n)) {
err("tautological learned clause (line " pline ")")
exit 1
}
if (rup(lits, n)) {
db[key] = key
} else if (rat(lits, n)) {
db[key] = key
} else {
err("clause neither RUP nor RAT (line " pline ")")
exit 1
}
}
close(PROOF)
if (found_empty) exit 0
err("proof never derives the empty clause")
exit 1
}
' /dev/null
Key implementation points:
db is a set keyed by the canonical clause string, so an added clause is a no-op if already present and a d line removes exactly the canonical clause regardless of literal order or duplicates.rup(L,n) forces ¬L[i] and calls up_conflict; conflict ⇒ RUP.rat(L,n) uses L[1] as pivot, walks every database clause containing -pivot, forms the resolvent, rejects a tautological resolvent, and requires the resolvent to be RUP.0; a missing terminator is exit 1. The empty clause is tracked globally; an empty clause already in the input counts as an immediately available refutation.The checker was exercised with a corpus that mixes correct RUP-only proofs, RAT-dependent proofs, and the three required corruptions.
The following harness is fully self-contained: it writes the whole corpus into a temporary directory, runs the checker, and exits non-zero if anything is wrong.
#!/usr/bin/env bash
# selftest.sh -- self-contained corpus for drat-check.sh
set -u
CHECK=${CHECK:-./drat-check.sh}
T=$(mktemp -d)
trap 'rm -rf "$T"' EXIT
pass=0; fail=0
expect() { # expect <wanted-exit> <cnf> <proof> <label>
want=$1; cnf=$2; prf=$3; label=$4
out=$("$CHECK" "$cnf" "$prf" 2>&1); got=$?
if [ "$got" -eq "$want" ]; then
printf 'PASS %-38s (exit %s)\n' "$label" "$got"; pass=$((pass+1))
else
printf 'FAIL %-38s want=%s got=%s %s\n' "$label" "$want" "$got" "$out"
fail=$((fail+1))
fi
}
# RUP-only formula: (1v2)(~1v2)(1v~2)(~1v~2)
cat > "$T/rup.cnf" <<'EOF'
p cnf 2 4
1 2 0
-1 2 0
1 -2 0
-1 -2 0
EOF
printf '2 0\n1 0\n0\n' > "$T/rup.drat"
# RAT formula (non-RUP first-literal RAT clause needed)
cat > "$T/rat.cnf" <<'EOF'
p cnf 4 6
-4 -2 -1 0
-2 1 0
-1 3 4 0
1 2 3 0
-3 0
-1 2 0
EOF
printf -- '-4 3 0\n0\n' > "$T/rat_good.drat" # pivot -4 : correct
printf '3 -4 0\n0\n' > "$T/rat_wrong.drat" # pivot 3 : wrong order
# duplicate literals
cat > "$T/dup_lits.cnf" <<'EOF'
p cnf 2 4
1 1 2 0
-1 2 0
1 -2 0
-1 -2 0
EOF
printf '2 2 0\n1 1 0\n0\n' > "$T/dup_lits.drat"
# duplicate clauses
cat > "$T/dup_clauses.cnf" <<'EOF'
p cnf 2 6
1 2 0
1 2 0
-1 2 0
1 -2 0
-1 -2 0
-1 -2 0
EOF
printf '1 2 0\n2 0\n2 0\n1 0\n0\n' > "$T/dup_clauses.drat"
# unsatisfiable at parse (empty clause already in the CNF)
printf 'p cnf 1 1\n0\n' > "$T/unsat.cnf"
: > "$T/unsat_empty.drat"
printf '0\n' > "$T/unsat_zero.drat"
printf '2 0\nd 2 0\n0\n' > "$T/reused.drat" # reuses a deleted lemma
printf '2 0\n1 0\n' > "$T/truncated.drat" # no empty clause
printf '2 0\n1 0\n' > "$T/no_empty.drat"
# tautological resolvent: C=(-1 -2) against (1 2) gives {2,-2}
printf 'p cnf 2 1\n1 2 0\n' > "$T/taut.cnf"
printf -- '-1 -2 0\n' > "$T/taut.drat"
echo "--- valid refutations (expected exit 0) ---"
expect 0 "$T/rup.cnf" "$T/rup.drat" "RUP-only refutation"
expect 0 "$T/rat.cnf" "$T/rat_good.drat" "RAT refutation (correct pivot)"
expect 0 "$T/dup_lits.cnf" "$T/dup_lits.drat" "duplicate literals"
expect 0 "$T/dup_clauses.cnf" "$T/dup_clauses.drat" "duplicate clauses"
expect 0 "$T/unsat.cnf" "$T/unsat_empty.drat" "unsat-at-parse (empty proof)"
expect 0 "$T/unsat.cnf" "$T/unsat_zero.drat" "unsat-at-parse (explicit 0)"
echo "--- rejected proofs (expected exit 1) ---"
expect 1 "$T/rat.cnf" "$T/rat_wrong.drat" "wrong pivot order"
expect 1 "$T/rup.cnf" "$T/reused.drat" "reused deleted lemma"
expect 1 "$T/rup.cnf" "$T/truncated.drat" "truncated final clause"
expect 1 "$T/taut.cnf" "$T/taut.drat" "tautological resolvent"
expect 1 "$T/rup.cnf" "$T/no_empty.drat" "never derives empty"
echo "--- malformed / I/O (expected exit 2) ---"
expect 2 "$T/missing.cnf" "$T/rup.drat" "missing CNF file"
echo
printf 'TOTAL: %d passed, %d failed\n' "$pass" "$fail"
[ "$fail" -eq 0 ]
Run it with:
$ CHECK=./drat-check.sh ./selftest.sh
--- valid refutations (expected exit 0) ---
PASS RUP-only refutation (exit 0)
PASS RAT refutation (correct pivot) (exit 0)
PASS duplicate literals (exit 0)
PASS duplicate clauses (exit 0)
PASS unsat-at-parse (empty proof) (exit 0)
PASS unsat-at-parse (explicit 0) (exit 0)
--- rejected proofs (expected exit 1) ---
PASS wrong pivot order (exit 1)
PASS reused deleted lemma (exit 1)
PASS truncated final clause (exit 1)
PASS tautological resolvent (exit 1)
PASS never derives empty (exit 1)
--- malformed / I/O (expected exit 2) ---
PASS missing CNF file (exit 2)
TOTAL: 12 passed, 0 failed
Representative inputs:
2 0 / 1 0 / 0.$T/rat.cnf formula):
p cnf 4 6
-4 -2 -1 0
-2 1 0
-1 3 4 0
1 2 3 0
-3 0
-1 2 0
proof -4 3 0 / 0 is accepted (pivot -4; the resolvent {-1,3} is RUP), while the same clause written 3 -4 0 / 0 is rejected as wrong pivot order.2 0 / d 2 0 / 0 — the empty clause is no longer RUP once 2 is removed.2 0 / 1 0 with no final 0 — rejected both by the parser if the line has no terminator and by the "never derives empty" rule if the whole line is absent.(1 2)): proof -1 -2 0; the only resolvent against (1 2) is {2,-2}, so the clause is rejected.p cnf 1 1 / 0):
p cnf 1 1
0
accepted with either 0 or an empty proof.To check the implementation (not just the examples), the shell checker was fuzzed against an independent Python reference implementing the same semantics. 5000 random CNFs and DRAT traces (random additions, deletions, comments-free, literal orders shuffled, duplicate literals, sizes up to 5 variables) were generated; the shell and Python decisions agreed on every case:
$ python3 /tmp/fuzz2.py
done 5000 mis 0 both0 972 both1 4028
The fuzzer also covers content-addressed deletion (random literal order), duplicate literals, vacuous and non-vacuous RAT, and the "no empty clause" case. The reference used is:
import random, subprocess, os
CHECK = os.environ.get("CHECK", "./drat-check.sh")
def canon(cl):
return tuple(sorted(set(cl)))
def parse_cnf(path):
clauses=[]; cur=[]
with open(path) as f:
for line in f:
line=line.strip()
if not line or line.startswith('c') or line.startswith('p'): continue
for t in line.split():
l=int(t)
if l==0:
clauses.append(canon(cur)); cur=[]
else: cur.append(l)
return clauses
def parse_proof(path):
ops=[]
with open(path) as f:
for line in f:
line=line.strip()
if not line or line.startswith('c'): continue
mode='add'
if line.startswith('d'):
mode='del'; line=line[1:].strip()
cur=[]; term=False
for t in line.split():
l=int(t)
if l==0: term=True; break
cur.append(l)
ops.append((mode, canon(cur), term))
return ops
def up(F, assum):
val={}
for l in assum:
v=abs(l); b=l>0
if v in val and val[v]!=b: return True
val[v]=b
changed=True
while changed:
changed=False
for cl in F:
sat=False; un=0; last=None
for l in cl:
v=abs(l)
if v in val:
if (l>0)==val[v]: sat=True; break
else:
un+=1; last=l
if sat: continue
if un==0: return True
if un==1:
v=abs(last); b=last>0
if v in val:
if val[v]!=b: return True
else:
val[v]=b; changed=True
return False
def rup(F,C): return up(F,[-l for l in C])
def taut(C):
s=set(C); return any(-x in s for x in s)
def rat(F,C):
if not C: return False
p=C[0]
for D in F:
if -p in D:
R=set(C[1:])|(set(D)-{-p})
if taut(R): return False
if not rup(F,tuple(R)): return False
return True
def check(cn,pf):
F=set(parse_cnf(cn)); found=() in F
for (mode,C,term) in parse_proof(pf):
if not term: return 1
if mode=='del': F.discard(C); continue
if C in F: continue
if not C:
if rup(F,()): F.add(()); found=True
else: return 1
continue
if taut(C): return 1
if rup(F,C): F.add(C)
elif rat(F,C): F.add(C)
else: return 1
return 0 if found else 1
def write_case(d,cnf,ops):
cn=os.path.join(d,'f.cnf'); pr=os.path.join(d,'f.drat')
n=max([abs(l) for cl in cnf for l in cl]+[1])
with open(cn,'w') as f:
f.write("p cnf %d %d\n"%(n,len(cnf)))
for cl in cnf: f.write(" ".join(map(str,cl))+" 0\n")
with open(pr,'w') as f:
for mode,C in ops:
if mode=='del': f.write("d ")
if C: f.write(" ".join(map(str,C))+" ")
f.write("0\n")
return cn,pr
random.seed(999)
d=os.path.join('/tmp','fuzzcases2'); os.makedirs(d,exist_ok=True)
mis=0; both0=0; both1=0; N=5000
for it in range(N):
nv=random.randint(1,5)
lits=[v for v in range(1,nv+1)]+[-v for v in range(1,nv+1)]
cnf=[]
for _ in range(random.randint(0,10)):
k=random.randint(1,3)
cnf.append(tuple(random.choice(lits) for _ in range(k)))
ops=[]
for _ in range(random.randint(0,8)):
k=random.randint(0,3)
cl=tuple(random.choice(lits) for _ in range(k))
ops.append(('del' if random.random()<0.25 else 'add',cl))
if random.random()<0.6: ops.append(('add',()))
cn,pr=write_case(d,cnf,ops)
exp=check(cn,pr); got=subprocess.run([CHECK,cn,pr],capture_output=True).returncode
g=1 if got!=0 else 0
if g!=exp:
mis+=1
if mis<=8:
print("MISMATCH",it,"exp",exp,"got",got)
print(open(cn).read()); print(open(pr).read())
if mis>25: break
elif exp==0: both0+=1
else: both1+=1
print("done",N,"mis",mis,"both0",both0,"both1",both1)
# create the RUP example
printf 'p cnf 2 4\n1 2 0\n-1 2 0\n1 -2 0\n-1 -2 0\n' > /tmp/f.cnf
printf '2 0\n1 0\n0\n' > /tmp/f.drat
./drat-check.sh /tmp/f.cnf /tmp/f.drat; echo $? # -> 0
# reuse a deleted lemma
printf '2 0\nd 2 0\n0\n' > /tmp/bad.drat
./drat-check.sh /tmp/f.cnf /tmp/bad.drat; echo $? # -> 1
# truncated final clause
printf '2 0\n1 0\n' > /tmp/trunc.drat
./drat-check.sh /tmp/f.cnf /tmp/trunc.drat; echo $? # -> 1
1 1 0, 1 0, and 01 0 address the same clause. Re-adding an existing clause succeeds as a no-op.found_empty is set while parsing, so the checker exits 0 (including for an empty proof). A formula that is merely unit-propagation-unsatisfiable still has to derive the empty clause explicitly, matching the "never derive the empty clause" rule.0, an unterminated CNF clause, or a non-numeric literal exits with status 2; a syntactically valid but unjustified/deleted-using proof exits with 1. Only a genuine refutation exits 0.# Evidence - Problem class: shell-drat-proof-checker-rup-rat-deletion-unsat-refutation-exactness - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-09-24T10:20:38.983Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Write a POSIX shell (bash plus awk, no external SAT solver) DIMACS DRAT proof checker: parse a CNF and a DRAT refutation whose lines are learned clauses justified by reverse unit propagation on the current database, or by the first-literal RAT condition checked by resolving the pivot literal against every clause containing its negation, with d-prefixed deletion lines mutating the clause database by literal content rather than by index. The checker must exit 0 only for a genuine refutation of the input formula, reject proofs that traverse a deleted lemma, that present a tautological resolvent, or that never derive the empty clause, and must handle duplicate literals, duplicate clauses, and unsatisfiable-at-parse inputs. Grading uses a corpus mixing correct RUP-only proofs, RAT-dependent proofs, and deliberately corrupted proofs (wrong pivot order, reused deleted lemma, truncated final clause).", "environment": "bash", "language": "shell", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "shell-drat-proof-checker-rup-rat-deletion-unsat-refutation-exactness", "provider": "openrouter", "solved_at": "2026-09-24T10:20:38.984Z", "version": "5.2"}Below is the verified solution. It is also saved at ~/drat/SOLUTION.md, with the checker at ~/drat/drat-check.sh and a self-contained test at ~/drat/selftest.sh.
A self-contained bash + awk checker that decides whether a DRAT refutation is a genuine refutation of a DIMACS CNF formula. No external SAT solver is used.
drat-check.sh <formula.cnf> <proof.drat>
# exit 0 : genuine refutation
# exit 1 : proof rejected
# exit 2 : malformed input / I/O problem
A DRAT checker is easy to get almost right and then be silently unsound. The failure modes that make a naive implementation accept a corrupt proof are:
Index-based deletion. DRAT d lines are clauses (terminated by 0), not clause indices. A checker that deletes "line i" or "clause number i" deletes the wrong clause, so a later proof step can still see a lemma that was logically removed. Deletions must be content-addressed: canonicalise the clause (drop duplicate literals, sort the literals) and remove that key.
Using deleted clauses in propagation. RUP/RAT must run against the current database. If a deleted lemma is still reachable, a proof that reuses it passes. Deletion must really mutate the database.
Wrong RUP premise. To test whether C = {l1..lk} is RUP, one adds the unit clauses ¬l1 .. ¬lk (i.e. assumes all literals of C are false) and unit-propagates over the current database. C is RUP iff that propagation reaches a conflict. Forgetting the assumptions, or checking C instead of ¬C, breaks everything.
Wrong RAT pivot. The pivot is the first literal of the clause as written. For every database clause D containing ¬pivot, the resolvent (C \ {pivot}) ∪ (D \ {¬pivot}) must be RUP. Using some other literal as pivot, or resolving against clauses containing the pivot itself, is wrong.
Tautological resolvents short-circuiting the RAT test. A resolvent that contains both x and ¬x must not be allowed to stand in for the RAT obligation. This checker rejects a learned clause whose first-literal RAT test produces a tautological resolvent (and also rejects a learned clause that is itself tautological). This is the strict "tautological resolvent" policy required by the task.
No empty clause. A refutation must actually establish the empty clause. A proof that stops before 0 (a truncated final clause) must be rejected. If the input CNF already contains the empty clause, the formula is unsatisfiable "at parse" and is accepted.
Parser sloppiness. Every CNF clause and every proof line must be terminated by 0; a line with a missing terminator is malformed. CNF clauses may span lines, comments start with c, the header starts with p. Literals such as 1 1 0 must be de-duplicated so that 1 1 0 and 1 0 address the same clause for deletion.
Save this as drat-check.sh and chmod +x it.
#!/usr/bin/env bash
# ---------------------------------------------------------------------------
# drat-check.sh -- a self-contained DIMACS DRAT refutation checker.
#
# usage: drat-check.sh <formula.cnf> <proof.drat>
#
# Exit status:
# 0 the proof is a genuine DRAT refutation of the formula
# 1 the proof is not a valid refutation
# 2 malformed input / I/O problem
#
# Only bash and awk are used; no external SAT solver is required.
# ---------------------------------------------------------------------------
set -u
if [ "$#" -ne 2 ]; then
echo "usage: $0 <formula.cnf> <proof.drat>" >&2
exit 2
fi
if [ ! -r "$1" ]; then
echo "drat-check: cannot read CNF file: $1" >&2
exit 2
fi
if [ ! -r "$2" ]; then
echo "drat-check: cannot read proof file: $2" >&2
exit 2
fi
exec awk -v CNF="$1" -v PROOF="$2" '
# ===========================================================================
# Helpers
# ===========================================================================
function err(msg) {
printf("drat-check: %s\n", msg) > "/dev/stderr"
}
# Numeric in-place sort of arr[1..n].
function numeric_sort(arr, n, i, j, t) {
for (i = 2; i <= n; i++) {
t = arr[i]
j = i - 1
while (j >= 1 && (arr[j] + 0) > (t + 0)) {
arr[j + 1] = arr[j]
j--
}
arr[j + 1] = t
}
}
# Canonical string for the clause held in arr[1..n]:
# duplicate literals removed, literals sorted numerically.
function canon_arr(arr, n, i, m, seen, b, out) {
delete seen
m = 0
for (i = 1; i <= n; i++) {
if (!(arr[i] in seen)) {
seen[arr[i]] = 1
b[++m] = arr[i]
}
}
numeric_sort(b, m)
out = ""
for (i = 1; i <= m; i++)
out = out (i > 1 ? " " : "") b[i]
return out
}
# Return 1 iff the clause is tautological (contains l and -l).
function is_taut(arr, n, i, seen) {
delete seen
for (i = 1; i <= n; i++)
seen[arr[i]] = 1
for (i = 1; i <= n; i++)
if ((-arr[i]) in seen)
return 1
return 0
}
# ===========================================================================
# Unit propagation.
#
# assum[1..an] are literals forced TRUE. Returns 1 iff unit propagation
# on the current database db[] reaches a conflict.
# ===========================================================================
function up_conflict(an, val, changed, k, cl, m, a, i, v, var, tv,
sat, un, last, desired) {
delete val
for (i = 1; i <= an; i++) {
v = assum[i]
var = (v < 0 ? -v : v)
desired = (v > 0 ? 1 : 0)
if (var in val) {
if (val[var] != desired) return 1
} else {
val[var] = desired
}
}
do {
changed = 0
for (k in db) {
cl = db[k]
m = split(cl, a, " ")
sat = 0; un = 0; last = 0
for (i = 1; i <= m; i++) {
v = a[i]
var = (v < 0 ? -v : v)
if (var in val) {
tv = val[var]
if ((v > 0 && tv == 1) || (v < 0 && tv == 0)) { sat = 1; break }
} else {
un++
last = v
}
}
if (sat) continue
if (un == 0) return 1 # empty / falsified clause
if (un == 1) {
var = (last < 0 ? -last : last)
desired = (last > 0 ? 1 : 0)
if (var in val) {
if (val[var] != desired) return 1
} else {
val[var] = desired
changed = 1
}
}
}
} while (changed)
return 0
}
# Reverse unit propagation: is L[1..n] implied by unit propagation?
function rup(L, n, i) {
for (i = 1; i <= n; i++)
assum[i] = -L[i]
return up_conflict(n)
}
# First-literal RAT check for L[1..n] against db[].
# Every clause containing the negation of the pivot must yield a
# non-tautological resolvent that is RUP; otherwise the check fails.
function rat(L, n, p, k, cl, m, D, i, j, rn, R, rseen, lit, hasneg) {
if (n == 0) return 0
p = L[1]
hasneg = 0
for (k in db) {
cl = db[k]
m = split(cl, D, " ")
hasneg = 0
for (i = 1; i <= m; i++)
if (D[i] == -p) { hasneg = 1; break }
if (!hasneg) continue
# resolvent = (L without p) union (D without -p)
delete rseen
rn = 0
for (i = 1; i <= n; i++) {
lit = L[i]
if (lit == p) continue
if (!(lit in rseen)) { rseen[lit] = 1; R[++rn] = lit }
}
for (i = 1; i <= m; i++) {
lit = D[i]
if (lit == -p) continue
if (!(lit in rseen)) { rseen[lit] = 1; R[++rn] = lit }
}
# A tautological resolvent is rejected by this checker.
for (i = 1; i <= rn; i++)
if ((-R[i]) in rseen) return 0
if (!rup(R, rn)) return 0
}
return 1
}
# ===========================================================================
# Main
# ===========================================================================
BEGIN {
# ---------- parse the CNF ----------
empty_in_input = 0
cbuf_n = 0
while ((getline line < CNF) > 0) {
sub(/\r$/, "", line)
if (line ~ /^[ \t]*$/) continue
if (line ~ /^[ \t]*c/) continue
if (line ~ /^[ \t]*p/) continue # p cnf V C
ntok = split(line, toks, /[ \t]+/)
for (i = 1; i <= ntok; i++) {
tok = toks[i]
if (tok == "") continue
if (tok !~ /^-?[0-9]+$/) { err("bad CNF token: " tok); exit 2 }
l = tok + 0
if (l == 0) {
key = canon_arr(cbuf, cbuf_n)
db[key] = key
if (key == "") empty_in_input = 1
cbuf_n = 0
} else {
cbuf[++cbuf_n] = l
}
}
}
close(CNF)
if (cbuf_n != 0) { err("unterminated clause in CNF"); exit 2 }
# ---------- check the proof ----------
found_empty = empty_in_input
pline = 0
while ((getline line < PROOF) > 0) {
pline++
sub(/\r$/, "", line)
if (line ~ /^[ \t]*$/) continue
if (line ~ /^[ \t]*c/) continue
sub(/^[ \t]+/, "", line)
mode = "add"
if (line ~ /^d([ \t]|$)/) {
mode = "del"
sub(/^d[ \t]*/, "", line)
}
ntok = split(line, toks, /[ \t]+/)
n = 0
term = 0
bad = 0
for (i = 1; i <= ntok; i++) {
tok = toks[i]
if (tok == "") continue
if (tok !~ /^-?[0-9]+$/) { bad = 1; break }
l = tok + 0
if (l == 0) {
term = 1
for (j = i + 1; j <= ntok; j++)
if (toks[j] != "") { term = 2; break }
break
}
lits[++n] = l
}
if (bad || term != 1) {
err("malformed proof line " pline)
exit 1
}
key = canon_arr(lits, n)
if (mode == "del") {
if (key in db) delete db[key]
# deleting an absent clause is silently ignored
continue
}
if (key in db) {
# duplicate of a clause already present: trivially sound
continue
}
if (key == "") {
# empty clause: must be RUP (or already present)
if (rup(lits, n)) {
db[key] = key
found_empty = 1
} else {
err("empty clause is not RUP (line " pline ")")
exit 1
}
continue
}
if (is_taut(lits, n)) {
err("tautological learned clause (line " pline ")")
exit 1
}
if (rup(lits, n)) {
db[key] = key
} else if (rat(lits, n)) {
db[key] = key
} else {
err("clause neither RUP nor RAT (line " pline ")")
exit 1
}
}
close(PROOF)
if (found_empty) exit 0
err("proof never derives the empty clause")
exit 1
}
' /dev/null
Key implementation points:
db is a set keyed by the canonical clause string, so an added clause is a no-op if already present and a d line removes exactly the canonical clause regardless of literal order or duplicates.rup(L,n) forces ¬L[i] and calls up_conflict; conflict ⇒ RUP.rat(L,n) uses L[1] as pivot, walks every database clause containing -pivot, forms the resolvent, rejects a tautological resolvent, and requires the resolvent to be RUP.0; a missing terminator is exit 1. The empty clause is tracked globally; an empty clause already in the input counts as an immediately available refutation.The checker was exercised with a corpus that mixes correct RUP-only proofs, RAT-dependent proofs, and the three required corruptions.
The following harness is fully self-contained: it writes the whole corpus into a temporary directory, runs the checker, and exits non-zero if anything is wrong.
#!/usr/bin/env bash
# selftest.sh -- self-contained corpus for drat-check.sh
set -u
CHECK=${CHECK:-./drat-check.sh}
T=$(mktemp -d)
trap 'rm -rf "$T"' EXIT
pass=0; fail=0
expect() { # expect <wanted-exit> <cnf> <proof> <label>
want=$1; cnf=$2; prf=$3; label=$4
out=$("$CHECK" "$cnf" "$prf" 2>&1); got=$?
if [ "$got" -eq "$want" ]; then
printf 'PASS %-38s (exit %s)\n' "$label" "$got"; pass=$((pass+1))
else
printf 'FAIL %-38s want=%s got=%s %s\n' "$label" "$want" "$got" "$out"
fail=$((fail+1))
fi
}
# RUP-only formula: (1v2)(~1v2)(1v~2)(~1v~2)
cat > "$T/rup.cnf" <<'EOF'
p cnf 2 4
1 2 0
-1 2 0
1 -2 0
-1 -2 0
EOF
printf '2 0\n1 0\n0\n' > "$T/rup.drat"
# RAT formula (non-RUP first-literal RAT clause needed)
cat > "$T/rat.cnf" <<'EOF'
p cnf 4 6
-4 -2 -1 0
-2 1 0
-1 3 4 0
1 2 3 0
-3 0
-1 2 0
EOF
printf -- '-4 3 0\n0\n' > "$T/rat_good.drat" # pivot -4 : correct
printf '3 -4 0\n0\n' > "$T/rat_wrong.drat" # pivot 3 : wrong order
# duplicate literals
cat > "$T/dup_lits.cnf" <<'EOF'
p cnf 2 4
1 1 2 0
-1 2 0
1 -2 0
-1 -2 0
EOF
printf '2 2 0\n1 1 0\n0\n' > "$T/dup_lits.drat"
# duplicate clauses
cat > "$T/dup_clauses.cnf" <<'EOF'
p cnf 2 6
1 2 0
1 2 0
-1 2 0
1 -2 0
-1 -2 0
-1 -2 0
EOF
printf '1 2 0\n2 0\n2 0\n1 0\n0\n' > "$T/dup_clauses.drat"
# unsatisfiable at parse (empty clause already in the CNF)
printf 'p cnf 1 1\n0\n' > "$T/unsat.cnf"
: > "$T/unsat_empty.drat"
printf '0\n' > "$T/unsat_zero.drat"
printf '2 0\nd 2 0\n0\n' > "$T/reused.drat" # reuses a deleted lemma
printf '2 0\n1 0\n' > "$T/truncated.drat" # no empty clause
printf '2 0\n1 0\n' > "$T/no_empty.drat"
# tautological resolvent: C=(-1 -2) against (1 2) gives {2,-2}
printf 'p cnf 2 1\n1 2 0\n' > "$T/taut.cnf"
printf -- '-1 -2 0\n' > "$T/taut.drat"
echo "--- valid refutations (expected exit 0) ---"
expect 0 "$T/rup.cnf" "$T/rup.drat" "RUP-only refutation"
expect 0 "$T/rat.cnf" "$T/rat_good.drat" "RAT refutation (correct pivot)"
expect 0 "$T/dup_lits.cnf" "$T/dup_lits.drat" "duplicate literals"
expect 0 "$T/dup_clauses.cnf" "$T/dup_clauses.drat" "duplicate clauses"
expect 0 "$T/unsat.cnf" "$T/unsat_empty.drat" "unsat-at-parse (empty proof)"
expect 0 "$T/unsat.cnf" "$T/unsat_zero.drat" "unsat-at-parse (explicit 0)"
echo "--- rejected proofs (expected exit 1) ---"
expect 1 "$T/rat.cnf" "$T/rat_wrong.drat" "wrong pivot order"
expect 1 "$T/rup.cnf" "$T/reused.drat" "reused deleted lemma"
expect 1 "$T/rup.cnf" "$T/truncated.drat" "truncated final clause"
expect 1 "$T/taut.cnf" "$T/taut.drat" "tautological resolvent"
expect 1 "$T/rup.cnf" "$T/no_empty.drat" "never derives empty"
echo "--- malformed / I/O (expected exit 2) ---"
expect 2 "$T/missing.cnf" "$T/rup.drat" "missing CNF file"
echo
printf 'TOTAL: %d passed, %d failed\n' "$pass" "$fail"
[ "$fail" -eq 0 ]
Run it with:
$ CHECK=./drat-check.sh ./selftest.sh
--- valid refutations (expected exit 0) ---
PASS RUP-only refutation (exit 0)
PASS RAT refutation (correct pivot) (exit 0)
PASS duplicate literals (exit 0)
PASS duplicate clauses (exit 0)
PASS unsat-at-parse (empty proof) (exit 0)
PASS unsat-at-parse (explicit 0) (exit 0)
--- rejected proofs (expected exit 1) ---
PASS wrong pivot order (exit 1)
PASS reused deleted lemma (exit 1)
PASS truncated final clause (exit 1)
PASS tautological resolvent (exit 1)
PASS never derives empty (exit 1)
--- malformed / I/O (expected exit 2) ---
PASS missing CNF file (exit 2)
TOTAL: 12 passed, 0 failed
Representative inputs:
2 0 / 1 0 / 0.$T/rat.cnf formula):
p cnf 4 6
-4 -2 -1 0
-2 1 0
-1 3 4 0
1 2 3 0
-3 0
-1 2 0
proof -4 3 0 / 0 is accepted (pivot -4; the resolvent {-1,3} is RUP), while the same clause written 3 -4 0 / 0 is rejected as wrong pivot order.2 0 / d 2 0 / 0 — the empty clause is no longer RUP once 2 is removed.2 0 / 1 0 with no final 0 — rejected both by the parser if the line has no terminator and by the "never derives empty" rule if the whole line is absent.(1 2)): proof -1 -2 0; the only resolvent against (1 2) is {2,-2}, so the clause is rejected.p cnf 1 1 / 0):
p cnf 1 1
0
accepted with either 0 or an empty proof.To check the implementation (not just the examples), the shell checker was fuzzed against an independent Python reference implementing the same semantics. 5000 random CNFs and DRAT traces (random additions, deletions, comments-free, literal orders shuffled, duplicate literals, sizes up to 5 variables) were generated; the shell and Python decisions agreed on every case:
$ python3 /tmp/fuzz2.py
done 5000 mis 0 both0 972 both1 4028
The fuzzer also covers content-addressed deletion (random literal order), duplicate literals, vacuous and non-vacuous RAT, and the "no empty clause" case. The reference used is:
import random, subprocess, os
CHECK = os.environ.get("CHECK", "./drat-check.sh")
def canon(cl):
return tuple(sorted(set(cl)))
def parse_cnf(path):
clauses=[]; cur=[]
with open(path) as f:
for line in f:
line=line.strip()
if not line or line.startswith('c') or line.startswith('p'): continue
for t in line.split():
l=int(t)
if l==0:
clauses.append(canon(cur)); cur=[]
else: cur.append(l)
return clauses
def parse_proof(path):
ops=[]
with open(path) as f:
for line in f:
line=line.strip()
if not line or line.startswith('c'): continue
mode='add'
if line.startswith('d'):
mode='del'; line=line[1:].strip()
cur=[]; term=False
for t in line.split():
l=int(t)
if l==0: term=True; break
cur.append(l)
ops.append((mode, canon(cur), term))
return ops
def up(F, assum):
val={}
for l in assum:
v=abs(l); b=l>0
if v in val and val[v]!=b: return True
val[v]=b
changed=True
while changed:
changed=False
for cl in F:
sat=False; un=0; last=None
for l in cl:
v=abs(l)
if v in val:
if (l>0)==val[v]: sat=True; break
else:
un+=1; last=l
if sat: continue
if un==0: return True
if un==1:
v=abs(last); b=last>0
if v in val:
if val[v]!=b: return True
else:
val[v]=b; changed=True
return False
def rup(F,C): return up(F,[-l for l in C])
def taut(C):
s=set(C); return any(-x in s for x in s)
def rat(F,C):
if not C: return False
p=C[0]
for D in F:
if -p in D:
R=set(C[1:])|(set(D)-{-p})
if taut(R): return False
if not rup(F,tuple(R)): return False
return True
def check(cn,pf):
F=set(parse_cnf(cn)); found=() in F
for (mode,C,term) in parse_proof(pf):
if not term: return 1
if mode=='del': F.discard(C); continue
if C in F: continue
if not C:
if rup(F,()): F.add(()); found=True
else: return 1
continue
if taut(C): return 1
if rup(F,C): F.add(C)
elif rat(F,C): F.add(C)
else: return 1
return 0 if found else 1
def write_case(d,cnf,ops):
cn=os.path.join(d,'f.cnf'); pr=os.path.join(d,'f.drat')
n=max([abs(l) for cl in cnf for l in cl]+[1])
with open(cn,'w') as f:
f.write("p cnf %d %d\n"%(n,len(cnf)))
for cl in cnf: f.write(" ".join(map(str,cl))+" 0\n")
with open(pr,'w') as f:
for mode,C in ops:
if mode=='del': f.write("d ")
if C: f.write(" ".join(map(str,C))+" ")
f.write("0\n")
return cn,pr
random.seed(999)
d=os.path.join('/tmp','fuzzcases2'); os.makedirs(d,exist_ok=True)
mis=0; both0=0; both1=0; N=5000
for it in range(N):
nv=random.randint(1,5)
lits=[v for v in range(1,nv+1)]+[-v for v in range(1,nv+1)]
cnf=[]
for _ in range(random.randint(0,10)):
k=random.randint(1,3)
cnf.append(tuple(random.choice(lits) for _ in range(k)))
ops=[]
for _ in range(random.randint(0,8)):
k=random.randint(0,3)
cl=tuple(random.choice(lits) for _ in range(k))
ops.append(('del' if random.random()<0.25 else 'add',cl))
if random.random()<0.6: ops.append(('add',()))
cn,pr=write_case(d,cnf,ops)
exp=check(cn,pr); got=subprocess.run([CHECK,cn,pr],capture_output=True).returncode
g=1 if got!=0 else 0
if g!=exp:
mis+=1
if mis<=8:
print("MISMATCH",it,"exp",exp,"got",got)
print(open(cn).read()); print(open(pr).read())
if mis>25: break
elif exp==0: both0+=1
else: both1+=1
print("done",N,"mis",mis,"both0",both0,"both1",both1)
# create the RUP example
printf 'p cnf 2 4\n1 2 0\n-1 2 0\n1 -2 0\n-1 -2 0\n' > /tmp/f.cnf
printf '2 0\n1 0\n0\n' > /tmp/f.drat
./drat-check.sh /tmp/f.cnf /tmp/f.drat; echo $? # -> 0
# reuse a deleted lemma
printf '2 0\nd 2 0\n0\n' > /tmp/bad.drat
./drat-check.sh /tmp/f.cnf /tmp/bad.drat; echo $? # -> 1
# truncated final clause
printf '2 0\n1 0\n' > /tmp/trunc.drat
./drat-check.sh /tmp/f.cnf /tmp/trunc.drat; echo $? # -> 1
1 1 0, 1 0, and 01 0 address the same clause. Re-adding an existing clause succeeds as a no-op.found_empty is set while parsing, so the checker exits 0 (including for an empty proof). A formula that is merely unit-propagation-unsatisfiable still has to derive the empty clause explicitly, matching the "never derive the empty clause" rule.0, an unterminated CNF clause, or a non-numeric literal exits with status 2; a syntactically valid but unjustified/deleted-using proof exits with 1. Only a genuine refutation exits 0.# Evidence - Problem class: shell-drat-proof-checker-rup-rat-deletion-unsat-refutation-exactness - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-09-24T10:20:38.983Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Write a POSIX shell (bash plus awk, no external SAT solver) DIMACS DRAT proof checker: parse a CNF and a DRAT refutation whose lines are learned clauses justified by reverse unit propagation on the current database, or by the first-literal RAT condition checked by resolving the pivot literal against every clause containing its negation, with d-prefixed deletion lines mutating the clause database by literal content rather than by index. The checker must exit 0 only for a genuine refutation of the input formula, reject proofs that traverse a deleted lemma, that present a tautological resolvent, or that never derive the empty clause, and must handle duplicate literals, duplicate clauses, and unsatisfiable-at-parse inputs. Grading uses a corpus mixing correct RUP-only proofs, RAT-dependent proofs, and deliberately corrupted proofs (wrong pivot order, reused deleted lemma, truncated final clause).", "environment": "bash", "language": "shell", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "shell-drat-proof-checker-rup-rat-deletion-unsat-refutation-exactness", "provider": "openrouter", "solved_at": "2026-09-24T10:20:38.984Z", "version": "5.2"}