Solving Boolean Satisfiability Instances

Given a DIMACS CNF file like:

p cnf 1536 6912
-1309 725 -958 0
293 -72 854 0
...

Don't attempt to solve by hand or with ad-hoc reasoning — at this scale (1536 variables, 6912 clauses, 3-SAT), manual/LLM-native deduction cannot reliably find a satisfying assignment or prove unsatisfiability. Instead:

1. Parse and report the instance statistics (variables, clauses, clause-to-variable ratio).
2. Recommend/invoke an actual SAT solver (MiniSat, CaDiCaL, Glucose, Kissat, or Python's pysat/z3-solver) to get a definitive answer.
3. If asked to "reason it out," use structural analysis (unit propagation, pure literal elimination) only as a preprocessing step, not as a complete solving method.

Progress:

• Parse DIMACS header (p cnf <num_vars> <num_clauses>)
• Validate clause count and variable range
• Compute instance statistics (ratio, polarity balance, variable frequency)
• Classify instance (k-SAT type, density regime)
• Apply solver (external tool or library) — never hand-roll DPLL for >50 variables
• Report: SAT/UNSAT, assignment or proof artifact, solver/method used

Step 1: Parse the header

• First non-comment line: p cnf <nvars> <nclauses>
• Each subsequent line is a clause: space-separated integers ending in 0.
• Literal k means variable k is true; -k means variable k is false.

Step 2: Compute statistics

• Clause/variable ratio = nclauses / nvars. For 3-SAT, ratio ≈ 4.27 is the satisfiability phase transition — instances near this ratio are hardest. Ratio = 6912/1536 = 4.5, which is above the critical threshold, meaning the instance is more likely UNSAT (random 3-SAT) but structured instances can differ wildly.
• Check all clause widths (if all length 3 → 3-SAT, decidable but NP-complete).
• Check for unit clauses (length 1) and pure literals (variables appearing with only one polarity) — these simplify the instance immediately via unit propagation / pure literal elimination.

Step 3: Solve

Use a real solver. Example with Python + python-sat:

Python
from pysat.formula import CNF
from pysat.solvers import Glucose3

cnf = CNF(from_file='instance.cnf')
with Glucose3(bootstrap_with=cnf) as solver:
    sat = solver.solve()
    print("SAT" if sat else "UNSAT")
    if sat:
        model = solver.get_model()
        print(model)

Or command-line with MiniSat/CaDiCaL:

Bash
minisat instance.cnf result.txt
cat result.txt

Step 4: Report

• State SAT or UNSAT explicitly.
• If SAT, give the variable assignment (or a compact summary: "model found, see attached").
• If UNSAT, note that the solver's proof (if available, e.g., DRAT) certifies this.
• Always name the solver/method used — never claim to have solved a large instance "by hand."

Example 1: Input: A DIMACS file with p cnf 1536 6912 and 6912 3-literal clauses (as given). Output:

Instance: 1536 variables, 6912 clauses, all 3-SAT (width-3 clauses)
Clause/variable ratio: 4.50 (above random 3-SAT critical threshold ~4.27)
No unit clauses detected; no pure literals detected in a quick scan.
Recommendation: run a complete SAT solver (e.g., CaDiCaL or Glucose) — too large for manual/LLM resolution or naive DPLL.
Action: invoke `pysat`/Glucose3 → report SAT/UNSAT result and model if SAT.

Example 2: Input: p cnf 3 4 with clauses 1 2 0, -1 2 0, 1 -2 0, -1 -2 0 Output:

Small instance (3 vars, 4 clauses) — manual resolution feasible.
Clauses force: (1∨2)∧(¬1∨2)∧(1∨¬2)∧(¬1∨¬2) — this is UNSAT (classic contradiction: requires 1=2 and 1≠2).
Result: UNSAT.