constraint-construction-search
Skill4 starsChanged 20 days agoMITView on GitHub
Encode and verify finite construction or optimization searches with CryptoMiniSat, Z3, OR-Tools CP-SAT or Gurobi, including witness extraction, model audits, and calibrated UNSAT or optimality claims.
In this repository34 other files it gives its agents.
- AGENTS.mdAGENTS.md
- accepted-proof-exact-retuneSkill
- beachhead-ratchetSkill
- circuit-edit-integration-safetySkill
- computer-algebra-oraclesSkill
- cross-model-review-gateSkill
- deepseek-pressure-testSkill
- ecdsafail-fastevalSkill
- ecdsafail-lowq-playbookSkill
- ecdsafail-oracle-loopSkill
- ecdsafail-pareto-ratchetSkill
- ecdsafail-scratch-dietSkill
- elicit-researchSkill
- exact-search-engineeringSkill
- fast-lean-proof-loopSkill
- hard-problem-contractSkill
- invariant-chartSkill
- jev-second-perspectiveSkill
- lean-arklib-proofsSkill
- lean-finite-certificate-splittingSkill
- mission-commandSkill
- nasqret-playbookSkill
- pip-disciplineSkill
- portable-source-assertionsSkill
- proximity-prize-campaignSkill
- proximity-prize-frontier-archaeologySkill
- research-loopSkill
- route-compare-probe-disciplineSkill
- rust-archive-build-bindingSkill
- send-to-claude-fableSkill
- shot-autopsySkill
- squares-in-squares-campaignSkill
- verify-paired-native-measurementsSkill
- verify-research-transferSkill
The file
We split this skill into the rules it gives an agent
11 rules. About 0 are common, 11 are distinctive, and 0 are very specific to this project.
≈0
Common · estimate
Many files like this have a rule of this kind.
≈11
Distinctive · estimate
This author's own choices. Worth a look.
0
Very specific
Tied to their project's names, files or tools. Probably skip.
- Common
- Distinctive
- Very specific
- Distinctive: line 12
Read references/solver-routing.md when choosing between Boolean, SMT, CP-SAT, and MIP formulations.
- Distinctive: line 14
Use CryptoMiniSat for Boolean structure with substantial XOR or parity constraints.
- Distinctive: line 15
Use Z3 for bit-vectors, bounded integers, arrays, symbolic relations, or mixed logical structure.
- Distinctive: line 16
Use OR-Tools CP-SAT for bounded-integer combinatorial models with global or scheduling-style constraints.
- Distinctive: line 17
Use Gurobi for linear or mixed-integer formulations when a licensed installation is available and numerical tolerances are controlled.
- Distinctive: line 23
Test the encoding on hand-built satisfiable and unsatisfiable fixtures, including boundary cases.
- Distinctive: line 26
Treat feasibility, infeasibility, bounded objective, and proved optimum as different outcomes.
- Distinctive: line 31
Stop if the independent verifier reconstructs the solver's encoding instead of checking the original object.
- Distinctive: line 32
Stop if a real-valued tolerance, big-M constant, overflow, or implicit coercion can change feasibility.
- Distinctive: line 33
Stop if symmetry breaking has no proof that every equivalence class retains a representative.
- Distinctive: line 34
Stop before using licensed software, remote services, or paid compute without the required authority.
≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.
Files
Constraint construction search
Translate a finite mathematical construction problem into constraints, solve it, and verify the result outside the solver. The encoding is a proof obligation, not clerical glue.
Choose the formulation
Read references/solver-routing.md when choosing between Boolean, SMT, CP-SAT, and MIP formulations.
- Use CryptoMiniSat for Boolean structure with substantial XOR or parity constraints.
- Use Z3 for bit-vectors, bounded integers, arrays, symbolic relations, or mixed logical structure.
- Use OR-Tools CP-SAT for bounded-integer combinatorial models with global or scheduling-style constraints.
- Use Gurobi for linear or mixed-integer formulations when a licensed installation is available and numerical tolerances are controlled.
Encoding contract
- Define variables, domains, symmetry breaking, constraints, objective, and the mathematical map between models and objects.
- Bound every integer and bit-vector operation. State overflow, wraparound, and signedness semantics.
- Test the encoding on hand-built satisfiable and unsatisfiable fixtures, including boundary cases.
- Emit a witness in a solver-neutral format and verify the original mathematical predicate with separate code.
- Freeze model text or generated-model hash, solver version, parameters, seed, time limit, termination status, and logs.
- Treat feasibility, infeasibility, bounded objective, and proved optimum as different outcomes.
- Apply the certification rules in references/certification.md before reporting UNSAT or optimality.
Stop conditions
- Stop if the independent verifier reconstructs the solver's encoding instead of checking the original object.
- Stop if a real-valued tolerance, big-M constant, overflow, or implicit coercion can change feasibility.
- Stop if symmetry breaking has no proof that every equivalence class retains a representative.
- Stop before using licensed software, remote services, or paid compute without the required authority.
Does it work?
Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.
No reviews yet
People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.
- It worked
- Partly
- It didn't
Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.
Your trail
Files you open will collect here, so you can find them again.
Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.
Now do this for your own.
Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.