--- title: UNISOLVE input formats | SpinForge url: https://spin-forge.com/unisolve/formats description: Defined mathematical, graph and logical input subsets. The latest inventory includes weighted graph resources, source-preserving optional readers and… --- UNISOLVE / INPUT FORMATS # Bring the original model. Defined mathematical, graph and logical input subsets. The latest inventory includes weighted graph resources, source-preserving optional readers and feature-based native routing. Recognition is broader than complete language conformance. Current source G: UNISOLVE 0.16.1, 82 profiles, 65 entry functions, 133 Python exports, 38 CLI operations and nine stdio MCP tools. All profiles were exercised through the installed-package campaign; optional declines and incomplete outcomes remain explicit. [Current evidence ](https://spin-forge.com/unisolve/validation) Find a format or capability Execution path FORMAT / PATH SUPPORTED SCOPE BOUNDARY [Prepare a local command](https://spin-forge.com/unisolve/developers) Twenty editorial frontend groups, including the MiniZinc bridge—not twenty complete languages or seventy-two distinct engines. Unchanged detailed subsets come from the earlier supplied README; the current update expands the scopes stated here. Native ## JSON Validated typed intermediate representation, including symbolic theory and quantifier fields. The supplied typed model must pass validation. Native ## Hybrid JSON Mixed linear objective, graph-cut rewards, hard/soft clauses, linear constraints and supported finite globals. Composition retains the accepted original constraints and objective. Native ## MQLib / weighted graph 1-based weighted edges, signed weights, parallel edges and self loops. A graph-domain override must agree with the parsed model. Native ## DIMACS CNF clauses, empty and unit clauses, strict counts and zero terminators. SAT witnesses and UNSAT refutations have different proof obligations. Native ## WCNF / WDIMACS Legacy top-weight and modern h hard-clause syntax. Hard and soft constraints are kept distinct. Native ## OPB Linear Boolean constraints and objectives, including complemented literals. Boolean linear scope; not an arbitrary integer-program parser. Native + fallback ## MPS Finite MIP/LP and exact rational linear model paths; configured SCIP/VIPR original-model certificates for exact linear MIP. Broader source constructs depend on installed readers. Ordinary numerical status remains distinct from independently checked exact proof. Native ## FlatZinc Supported finite constraint models; matching, flow and automaton CP globals are available within the admitted native inventory. An emitted-model proof does not establish equivalence of a high-level MiniZinc translation. Confirm the actual construct subset before import. Native ## XCSP3 Supported finite CP and scheduling, including variable quantities and exact end equations; native scheduling admits typed optional presences and variable durations/demands. Only the admitted finite constraints, globals and scheduling formulations; not complete XCSP3 or every CP global. Native ## TSPLIB TSP/ATSP inputs, including a matching/branch exact route admitting up to 256 cities by default; sparse directed arcs and signed binary-rational costs are admitted. The 256-city limit is an admission guard, not a solve-time guarantee. Missing arcs are forbidden. Held–Karp retains its 20-city guard. Native ## METIS / SNAP / Matrix Market Supported graph normalization, including weighted METIS resource data and binary multi-resource balance. Current G adds labelled multiway partitioning with per-part quotas and admitted proofs; unrestricted completion and GPU performance remain unestablished. Confirm the selected graph format and resource interpretation. Native ## QDIMACS Preserved quantifier prefix with admitted quantified learning and prefix-preserving composition. Original-game strategy checking is separately budgeted; finite decomposition does not flatten quantifiers. Native + fallback ## SMT-LIB Feature-based native routing for admitted affine, Boolean/integer, UF/array, bit-vector, guarded nonlinear and quantified reasoning, including multivariate Presburger elimination. Full language conformance and arbitrary theory combinations remain unfinished. Optional Z3 is a separate external integration and trust boundary. Native + fallback ## LP / PIP Supported exact rational normalization, dependency-free rational LP and supported polynomial/mixed-integer proof paths, including bounded multivariate spatial covers. General nonpolynomial MINLP and exact irrational multivariate elimination are unsupported. Optional backend status is not an exact proof. Optional reader ## AMPL NL / OSiL Source-preserving optional SCIP reader adapter. Original bytes are retained for installed reader/backend integrations. No general native proof of original-language optimality is claimed. Native ## PGSolver Total parity games using the largest recurring priority convention. Strategy checks use the admitted parity-game convention. Native ## OR-Library set cover Boolean covering MIP. The supported set-cover input, not every OR-Library problem family. Native ## SteinLib STP Undirected nonnegative-cost Steiner tree represented as an integer flow model. The stated undirected, nonnegative-cost scope applies. Native + fallback ## Classical job-shop text Classical job-shop input. Separately, the native scheduling scope includes admitted calendars, typed optional task presences and variable durations/demands. Do not infer that every scheduling construct is expressible through this text format. Check the selected frontend and calendar/language limits. Optional compiler ## MiniZinc compiler bridge Compile a high-level model with its data and includes, retain compiler provenance, and strictly parse the emitted FlatZinc. A real MiniZinc installation is optional. High-level translation is trusted: native optimality on the emitted model is not a proof of high-level compiler equivalence. Native ## GCG set-cover models Supported set-cover solving. GCG decomposition and column-generation integration are not implemented. SEMANTICS & RESOURCES ## A supported input. Not an unlimited promise. Use unisolve formats, unisolve solvers and unisolve doctor in the installed package to inspect the actual admitted input, dependency and proof limits. 01 ### Keep the original question Unsupported semantic fields are rejected or retained for an explicit installed reader/backend; they are not silently removed. 02 ### Respect the compiler boundary The MiniZinc bridge retains original model, data, includes and compiler provenance. Its translation remains trusted. 03 ### Budget the selected path Work, node, byte, size and proof guards have documented scopes. They do not promise a bound on every machine allocation or resident-memory peak. [Review execution and recovery](https://spin-forge.com/unisolve/runtime)