10 · Profiles, budgets and cost

Which parts of the engine run is not a performance setting: it decides what an answer is allowed to claim. A refutation the SAT solver asserted cannot carry a self-contained certificate; a repair drawn from an expansion nobody built cannot claim to be the least disruptive. So the engine's settings come in named profiles, each a combination that supports one kind of claim, chosen per request with profile.

The five profiles

Profile	What it gives you	When to use it
fast	a verdict in about a quarter of a second: a verified SAT witness, or an UNSAT the SAT solver asserts. No certificate and no repair	the default for a question, and every row of a table that should stay green
patch	a repair and a certificate, from the algebraic expansion, with the SAT solver off	a hole fast found, or an UNSAT you need a certificate for
proof	the gating profile: the SAT solver decides, the expansion repairs what it leaves, at full certificate detail. A broken obligation is asked again with the SAT solver off, so its repair and its verdict come from one run	a gate that must produce both a verdict and a repair
enumerate	every situation that breaks the policy, and a proof there is no other	review and diagnosis; slow by design, and not for a gate
forest	the random forest default: the SAT solver decides, at production scale, and its UNSAT is admitted	random forests (chapter 14)

Every key each profile sets, generated from the profiles the service runs:

Key	fast	patch	proof	enumerate	forest
enable_phase0	true	false	true	false	true
oracle_unsat_admissible	true	false	true	false	true
certificate_detail	none	full	full	full	none
enable_phase3	false	false	false	true	true
enable_phase4	false	true	false	true	true
max_roots	1	1	1	0	1
report_phase2_trace	false	false	false	false	false
report_minimal_contexts	false	false	false	false	false
verbose	true	true	true	true	true
wall_budget_seconds	60.0	300.0	900.0	900.0	3600.0
contradiction_budget_seconds	60.0	120.0	180.0	180.0	60.0
Searches for a repair	no	yes	yes	yes	no

And why each is set that way, in the service's words:

Profile	Why
fast	the decide-only shape, which answers in about a quarter of a second; a minute is generous and there is no repair search to fund
patch	the repair run: the search is the point, so most of the allowance is the search's
proof	the gating profile: Phase 0 decides, Phase 2 patches what it leaves, and no closure -- seconds rather than minutes, which is the difference between a gate and a nightly
enumerate	the closure endgame and an unbounded root count: every context that breaks the policy and a proof there is no other. Slow by design, and for diagnostics rather than for a gate
forest	a deployed forest is retrained rather than patched, so there is no repair to search for and the whole allowance is the property's own

The two-run protocol

The cheapest way to an actionable answer is two runs, and the second only when it is needed:

1. Decide with fast. About a quarter of a second. UNSAT and no certificate wanted: stop, and the record says oracle_dependent: true, so the weaker claim is on the record rather than implied.
2. SAT, or STALL, or UNSAT with a certificate wanted: ask again with patch. The repair needs the algebraic expansion, which fast does not build, and so does a certificate anyone can replay.

proof does the two runs for you, and pays for the second only where the first found a hole. A property table does the same row by row: it decides each row with the SAT solver, and solves a row a second time only where its answer owes what the SAT solver cannot build, a repair or a certificate the row asks for (chapter 11).

Changing one key: config

A profile is a baseline, not a lock. config overrides single keys on top of it, in that order, so a request that changes a budget leaves the phases the profile chose standing. A key the service does not know is refused with the list it does accept; a value outside a key's bounds is clamped to the bound, or refused where the bound stands for something else. The job's run.config_effective is what ran, and run.clamped_by says what a bound changed.

The keys, generated from the service's registry:

Key	Type	Meaning	Values
enable_phase0	bool	run the bounded CDCL oracle
oracle_unsat_admissible	bool	allow an oracle-asserted refutation to end the run; no certificate resting on one is self-contained
enable_phase1_5	bool	run the sexed-reproduction expansion
enable_phase2	bool	run the evolutionary expansion loop
enable_phase3	bool	run the border-basis closure endgame
enable_phase4	bool	run condensation and exhaustive search over what the closure left undecided
max_roots	int	upper bound on the roots the closure returns; 0 is unbounded	≥ 0
max_quotient_dimension	int	absolute ceiling on the quotient basis; 0 uses the scaled guard	≥ 0
min_quotient_dimension	int	floor under the scaled quotient guard; 0 is no floor	≥ 0
max_quotient_dimension_scalar	double	fraction of the ambient degree-2 space the quotient basis may reach before the closure gives up	≥ 0.0
max_pivot_row_width	int	terms a stored pivot row of the phantom sweep's elimination may hold. Rows wider than this are dropped whole rather than stored, which bounds the phase's resident cost at the price of a larger quotient to filter; 0 removes the bound and lets the elimination fill freely	≥ 0
phase3_admission	string	border-admission strategy for the closure	Greedy, Stratified
wall_budget_seconds	double	wall-clock budget for the solve; stops at a loop boundary with the cascade intact, so a stopped run is a valid partial closure rather than a corrupt one. 0 is no deadline, and the service does not grant one: a budget below the floor is raised to it	≥ 1.0; ≤ 21600.0
sds_target_threshold	int	disruption score at or below which the seat-belt search accepts a candidate and stops scanning	≥ 0
contradiction_budget_seconds	double	separate wall-clock budget for the seat-belt search, which runs after the solve. 0 is no deadline rather than no search, and the service does not grant one: use enable_contradiction_search to turn the search off	≥ 1.0; ≤ 3600.0
enable_contradiction_search	bool	follow a non-UNSAT verdict with the seat-belt search. Off means no candidate is proposed at all, rather than a worse one
verbose	bool	console verbosity of the run
enable_operation_tracking	bool	record the provenance of every rank-increasing insertion, which a full certificate cannot be reconstructed without
report_phase2_trace	bool	publish the per-generation rank trace in the payload
report_minimal_contexts	bool	reserved for minimal-context reduction, which does not exist
certificate_detail	string	how much of the refutation to write down, and therefore how much bookkeeping the solve pays for	full, core, none

certificate_detail decides how much of the refutation is written down: full writes the whole derivation; core first shrinks the system to the smallest set of your equations that still refutes, and certifies that, which keeps a certificate small on a large system; none writes no certificate.

The budgets

A run has two clocks:

• wall_budget_seconds bounds the whole solve. A run it stops ends as STALL with verdict.budget_exhausted: true and the cause budget-expired, and another run with a larger budget is worth having. Your key's wall_budget_ceiling_seconds caps it: a request above the ceiling is reduced to it, not refused, and run.clamped_by says so. Above 900 seconds needs the long_solve grant.
• contradiction_budget_seconds bounds the search for a repair. A search it stops returns the best repair found so far, still proved to close the hole; only least disruptive is withdrawn, and corrective_action.search_truncated is true.

Zero means unbounded in both, which your key's ceiling still caps. A budget exhausted is never a silent failure: a stopped run says it was stopped, and what it returns is still sound.

Counting every way through: enumerate

A witness answers is there a hole. Under the enumerate profile, with enumerate set on the request, the engine answers how many, and is that all of them: it closes the system completely, counts the situations that break the policy, and proves the count is complete, because the count is a dimension it computed rather than the point a search stopped finding things. The answer carries the count and whether it is complete; a count the engine had to cut short reads as a lower bound. The strongest form is zero, proved: no situation breaks the policy, and there is none left to look for.

This is a review instrument. No gating profile runs it, and no verdict needs it: a verdict and a signed certificate are reached without it. It is slow by design, and enumerate is refused alongside fast or patch, neither of which runs the closure it needs.

What frat_proof costs

A FRAT proof of a Phase 0 refutation (chapter 7) costs nothing unless you ask for it. Asked for, it is a second solve of a refutation the SAT solver already reached, with proof logging on. On the reference refutations a run went from a median of 30 ms to 44 ms, the CNF was 0.2 to 5.5 KB, the FRAT log 1.3 to 49 KB, and frat-rs checked it in about 30 ms. That is not a bound: on some systems the proof is far harder than the solve, and a proof the run's budget stops is not written, which leaves the certificate the oracle's, exactly as without the option. The stored files count against your key's max_proof_bytes, and a proof that would exceed it is discarded, never the verdict (chapter 16).

What a solve costs

Each finished job writes one usage record, and the solve seconds it used count against your key's monthly_solve_seconds (chapter 16):

How the job ended	Counted
succeeded, whatever the verdict, SAT and STALL included	yes
failed for a cause of yours: a policy that does not compile, a digest that does not match, a budget you set	yes
failed for a cause of ours: a lost worker, an internal error	no
failed for a cause nothing has classified	no
cancelled	yes, for the seconds actually used
refused before anything ran	nothing is recorded

A stall is counted because it used the compute and still returns a repair: it is a delivered answer. Quota is checked when a job is submitted and not again while it runs, so a run that started under quota finishes.

On the free plan, a job runs Phase 0 alone, which is the fast profile; a job that asks for more, a patch or proof profile or a later phase, runs it fully up to the plan's monthly number of full solves (chapter 40).

The limits

• What a profile does not run, its answer cannot claim: fast builds no certificate and no repair, and its UNSAT is the SAT solver's assertion.
• A budget-stopped run is a sound partial answer, and says so; a larger budget may give a stronger one.
• An enumeration's count is complete only where the answer says it is.
• The FRAT figures above are measurements on reference refutations, not a bound on yours.