Solver domains
7 / 7
measured / mapped
Loading experiment data
Resolving capability…
Contacting the configured Observatory adapter.
Research in progress
Observatory is preparing and verifying real benchmark data. Public numbers will be released only after that verification is complete. Placeholder and test results stay hidden until then.
Unified solver observatory
A single evidence surface for Xolver across satisfiability, optimization, constraint programming, mathematical programming, quantified reasoning, and synthesis.
Every domain follows the same reproducible experiment contract
Logical decision procedures
Satisfiability Modulo Theories
Decision procedures across arithmetic, bit-vectors, arrays, floating point, and combined theories.
Theory-aware optimization
Optimization Modulo Theories
Optimal models, lexicographic and Pareto objectives, and MaxSMT over rich background theories.
Combinatorial search
Constraint Programming
Finite-domain constraints, global propagators, scheduling, routing, and discrete optimization.
Mathematical optimization
Mixed-Integer Linear Programming
Linear relaxations, branch-and-bound, cutting planes, and mixed discrete-continuous models.
Propositional reasoning
Boolean Satisfiability
SAT, weighted and unweighted MaxSAT, pseudo-Boolean optimization, and core extraction.
Quantified reasoning
Quantified Boolean Formulas
Alternating quantifiers, dependency-aware reasoning, expansion, and quantified proof search.
Constructive reasoning
Synthesis and Constrained Horn Clauses
Program synthesis, invariant discovery, Horn-clause solving, and solver-guided repair.
Solved share of the current comparable suite
Recent changes across the portfolio
All nonlinear arithmetic answers replayed without mismatch.
SAT campaign now records DRAT/LRAT availability per track.
Multi-objective experiments appear as a first-class OMT track.
Four cumulative instances moved into the research queue.
Optimality and feasibility tolerances are now part of identity.
The Observatory is organized by reasoning intent, not by one benchmark format
Determine whether formulas and quantified constraints admit a model.
Search for provably better or optimal solutions under symbolic and numeric constraints.
Model finite-domain structure, propagation, scheduling, and discrete search.
Construct programs, invariants, and explanations rather than returning a decision alone.
A compact view of maturity, scale, coverage, and correctness
| Domain | Stage | Tracks | Benchmarks | Solved | Coverage | Quality gate |
|---|---|---|---|---|---|---|
SMTSatisfiability Modulo Theories | Stable | 6SMT-LIB logics | 42,680 | 38,914 | 91.2% | Passed |
OMTOptimization Modulo Theories | Beta | 5objective familys | 15,200 | 13,235 | 87.1% | 1 wrong |
CPConstraint Programming | Preview | 5problem familys | 28,600 | 23,892 | 83.5% | Passed |
MILPMixed-Integer Linear Programming | Preview | 5model classs | 18,750 | 15,183 | 81.0% | 2 wrong |
SAT · MaxSATBoolean Satisfiability | Beta | 4competition tracks | 25,000 | 22,784 | 91.1% | Passed |
QBFQuantified Boolean Formulas | Planned | 4quantifier fragments | 11,700 | 8,049 | 68.8% | 1 wrong |
SyGuS · CHCSynthesis and Constrained Horn Clauses | Planned | 4reasoning tasks | 13,000 | 8,570 | 65.9% | Passed |