Compendium

Constraint / SMT / SAT Input Languages Family Index

14 min read

Constraint / SMT / SAT Input Languages Family Index

type: language-family-index family: constraint-and-smt-input languages_catalogued: 40 tags: [language-reference, family-index, constraint-and-smt-input, sat, smt, qbf, minizinc, flatzinc, xcsp3, asp, aspcore2, milp, mps, lp, ampl, tptp, drat, lrat, qrat]

Constraint / SMT / SAT Input Languages — Family Index

Family overview

This family is defined by a deliberate inversion of the usual perspective: these are not languages humans want to write, they are the languages solvers actually consume. A modeller writes MiniZinc, Essence, OPL, AMPL, Python with PySAT, or s-expressions in a Z3 script — but the binary that grinds through millions of branching decisions is reading something flatter, simpler, and more boring. This family catalogues that flatter layer: the textual input formats of SAT, SMT, QBF, CSP, ASP, and MILP solvers, plus the proof formats those solvers emit on their way back out. The defining property is that every entry here has a competition or a standard committee behind it, not a programming-language community — these formats exist because two solver authors needed to compare results on the same instance.

The DIMACS CNF lineage is the spine. The format was finalised in May 1993 for the 2nd DIMACS Implementation Challenge (1992–1993, Maximum Clique / Graph Coloring / Satisfiability) and has run every SAT competition since. The header is one line — p cnf <vars> <clauses> — and clauses are space-separated literals terminated by 0. That napkin-scale simplicity is why DIMACS still wins: every SAT solver in 2026 (CaDiCaL, Kissat, Glucose, MapleSAT, IsaSAT, …) reads it natively, and every extension — WCNF (weighted MaxSAT), GCNF (groups), iCNF (incremental), QDIMACS (QBF, 2005) — kept the p <variant> header pattern so that a DIMACS instance is also a valid instance in every successor. SAT Competition 2025’s Main Track UNSAT was won by CaDiCaL-SC2025 (Biere et al., Freiburg) with Kissat-VSA second; both still parse the 1993 spec verbatim.

The SMT-LIB family is the deliberate antithesis. Where DIMACS optimises for parser-on-a-napkin, SMT-LIB optimises for portability across rich theories — bitvectors, arrays, reals, integers, datatypes, floating-point, strings — across Z3 (Microsoft), CVC5 (Stanford/Iowa/NYU), Yices 2 (SRI), MathSAT (FBK), and Boolector/Bitwuzla. The current standard is SMT-LIB 2.6 (reference v2.6-r2021-05-12, Barrett/Fontaine/Tinelli), with 2.7 released as a draft 2025-02-05 and 3.0 under active design as of 2025–2026. The cost of that portability is a verbose, parenthesis-heavy s-expression syntax that almost no one writes by hand — modellers use Python (PySMT), Rosette, or Z3’s Python API and serialise to SMT-LIB only at the wire boundary. Yices 2 also keeps its older native specification language alongside SMT-LIB 2 support.

The CSP / CP world solved the modelling–vs–solving tension with a two-language stack: humans write MiniZinc (high-level: array[1..n] of var 1..n: queens; constraint alldifferent(queens);), and the MiniZinc compiler flattens it to FlatZinc, which is what Gecode, Chuffed, OR-Tools’ CP-SAT, Choco, Picat-SAT, and HiGHS actually consume. The current MiniZinc release (2.9.7, 2026-04-30) ships handbooks for both layers; the FlatZinc spec is published as part of the MiniZinc Handbook (“Interfacing Solvers to FlatZinc”). XCSP3 (currently v3.2, xcsp.org) plays the same role at the XML layer, hosting the XCSP3 competition benchmarks; Essence (St Andrews / York, refined to Essence Prime by the Conjure 2.6 tool, 2024+) sits even higher up the abstraction ladder. ASP standardised on ASPCore-2 (formalised in arXiv:1911.04326, used since 2013 ASP Competitions) — gringo, Clingo, DLV, and WASP all consume it. MIP/LP has its own parallel universe inherited from IBM’s MPSX/360 in the late 1960s — MPS column-oriented, CPLEX LP row-oriented, AMPL .nl binary-or-text — read by Gurobi, CPLEX, HiGHS, SCIP, and COIN-OR. Finally, DRAT/LRAT/FRAT and QRAT are the proof-emission family that grew up alongside CNF/QDIMACS once “trust the solver” stopped being acceptable for safety-critical and journal-grade results.

In our deep library

None of the formats in this family have standalone deep-library notes — they live below the level at which the Languages library catalogues “languages.” Cross-link instead to the modelling and host layers above them:

  • logic-and-constraint — Prolog, Datalog, MiniKanren, Mercury, ASP host languages. The modelling layer above these inputs.
  • theorem-prover-dsls — TPTP and SMT-LIB both heavily used by ATP / ITP systems (Vampire, E, iProver, Lean, Coq/Rocq, Isabelle).
  • notation-spec — these are notation-spec adjacent: machine-consumed serialisations rather than programming languages.
  • python — host language for PySAT, PySMT, OR-Tools’ Python API, MiniZinc Python, PyCSP3, Pyomo, AMPL Python, Gurobipy.
  • cpp — most solvers (CaDiCaL, Kissat, Z3, CVC5, Gurobi, CPLEX, OR-Tools, Gecode) are written in C++; their parsers define what “valid” means.
  • rust — Bitwuzla bindings, IsaSAT (Isabelle-extracted), and several newer competition entrants now ship Rust frontends.
  • scientific — Pyomo, JuMP, PuLP, GAMS, AMPL all live in this neighbourhood.

Tier 3 family table — SAT / QBF / proof formats

FormatFirst appearedOriginTypeStatus (2026)URL
DIMACS CNF1993 (May)2nd DIMACS Implementation Challenge (Rutgers)Plain-text CNF: p cnf V C header + clauses terminated by 0. The lingua franca of SAT for 30+ yearsUniversal, every SAT solver reads ithttps://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/dimacs-cnf.pdf
DIMACS WCNF (MaxSAT)~2006 (MaxSAT Eval era)MaxSAT Evaluation working groupWeighted CNF: each clause prefixed by integer weight; top weight marks hard clauses. Header p wcnf V C top (older)Active, used by MaxSAT Evaluations 2020+ “new format” variant drops the p linehttps://maxsat-evaluations.github.io/2020/rules.html
DIMACS GCNF2003+Group-MUS / group-oriented SAT researchCNF with each clause tagged by a group ID {g}; used for group-MUS extractionNiche, active in MUS researchhttp://www.satcompetition.org/2011/format-benchmarks2011.html
iCNF (incremental CNF)~2008IPASIR / incremental SAT communityExtends DIMACS with a-prefixed assumption lines for solve-under-assumptionsActive, used by IPASIR-compliant incremental solvershttps://github.com/biotomas/ipasir
QDIMACS2005-12-21 (v1.1)QBFLIB / QBFEVAL working groupDIMACS extended with a (universal) and e (existential) quantifier prefix linesActive, the QBF lingua franca; QBFEVAL since 2004https://www.qbflib.org/qdimacs.html
QCIR2014Klieber et al. (CMU)Non-CNF QBF: circuit form with named gates, accepted at QBFEVAL alongside QDIMACSActivehttps://www.cs.cmu.edu/~wklieber/papers/bnp16-qcir.pdf
QAIGER~2017QBF competition working groupAIGER-based QBF input, used at QBFEVAL alongside QDIMACS / QCIRActivehttps://qbf.pages.sai.jku.at/
DRAT2014Heule, Hunt, Wetzler (UT Austin)Clausal proof: each line is a clause addition or d-prefixed deletion preserving satisfiabilityDe facto SAT proof standard; emitted by CaDiCaL, Kissat, Glucose, MapleSAThttps://github.com/marijnheule/drat-trim
LRAT2017Cruz-Filipe, Heule, Hunt, Kaufmann, Schneider-KampDRAT plus per-step resolution hints; checkable in linear time, formally verified checkers exist (Coq, Isabelle, Agda)Active, growing; the format of choice when a proof must itself be trustedhttps://www.cs.utexas.edu/~marijn/publications/lrat.pdf
FRAT2021Tan, Heule, HuntDRAT-with-hints intermediate; >84% median reduction in elaboration-to-LRAT time, >94% peak-memory cutActive, used as DRAT→LRAT pipeline stagehttps://arxiv.org/html/2109.09665
QRAT2014Heule, Seidl, BiereQBF-level analogue of DRAT: ATA / QRATA / QRATU / EUR + clause deletion; can simulate all current QBF preprocessorsActive, candidate standard for QBF certification (QRAT-trim checker)https://www.cs.utexas.edu/~marijn/publications/qrat.pdf

Tier 3 family table — SMT

FormatFirst appearedOriginTypeStatus (2026)URL
SMT-LIB 1.x2003SMT-LIB initiative (Barrett, Stump, Tinelli + working group)First standardised SMT input; theory-typed, less expressive than 2.xLegacy, no longer accepted at SMT-COMPhttps://smt-lib.org/
SMT-LIB 2.02010Barrett, Stump, TinelliMajor redesign: s-expression command language (set-logic, declare-fun, assert, check-sat, get-model)Legacy, superseded by 2.6https://smt-lib.org/papers/smt-lib-reference-v2.0-r10.12.21.pdf
SMT-LIB 2.62017-07-18 (initial), latest revision 2021-05-12Barrett, Fontaine, Tinelli + working groupAdds user-defined algebraic datatypes (declare-datatype(s)); current accepted standard at SMT-COMP through 2025Current standard as of 2026; 2.7 draft (2025-02-05) circulatinghttps://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
SMT-LIB 2.7 (draft)2025-02-05SMT-LIB working groupRefinements to 2.6 ahead of the larger 2.x→3.0 redesignDraft / under reviewhttps://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-02-05.pdf
SMT-LIB 3.0 (in design)announced 2024–2025SMT-LIB working groupLarger redesign signalled by working-group communications; details TBDPre-release / under designhttps://groups.google.com/g/smt-lib/
Yices 2 native2014 (Yices 2.2 paper)Bruno Dutertre et al., SRI InternationalYices’s pre-SMT-LIB specification language (tuples, scalar types, distinct semantics for some theories); kept alongside SMT-LIB 2 supportActive but secondary to SMT-LIB 2https://yices.csl.sri.com/
Z3 SMT-LIB extensions2008+Microsoft Research (de Moura, Bjørner)SMT-LIB 2 plus Z3-specific commands: (simplify), (eval), (rule), fixed-point logic, optimisation (maximize)/(minimize)Active, de facto extension subset many other solvers also accepthttps://microsoft.github.io/z3guide/
CVC5 SMT-LIB extensions~2018+ (CVC5 fork from CVC4)Stanford / Iowa / NYU / SRISMT-LIB 2.6 plus syntax-guided synthesis SyGuS-IF, finite model finding extensionsActivehttps://cvc5.github.io/
MaxSMT extensions~2014+Bjørner, Phan (Z3) and OptiMathSAT (FBK)(assert-soft …) over SMT-LIB; turns SMT into weighted optimisation analogous to MaxSAT-over-CNFActive, used by Z3, OptiMathSAT, νZhttps://theory.stanford.edu/~nikolaj/programmingz3.html

Tier 3 family table — CSP / ASP / CP

FormatFirst appearedOriginTypeStatus (2026)URL
MiniZinc2007 (Nethercote et al., CP’07)Monash + NICTA → MiniZinc FoundationHigh-level CP modelling language; arrays, sets, generators, predicates, global constraints (alldifferent, circuit, cumulative)Active, current 2.9.7 (2026-04-30)https://www.minizinc.org/
FlatZinc2007 (alongside MiniZinc)MiniZinc compiler outputLow-level flat form: var int: x; constraint int_lin_le(...). The actual input most CP solvers consumeActive, spec maintained as part of the MiniZinc Handbookhttps://docs.minizinc.dev/en/stable/fzn-spec.html
XCSP32016 (XCSP3 v3.0); current v3.2Lecoutre, Roussel et al. (CRIL)XML-based constraint instance format; arrays of variables, groups, blocks, meta-constraints; hosts XCSP3 competition benchmarksActivehttps://xcsp.org/
Essence2008 (Frisch et al., AIJ)York / St AndrewsHigh-level abstract specification language with set, multiset, partition, function, relation types — closer to Z than to MiniZincActive, current Conjure 2.6 (2024+)https://conjure.readthedocs.io/en/latest/essence.html
Essence Prime2008+St AndrewsMedium-level CP modelling language; the Conjure refinement target between abstract Essence and solver inputsActivehttps://conjure.readthedocs.io/en/latest/
ASPCore-22012 draft, formalised in arXiv:1911.04326 (2019)ASP Standardization Working Group (Calimeri, Faber, Gebser, Ianni, Kaminski, Krennwallner, Leone, Maratea, Ricca, Schaub)Standardised ASP rules (normal/disjunctive/aggregate/choice), used at ASP Competition since 2013Current ASP standardhttps://arxiv.org/abs/1911.04326
Lparse format1996+Niemelä / Simons (Helsinki/Aalto)Older ASP intermediate produced by lparse, consumed by smodels — predecessor to gringo’s intermediateLegacyhttps://www.tcs.hut.fi/Software/smodels/
gringo intermediate2007+Potsdam (Gebser, Kaminski, Schaub)Internal grounded intermediate produced by gringo, consumed by Clingo’s solver core (clasp)Active, internal to Clingo pipelinehttps://potassco.org/
OPL1999Pascal Van Hentenryck (ILOG, then IBM)Constraint + LP modelling language; commercial, ships with IBM ILOG CPLEX Optimization StudioActive, IBM commercialhttps://www.ibm.com/products/ilog-cplex-optimization-studio
OR-Tools cp_model.proto2018+GoogleProtobuf serialisation of CP-SAT models; binary .pb or text .pb.txtActive, the CP-SAT wire formathttps://github.com/google/or-tools/blob/stable/ortools/sat/cp_model.proto
PySAT formula objects2017+Ignatiev, Morgado, Marques-SilvaPython-level CNF/WCNF object model with serialisation to DIMACS / WCNF; bridges Python modelling to native C/C++ solversActivehttps://pysathq.github.io/

Tier 3 family table — MIP / LP / mathematical programming

FormatFirst appearedOriginTypeStatus (2026)URL
MPSlate 1960s (IBM MPS/360 → MPSX)IBM (extending the earlier SHARE format)Column-oriented, fixed-column ASCII; 8-character names (because 8 chars = double word on 360); the de facto LP interchange formatActive, every commercial and OSS LP solver still reads ithttps://en.wikipedia.org/wiki/MPS_(format)
CPLEX LP format~1988 (CPLEX 1.0)CPLEX Optimization (Bixby) → IBMRow-oriented, algebraic, human-readable LP/MIP; backslash comments; complementary to MPSActive, supported by Gurobi, CPLEX, HiGHS, SCIP, glpkhttps://www.ibm.com/docs/en/icos/22.1.2?topic=cplex-lp-file-format-algebraic-representation
AMPL .nl~1990Robert Fourer, David Gay, Brian Kernighan (Bell Labs)Low-level postfix-tree representation of nonlinear models; both binary and ASCII variants; the AMPL→solver wire formatActive, dozens of solvers (CBC, CPLEX, IPOPT, KNITRO, MINOS, MOSEK, SNOPT) accept ithttps://en.wikipedia.org/wiki/Nl_(format)
GAMS scalar1976+GAMS Development Corp. (Meeraus, Bisschop)Older commercial modelling language predating AMPL; produces solver-specific scalar outputsActive, commercialhttps://www.gams.com/
OSiL2004COIN-OR Optimization ServicesXML-based optimisation instance format; sibling of XCSP3 in spirit, for MILP/NLPActive but nichehttps://projects.coin-or.org/OS

Tier 3 family table — Theorem-prover input

FormatFirst appearedOriginTypeStatus (2026)URL
TPTP CNF1993+Sutcliffe & Suttner (Miami / TU Munich)Original TPTP form: clause normal form for first-order logicActive, base layer of TPTPhttps://tptp.org/
TPTP FOF~1996+Sutcliffe et al.Full first-order form, untypedActivehttps://tptp.org/UserDocs/TPTPWorldTutorial/LogicFOF.html
TPTP TFF (TF0/TF1)2011 (TF0) / 2014 (TF1)Sutcliffe + theorem-prover communityMonomorphic / rank-1 polymorphic typed first-order with arithmeticActive, primary CASC competition formathttps://link.springer.com/chapter/10.1007/978-3-642-28717-6_32
TPTP THF (TH0/TH1)~2010 (TH0) / 2017 (TH1)Benzmüller, Sutcliffe et al.Monomorphic / rank-1 polymorphic typed higher-order formActivehttps://tptp.org/UserDocs/TPTPWorldTutorial/LogicTHF.html
TPTP TFX2018Sutcliffe + KaliszykExtended TFF with boolean terms, tuples, conditional expressionsActivehttps://ceur-ws.org/Vol-2162/paper-07.pdf

Notable threads

  • DIMACS CNF as the lingua franca that never needed a successor. The 1993 spec from the 2nd DIMACS Implementation Challenge fits on a postcard: one p cnf V C header line, then space-separated literals terminated by 0, comments prefixed c. Thirty-three years later it is still what every SAT solver reads. The format optimises for parser-on-a-napkin, which means any new C/C++/Rust solver can implement input parsing in an afternoon. WCNF, GCNF, iCNF, and QDIMACS all kept the p <variant> header pattern so existing parsers compose. The closest thing to a successor is AIGER (And-Inverter-Graph) for hardware verification problems, but for pure SAT, no replacement has stuck — and SAT Competition 2025 (CaDiCaL-SC2025 winning UNSAT, Kissat-VSA second) was decided on DIMACS instances exactly as in 1993.

  • SMT-LIB 2.6 standardisation: portability across Z3 / CVC5 / Yices / MathSAT / Boolector at the cost of nobody loving the syntax. Before SMT-LIB, every SMT solver had its own input language and benchmarking required hand-translation. The Barrett–Stump–Tinelli initiative (started ~2003, hitting 2.0 in 2010, 2.5 in 2015, 2.6 in 2017, latest revision 2021-05-12) gave the field a portable theory-typed s-expression syntax. The 2.7 draft appeared 2025-02-05 and 3.0 is under active design. The cost: SMT-LIB 2.6 is verbose, parenthesis-heavy, and almost nobody writes it by hand — modellers use Python/Rosette/Lean front-ends and emit SMT-LIB 2 only at the wire boundary. But the wire-boundary win is decisive: a benchmark instance written today runs unchanged on Z3 (Microsoft), CVC5 (Stanford/Iowa/NYU), Yices 2 (SRI), MathSAT (FBK), and Bitwuzla.

  • The MiniZinc → FlatZinc compilation model. This is the cleanest two-language stack in the family. MiniZinc 2.9.7 (2026-04-30) is what humans write — generators, comprehensions, global constraints (alldifferent, circuit, cumulative, bin_packing). The compiler flattens the model to FlatZinc, a much simpler language of typed variable declarations and primitive constraints (int_lin_le, array_int_element, …) — and that is what Gecode, Chuffed, OR-Tools’ CP-SAT, Choco, Picat-SAT, and HiGHS actually consume. The compilation is solver-aware: each backend ships a “solver library” (share/minizinc/gecode, share/minizinc/chuffed) telling MiniZinc which globals it natively supports, so the same .mzn file can run on a SAT-based, CP-based, or LP-based backend with different generated FlatZinc.

  • ASPCore-2 settling the gringo/clingo vs DLV split. For most of the 1990s and 2000s the two ASP camps — Helsinki/Aalto (lparse → smodels) and Calabria (DLV) — had divergent input syntaxes. The ASP Standardization Working Group (Calimeri, Faber, Gebser, Ianni, Kaminski, Krennwallner, Leone, Maratea, Ricca, Schaub) shipped ASPCore-2 as the unified standard, used at ASP Competition since 2013 and formalised in Theory and Practice of Logic Programming / arXiv:1911.04326. Today gringo, Clingo, DLV, WASP, and most ASP teaching toolchains all read ASPCore-2; the format covers normal rules, disjunctive heads, aggregates (#count, #sum, #min, #max), choice rules, weak constraints, and optimisation.

  • DRAT / LRAT / FRAT and the rise of proof-producing SAT. The trust-crisis trigger was the Pythagorean triples / Schur-five-coloring results of 2016 — proofs that produced terabytes of resolution trace, with no human able to spot-check. DRAT (Heule/Hunt/Wetzler 2014) gave SAT a clausal proof format where each line is “add this clause” (preserving satisfiability) or d-prefixed “delete this clause”; DRAT-trim can verify the proof. LRAT (Cruz-Filipe et al., 2017) added per-step resolution hints making verification linear-time and fast enough to mechanise — formally verified LRAT checkers now exist in Coq, Isabelle, Agda, and ACL2. FRAT (Tan/Heule/Hunt, 2021) is an intermediate that lets solvers emit richer hints, cutting elaboration-to-LRAT time by >84% median. Modern SAT competitions in the certified-track essentially require DRAT or LRAT emission — “trust the result” stopped being acceptable around 2017.

  • MPS format archaeology: 80-column punchcards still visible in 2026. MPS originated with IBM MPS/360 in the late 1960s, extending the earlier SHARE format; column names were 8 characters because that was a double-word on System/360. Fixed-column field widths, column-oriented storage, the section markers (NAME, ROWS, COLUMNS, RHS, RANGES, BOUNDS, ENDATA) — every artefact of the punchcard era is still there, and Gurobi / CPLEX / HiGHS / SCIP / glpk in 2026 all parse it. CPLEX LP format (~1988, Bixby) is the row-oriented, algebraic counterpoint: human-readable, easy to generate from a C application, but less standardised — which is why MPS, despite being uglier, is still the de facto interchange format.

  • TPTP as the SMT-LIB equivalent for first-order theorem proving. While SMT-LIB anchors decision-procedure-based reasoning, TPTP (Sutcliffe & Suttner, 1993+) anchors saturation/resolution-based first-order theorem proving. The format hierarchy mirrors SMT-LIB’s logic hierarchy: CNF (clauses), FOF (full first-order, untyped), TFF (typed first-order: TF0 monomorphic, TF1 rank-1 polymorphic, with arithmetic), THF (higher-order: TH0/TH1), and TFX (TFF with booleans, tuples, conditionals, 2018). The format drives the CASC (CADE ATP System Competition) the way DIMACS drives the SAT Competition and SMT-LIB drives SMT-COMP — Vampire, E, iProver, Zipperposition, Leo-III, and the Lean/Coq automation tools all consume it.

  • OR-Tools’ cp_model.proto as the first protobuf-native solver input. Google’s CP-SAT (the dominant constraint-programming solver as of the mid-2020s, winning the MiniZinc Challenge multiple years running) broke from the ASCII-format tradition: its native serialisation is Protocol Buffers, with .pb binary and .pb.txt text variants. This is faster to parse, schema-versioned, and trivially generated from any of CP-SAT’s six SDK languages (C++, Python, Java, .NET, Go, Swift bindings via OR-Tools). It points to a possible future where new solvers ship protobuf-or-flatbuffers schemas instead of bespoke ASCII formats — though the compatibility-with-30-years-of-benchmarks argument keeps DIMACS / SMT-LIB / FlatZinc dominant.

Citations

Graph View