Deepwoken Build Solver

A tool for making the mathematically optimal build in Deepwoken

Try the web frontend here:
https://www.buildsolver.app/

The idea

Users should be able to provide the tool with the following:

• A list of talents
• A list of mantras
• A weapon to use
• Ending mantra levels
• Specific desired final stats the build must satisfy
• An optimization objective (i.e. maximize MED at the end, or minimize the post-shrine cost)

And recieve an optimal stat progression order, including where to use the Shrine of Order, where to use the Shrine of Mastery, etc.

Setup

In the readmes of the respective folder.

TODO

• Allow prioritized optimization of multiple values
• Add EXTREMELY detailed analytics
• Optimize general solve speed

Usage

Unless you are developing or contributing to this project, I recommend you to use the python wrapper provided in python/ to play around with the tool. The main.py script gives plenty of usage examples.

Building requirements

The requirement is a fundamental object, representing a stat requirement for anything you could probably want to obtain. In this model, we express a requirement as a comma-separated list of clauses, that have to be simultaneously satisfied in order to acquire whatever that requirement is for. Each clause can contain multiple OR requirements to be satisfied.

For example, the requirement for Perseverance:

30 ftd, 30 wll  
╰────╯ <-- a single clause

For Neuroplasticity:

35 int or 35 cha or 35 wll 
╰────────────────────────╯ <-- still a single clause!

For a more complex requirement like Silentheart:

25r str, (25 agl or 25 cha), (hvy + med + lht = 75)
╰─────╯  ╰────────────────╯  ╰─────────────────────╯
parantheses are optional ^^   ^^^ a sum requirement

An insane, arbitrary example to show what's expressible:

35 cha or (flm + wnd = 50), (lht + med + hvy = 90) or (lht + mtl + str = 75), 90 wll or 30 int

Below are examples of different syntax you can use to build a requirement:

• ftd = 40
• ftd = 40
• FTD=40
• 40 FTD
• 40 Fortitude
• 1 cha OR 2 int
• STr=1 oR 95 cha

Strict or reducible

Some requirements prevent you from using SoM (Shrine of Mastery) if acquired, and some don't. We refer to the blocking ones as strict, and the rest as reducible (the stat is reducible via SoM).

To express a strict requirement, append an 's' to the end of a value:

• 40s ftd
• 25s wnd or 25s ltn

To express a reducible requirement, append an 'r' instead:

• 40r ftd
• 25r wnd or 25r ltn

If unspecified, reducability has defaults depending on the kind of clause it's in.

There's a few rules on reducability to mirror in-game requirements:

• Any single stat clause (i.e. 90 ftd) is strict by default

Most single-stat requirement talents are strict.

• Any stat in an OR clause (i.e. 35 int or 35 cha) is reducible by default

There are no known OR clauses with any strict components, think oaths, the Mind and Body stat, etc

• Strict sum components do not exist, they are all reducible even when specified strict.

Due to the fact we don't need strict sum representations for anything in-game, and complications defining how a strict sum should gate SoM usage, we leave it undefined.

.req files

The requirements for a build can be expressed entirely within a .req file. The instructions on how to solve one with this tool is in python/main.py.

An example for a bladeharper deepspindle build:

# I am a comment
// i am also a comment?!
Free:
40 str
perseverance := 30 wll, 30 ftd
30 int
30 str, 35 ftd
15 ftd, 40 wll

Post:
perseverance => 90 ftd
80 sdw
(lht + med + hvy = 90r or 75r med), (25 agl or 25 str)

Requirements in the Free section can be obtained anywhere in the progression (i.e. talents, mantras), while requirements in the Post section must be obtained after using the shrine of order. Theres a few reasons why one might want specific requirements in Post. Take the case where you want level 5 gale mantras <=> 80r WND must be satisfied. If you satisfy this pre-shrine and then use the shrine to reduce gale, your mantra levels will be reduced accordingly. Thus, mantra level requirements must be fulfilled post-shrine.

You may also give requirements identifiers with the following syntax:

perseverance := 30 wll, 30 ftd
^^^ assigns 30 wll, 30 ftd to the variable 'perseverance'

This is optional, but required if you want to express that a requirement is a prerequisite of another, which is done later in the file:

perseverance => 90 ftd
^^^ perseverance is a requirement for reinforced armor (90 ftd)

Alternatively, you can name both requirements and write a prereq assertion later:

Free:
perseverance := 30 wll, 30 ftd
...

Post:
ra := 90 ftd
...

# It doesn't matter if this assertion is in Post or Free, as long as the identifiers present
# are defined in the right section.
perseverance => ra 

For asserting multiple prereqs:

Free:
perseverance := 30 wll, 30 ftd
battle_tendency := 15 wll, 15 ftd
...

Post:
ra := 90 ftd
...

perseverance, battle_tendency => ra 

If you have a req that doens't have any stat requirement, but requires prereqs, create an empty named requirement:

Free:
scrapsinger := 35 mtl
crystal := 40 ice
surge := 40 ltn

# empty requirement! 
golden_age := ()

scrapsinger, crystal, surge => golden_age

Optional requirements [DRAFT]

An optional requirement is one that is not required to be obtained, but can be obtained as a part of an optimization objective.

Free:
# specify a weight for the optional req, from 1-5.
1; scrapsinger := 35 mtl
crystal := 40 ice
surge := 40 ltn

# empty requirement! 
golden_age := ()

scrapsinger, c

Note: Making any prereq of a required req optional is invalid. To model optional reqs with prereqs, simply make the req itself optional:

p1 := ...
p2 := ...
p3 := ...

1; has_alot_of_prereqs := 42 hvy

p1, p2, p3 => has_alot_of_prereqs

# this works also!
1; p1, p2, p3 => 42 hvy

This recursively marks all prereqs as optional, with their obtainment being directly tied to the optional dependents'. That is, p1, p2, p3 and any of their prereqs are now obtained if and only if has_alot_of_prereqs is obtained.

If you still want to acquire a prereq regardless of whether the dependent is chosen, use a special directive to re-mark a prereq as required:

p1 := ...
# must acquire p2 now!
+ p2 := ...
p3 := ...

1; has_alot_of_prereqs := 42 hvy

p1, p2, p3 => has_alot_of_prereqs

Naturally, if p2 has any prereqs, they will be marked as required again.

Tests

Tests act on the files tests/*.req. A test passes if the solver returns UNSAT[isfiable] for a .req file with 'unsat' in it's name, otherwise it passes if the solver returns SAT and all requirements were able to be acquired at their respective stages in the progression.

Benchmarks

Benchmarks are produced by the bench.py script in the python/ folder. There are also benchmarks in the benchmarks/ folder, which are keyed by the commit they were produced on. Average builds take 300ms to 20 seconds to solve, for particularly difficult builds.

The theory (how the solver is implemented)

The optimization objective is to maximize/minimize an integer parameter based on a set of constraints. To achieve this, we use z3, a popular theorem prover, to solve for the optimal stat configuration.

Definitions

Define the following:

The finite set of all stat names, $S=\set{\text{Str},\text{Agl},\text{Ftd},\ldots}$, and a subset containing only attunement stats, $S_{a} \subset S$.

The following stat mappings from $S\to \mathbb{Z}$:

• Stats to go to first before shrine of order, $Start$
• Stats right before shrine of order, $Pre$
• Stats immediately after using shrine of order, $Post$
• Stats to go after using shrine of order, $Finish_1$
• Two intermediate SoM stat distributions, $Finish_2, \space Finish_3$
• Stats the build ends with, $Finish_4$

We will use $Final$ as an alias for $Finish_4$ when appropriate.

Each of these names model a different stage in a character's progression. A useful way to think about these stages is $Start \to Pre \to Post \to Finish_1 \to Finish_2 \to Finish_3 \to Finish_4$.

The invested totals, for any stat mapping $Stats$:

$$T_{Stats} = \sum Stats(s)$$

The cost:

$$Cost_{Stats} = T_{Stats} - \max(0, |\set{s \in S_a | Stats(s) \gt 0}| - 1)$$

The first point of attunements besides a character's first attunement don't count towards the total cost, in other words, the character's available points to invest don't get consumed.

Subtraction on any two stat distributions $A, B$:

$$C(s) = A(s) - B(s)$$

The boolean $\text{useOrder}$.

The set of constraints $C$.

'Attributes' and 'stats' are used interchangeably.

Trivial constraints

A character's maximum total cost of points is 330.

$$(0 \le Cost_{start} \le 330) \land (0 \le Cost_{pre} \le 330) \land \ldots \in C$$

Stat requirements

Most things have stat requirements, including talents, mantras, and weapons. Talents, oaths etc may require one or more stats, including a disjunction of multiple stats to be fulfilled (e.g. Neuroplasticity requires 35 Mind, which requires 35 CHA OR 35 WIL OR 35 INT), or a sum of multiple stats to be fulfilled. To obtain what the requirement is for, a character must satisfy all of these conditions simultaneously. For example, a stat may require 50 Charsma and 35 Weapon, which would require (50 CHA AND (35 LHT OR 35 MED OR 35 HVY)).

Let

$$\mathcal{D} = \set{\text{and}, \text{or}}$$

$$\mathcal{T} = \set{\text{strict}, \text{red}}$$

The properties strict and red[ucible] refers to it's locking behavior with the Shrine of Mastery, as explained later.

Let $A = \mathcal{P}(S) \times \mathbb{Z} \times \mathcal{T}$. We define an atomic condition as,

$$a = (Q, v, t) \in A \text{ where } Q \subseteq S$$

and for any stat mapping $Stats$, satisfaction as,

$$Stats \models a \iff (\sum_{s \in Q} Stats(s)) \geq v$$

In most cases, $|Q| = 1$. We need the summation for modeling sum requirements, e.g. Bladeharper's (75 MED OR (LHT + MED + HVY = 90))

Then, a clause, consisting of a set of atoms and an aggregator, as,

$$c = (L, d) \quad \text{where } L \subseteq A \text{ and } d \in \mathcal{D}$$

and satisfaction as,

$$Stats \models c \iff \begin{cases} \forall a \in L, \quad Stats \models a & \text{if } d = \text{and} \\ \exists a \in L, \quad Stats \models a & \text{if } d = \text{or} \\ \end{cases} $$

Let $\mathcal{C}$ be the set of clauses. Finally, a requirement is a set of clauses,

$$R = \set{c_1, \ldots, c_n}$$

and satisfaction,

$$Stats \models R \iff \forall c \in R, \space Stats \models c$$

I believe this can model any requirement currently in the game, pls let me know if I'm wrong.

Shrine of Order & Mastery

The Shrine of Order performs is an iterative algorithm that attempts to redistribute stat points equally, amongst the stats the character has invested in. However, a single (non-attunement) stat cannot drop more than 25, so some stats get 'stuck' above the value everything else is. We refer to these stats as fixed stats, the other stats are free. In-game, the remainder points that were not able to be distributed amongst the free stats, due to them needing to end equal, are refunded to the player.

More formally, define an 'equilibrium' stat value $l \in \mathbb{Z}$. A stat $s \in S$ is free if and only if $l = Post_s$. We refer to a stat that is not free as fixed.

Let $Free$ and $Fixed$ be the set of free and fixed stats respectively.

Let $P = \set{s \in S | Pre(s) \gt 0}$ be the set of invested stats.

Define $F$, the stat floor function as

$$ F(Stats, s) = \begin{cases} 0 & \text{if } s \in S_a \\ \text{max}(0, Stats(s) - 25) & \text{else} \\ \end{cases} $$

Then, the shrine finds a value of $l$ such that the following hold:

$$ Post(s) = \begin{cases} 0 & \text{if } s \notin P \\ \text{max}(l, F(Pre, s)) & \text{else} \\ \end{cases} $$

$$\Delta = T_{pre} - T_{post}, \space \Delta < |Free|$$

$$0 \leq T_{post} \leq T_{pre}$$

Then, $Post(s)$ yields the points of stat $s \in S$ directly after using the shrine of order, giving us a method to compute the post-shrine stats for a guessed pre-shrine configuration within z3.

The Shrine of Mastery allows a player to reduce 1 point of a stat at any point in the progression. This can be done for a total of three times per character. This can only be done if the character does not certain requirements that will not be satisfied once that point is deducted. From this point onwards, SoM refers to the Shrine of Mastery, and pre/post-shrine refers to the stages immediately before and after using the shrine of order.

There are some stats in requirements that don't lock the player out of using SoM, including weapons reqs, oath reqs, and mantra level reqs. We refer to these stats within the requirement as reducible, and the blocking stats as strict.

The Wiki states: "Talents that require attribute category investment instead of a specific attribute such as Mind, Body, Element, or Weapon as well as the Attributes Unbound Talents are ignored by Shrine of Mastery, allowing you to reinvest freely." Despite this, we still choose to model OR clauses with strict reqs, and strict SUM reqs for completeness.

Let:

$$u_{pre}, \space u_{f1}, \space u_{f2}, \space u_{f3}\in \mathbb{Z}, \space u_{pre} + u_{f1} + u_{f2} + u_{f3} \leq 3$$

denote the amount of SoM points used in each respective stage, and

$$dec(A, B) = \sum max(0, A_s - B_s)$$

$$inc(A, B) = \sum max(0, B_s - A_s)$$

be the total decrease and increase functions from a stat distribution $A$ to $B$.

Pre-shrine

There are two reasons why we may choose to use SoM that I can think of.

We have a reducible req

In this case, a valid course of action is to meet the req, use SoM to deduct $u_{pre}$ points (possibly changing the post-shrine distribution), then shrining.

There is another course of action where we can leave $u_{pre}$ points out of a strict req, satisfy a reducible req, and then deduct $u_{pre}$ points from the reducible req, finally investing them into the strict req.

We hit power 5 (exactly 90 pts), and using SoM to reduce the points spent may change the post-shrine distribution favorably

This is some insane metamancing shit.

In all cases,

$$inc(Start, Pre) \leq dec(Start, Pre) = u_{pre}$$

$$T_{pre} \leq T_{start}$$

TODO! the constraints on $T$ i think should be on $Cost$.

Post-shrine:

$$\forall i \in \set{1 \ldots 3}$$

$$inc(Finish_i, Finish_{i+1}) \leq dec(Finish_i, Finish_{i+1}) = u_{fi}$$

$$T_{finish_{i+1}} \leq T_{finish_i}$$

As you may know, requirements for talents can be satisfied either pre-shrine or post-shrine, allowing us to acquire talents, use the shrine of order to bring down high stat investments, and invest into other stats. However, weapon requirements cannot be satisfied pre-shrine (unless that timing bug still exists), so we must have the required stats for any weaopns after using the shrine. Additionally, oath requirements must be satisfied post-shrine (as you cannot use the shrine of order while having an oath). The reducibility of each stat in the clauses of requirements is independent of all this.

Let $\text{Req}$ be the set of requirements. We partition $\text{Req}$ into three sets:

$\text{general}$ - Reqs satisfiable pre and post-shrine.

• Mantra obtainment requirements
• Attribute unbound
• Talent card requirements (excluding oaths)

$\text{post}$ - Reqs only satisfiable post-shrine.

• Mantra level requirements
• Weapon requirements (with a slight penalty)
• Oath requirements
• User specified required ending stats

$\text{implicit}$ - Reqs that are not really requirements, but will be satisfied as a byproduct of having a certain stat value. These disappear after shrining the attribute below the requirement.

• Attunement milestones (Adept, Master etc). These talents will be removed from the character if the shrine of order forces their attunement below the requirements, and additionally restricts SoM.

This seems very arbitrary but we need this defined, as the attunement milestone talents gate SoM if they exist, but they disappear after the shrine of order brings down their attunement below the requirements. Attunement milestone talents are automatically added to the character in-game if the attunement goes above the requirement.

We will NEVER have implicit requirements that are above any explicit requirement's value, and so any implicit requirements should not impact the satisfiability of a build.

Multifaceted

Multifaceted is an echo unlocked upgrade that allows you to invest your character's innate points granted to you by its race. For example, if you didn't have multi and had a felinor slot, you would be stuck with 3 starting CHA and 2 starting AGL (this does allow you to go to 103 CHA and 102 AGL however). Once you unlock multi, you will be able to invest those points freely. Once you unlock it, all current slots will have their innate points deducted and returned to you as free stats, while retaining anything that was obtained using those points. For example, going to 100 CHA without multi on a felinor slot, getting a strict OR reducible req (say a talent), then unlocking multi on another slot, thus reducing CHA to 97 and retaining that talent is a valid progression path.

Define $Stage: \text{Req} \to \set{0, 1, \ldots, 5}$ which denotes the stage a requirement is chosen to be acquired at, where

$$\forall R \in (\text{general} \cup \text{post})$$

$$Stage(R) = 0 \iff \text{R is chosen at } Start$$

$$Stage(R) = 1 \iff \text{R is chosen at } Pre$$

$$Stage(R) \geq 2 \iff \text{R is chosen at } Finish_{Stage(R) - 1}$$

We require the solver to decide an acquisition stage, that is, the stage of progression the solver decides to obtain the requirement at, because using a req satisfaction to gate SoM usage is too restrictive. For example, $Start \models R$ can be true, but we may want to defer the obtainment of that requirement for post-shrine. Using $Start \models R$ to gate SoM usage in this case may wrongly restrict us from using SoM pre-shrine, when we don't even have that req pre-shrine.

$Stage$ is undefined for implicit requiremnents beacuse we never choose to obtain them.

Define $\text{multiStage}$, an integer that denotes the stage that we choose to unlock multifaceted immediately after reaching. For example, if $\text{multiStage} = 0$, we unlock multifaceted immediately after reaching $Start$ (since we previously defined stage 0 as $Start$), and the stages $Pre$ and onwards are affected. $\text{multiStage} \in {0, \ldots, 5}$, the image of $Stage$. To represent starting with no race, we inject an 'empty' race into the list of races.

Each race has its own set of innate stats. Define $Innate_r : S \to \mathbb{Z}$, the innate stat mapping for a given race $r$. $r$ is a constant race parameter chosen by the solver.

Define a function that maps from the base stats (stats we currently have invested) to the effective stats (stats that includes invested + innate race points):

$$E(Stats) = \begin{cases} Stats + Innate_r & \text{stageOf}(Stats) \leq \text{multiStage} \\ Stats & \text{else} \end{cases}$$

The effective stat mapping is used for all requirement satisfaction constraints. We now formally define implications on the $Stage$ of acquisition:

$$\forall R \in (\text{general} \cup \text{post})$$

$$Stage(R) = 0 \implies E(Start) \models R$$

$$Stage(R) = 1 \implies E(Pre) \models R$$

$$Stage(R) \geq 2 \implies E(Finish_{Stage(R) - 1}) \models R$$

Then, for any stat mapping $Stats$, we have the following constraints, modeling all base stats in the range of 0-100:

$$\forall s \in S, \space 0 \le Stats(s) \le 100$$

Then, define a variant of $E$ that yields the stats of the stat mapping after multifaceted is unlocked:

$$E_a(Stats) = \begin{cases} Stats + Innate_r & \text{stageOf}(Stats) \lt \text{multiStage} \\ Stats & \text{else} \end{cases}$$

This allows us to retrieve a 'view' of a stat mapping after it was transformed by the multifaceted acquisition, which is needed for some sequential modeling, like the shrine of order (should act on $E_a(Pre)$) and SoM constraints.

We can now properly define constraints on the shrine of order and mastery, while properly modeling multifaceted mechanics.

Constraints

All the constraints listed below are present in $C$.

$Stage$ constraints:

$$\forall R \in (\text{general} \cup \text{post})$$

$$Stage(R) = 0 \implies E(Start) \models R$$

$$Stage(R) = 1 \implies E(Pre) \models R$$

$$Stage(R) \geq 2 \implies E(Finish_{Stage(R) - 1}) \models R$$

Prerequisite requirements These were not mentioned until now because with the introduction of the $Stage$ mapping, the handling of prerequisites is trivial, if they exist.

Define $Preq : \text{Req} \to \mathcal{P}(\text{Req})$, which denotes the set of requirements that is are prerequisites for the input. We assume that all prerequisites must be acquired to acquire the target requirement.

$$\forall R \in \text{Req}, \space \forall p \in Preq(R), \space Stage(p) \leq Stage(R)$$

This is enough to model transitive dependencies.

Shrine of order can only be used after power 5 (90 points invested at any time).

$$Cost_{start} \lt 90 \implies \lnot \text{useOrder}$$

For modeling convenience and efficiency, multifaceted cannot be unlocked at $Stage = 0$. There is no scenario where unlocking multifaceted before pre-shrine SoM teps is beneficial, and any reinvestment of multifaceted-returned points can be modeled by $Start$ reaching the 'peak', then subtracting the multifaceted points after $Pre$.

$$\text{multiStage} \neq 0$$

This 'visiting peak' approach holds as long as we assume $330 - T_{pre} \geq T_{innate_r}$, and I believe this assumption is valid.

Ignoring the shrine $(\lnot \text{useOrder} \implies)$:

$$Start = Pre = Post = Finish_i$$

$$\forall R \in \text{general} \cup \text{post}, \space Stage(R) \geq 2$$

Ignoring the shrine, the model collapses into $Finish_1 \to Finish_2 \to Finish_3 \to Finish_4$

Using the shrine $(\text{useOrder} \implies)$:

$$Counted(s) := \begin{cases} E_a(Pre)(s) & \text{if } s \in P\\ 0 & \text{else} \\ \end{cases} $$

The points from the pre-shrine distribution that are actually counted towards shrine math. Racial points are only counted for shrine math if one or more points are invested into them. If $\text{multiStage} = -1$ or multifaceted search is disabled, $Counted = Pre$.

$$ Post(s) = \begin{cases} \text{max}(l, F(Counted, s)) & \text{if } s \in P \\ E_a(Pre)(s) & \text{else} \\ \end{cases} $$

$$ Post_P(s) := \begin{cases} Post(s) & \text{if } s \in P \\ 0 & \text{else} \\ \end{cases} $$

$$\Delta := T_{Counted} - T_{post_P}, \space \Delta < |Free|$$

$$0 \leq T_{post_P} \leq T_{Counted}$$

$$\forall R \in \text{general}, \space Stage(R) \text{ is defined}$$

$$\forall R \in \text{post}, \space Stage(R) \geq 2$$

Finishing stats post-shrine (before SoM) must be greater or equal to the shrine-distributed stats.

$$\forall s \in S, \space Post(s) \leq E(Finish_1)(s)$$

Note: $Post$ is an internal, purely mechanical stage for calculating the result of the shrine of order. There is no stage between $Pre$ and $Finish_1$, which is why we can enforce the constraint on the effective value of $Finish_1$ instead of the base.

SoM can be used at most 3 times, and points refunded may either be invested again or kept out of the distribution.

$$u_{total}=u_{pre} + u_{f1} + u_{f2} + u_{f3} \leq 3$$

$$inc(Start, Pre) \leq dec(Start, Pre) = u_{pre}$$

$$\forall i \in \set{1 \ldots 3}$$

TODO this is slightly outdated we account for reinvestment in the code

$$inc(Finish_i, Finish_{i+1}) \leq dec(Finish_i, Finish_{i+1}) = u_{fi}$$

$$u_{fi} = 0 \implies \forall s \in S, \space E_a(Finish_i)(s) = E(Finish_{i+1})(s)$$

The last constraint is implied, but making it explicit may help with performance.

SoM cannot create new points, only transfers and decreases.

$$T_{pre} \leq T_{start}$$

$$\forall i \in \set{1 \ldots 3}$$

TODO CHECK THIS PART AGAIN

$$T_{E(finish_{i+1})} \leq T_{E(finish_i)}$$

SoM cannot be used for stats at or under obtained strict requirements.

Define $\text{Used} : \set{d = \text{or} | (L, d) \in \mathcal{C}} \to A$ which denotes the atom selected/used to satisfy an $\text{or}$ clause.

$$\forall R \in \text{general} \cup \text{post}, \space \forall c = (L, d) \in R$$

$$\forall (Q, v, \text{strict}) \in \begin{cases} L & \text{ if } d = \text{and} \\ \set{\text{Used}_c} & \text{ if } d = \text{or} \end{cases}$$

$$\forall s \in Q$$

TODO! this part is slightly outdated (AND WRONG!) bc now each $v$ is sum over $Q$ instead of being a specific stat value $s$. This part must be fixed in the code as well!! This is only incorrect if we choose to model strict sum Atoms, such as LHT + MED + HVY = 90S, otherwise the model is correct as is.

$$Stage(R) = 0 \implies E(Pre)(s) \geq \min(E_a(Start)(s), v)$$

$$1 \geq Stage(R) \geq 0 \implies \forall i \in \set{2, 3, 4}$$

$$E(Finish_{i})(s) \geq \min(E_a(Finish_{i-1})(s), v)$$

$$4 \geq Stage(R) \geq 2 \implies \forall m \in \set{Stage(R),\ldots,4}$$

$$E(Finish_{m})(s) \geq \min(E_a(Finish_{m-1})(s), v)$$

As per the Wiki: You are [now] unable to change the attributes below what shrine of order gave you.

$$\forall s \in S, \space v = Post(s)$$

$$E(Finish_{m})(s) \geq \min(E_a(Finish_{m-1})(s), v)$$

OPTIMIZATION: The last constraint for the last two sections collapses to $Finish_m(s) \geq v$ if we do not search with multifaceted enabled.

Make sure the solver can't reinvest points from SoM into attunements currently at 0, which is both redundant and impossible.

$$\forall s \in S_a$$

$$Start(s) = 0 \implies Pre(s) = 0$$

$$Finish_i(s) = 0 \implies Finish_{i+1} = 0 $$

For implicit requirements

$$\forall R \in \text{implicit}, \space \forall (L, \text{and}) \in R, \space \forall (Q, v, \text{strict}) \in L$$

$$\forall s \in Q$$

$$Start \models R \implies Pre(s) \geq v$$

$$\forall i \in \set{1 \ldots 3}$$

$$Finish_i \models R \implies \forall m \in \set{i+1, \ldots, 4}, \space Finish_m(s) \geq v$$

Note: We only use the base stats for implicit reqs, because implicit reqs are only for attunement milestones as of right now (1/22/2026), and for any attunement stat, $E(Stats)(s) = Stats(s)$.

Optimization implementation

Note the optimization objctive is to minimize $Cost_{final}$. For any $n \in \mathbb{N}$:

$$C \cup (Cost_{final} \le n) \text{ is unsat} \implies \forall m < n, \space C \cup (Cost_{final} \le m) \text { is unsat}$$

$$C \cup (Cost_{final} \le n) \text{ is sat} \implies \forall m > n, \space C \cup (Cost_{final} \le m) \text { is sat} $$

Since the property of satisfiability is monotonic in the case of one optimization objective, a binary search on values of $n$ will suffice. The minimum value of $n$ where $C \cup (Cost_{final} \le n) \text{ is sat}$ yields an optimal stat distribution.

(z3 already supports optimization, but it's painfully slow, and SAT checking is a lot faster.)

Optimizing solving speeds

Below are some optimizations that are done to prune the search space or allow more efficient propagation by z3.

Constraining stats from reducible requirements For builds that have mostly/all reducible requirements (cough all oaths), solving takes a tremendous amount of time, since we allow the solver more freedom in the SoM stages. We do imply that a stat mapping for a stage cannot decrease by more than 3, but very indirectly. So, we require that reducible reqs set explicit lower bound constraints. This is simple, because at any given stage, any stat can decrease by at most $u_{total}$ points.

$$\forall R \in \text{general} \cup \text{post}, \space \forall c = (L, d) \in R$$

$$\forall (Q, v, \text{red}) \in \begin{cases} L & \text{ if } d = \text{and} \\ \set{\text{Used}_c} & \text{ if } d = \text{or} \end{cases}$$

$$\forall s \in Q$$

$$(Stage(R) = 0 \lor Stage(R) = 1) \implies (Pre(s) \geq v - u_{total})$$

$$(Stage(R) = 0 \lor Stage(R) = 1) \implies (\forall i \in \set{2, 3, 4}, \space Finish_{i}(s) \geq \min(Finish_1(s), v) - u_{total})$$

$$4 \geq Stage(R) \geq 2 \implies \forall m \in \set{Stage(R) - 1,\ldots,4}, \space Finish_m(s) \geq v - u_{total}$$

TODO slightly outdated, constraints have been tightened to the individual $u$ per stage over $u_{total}$.

Shrine usage estimation We can estimate when the solver must use the shrine of order, to reduce branching on more complex builds.

Someone remind me to rewrite this I'm too tired but here's the rust code for this part:

if maxes.values().sum::<i64>() > 330 {
    // shrine should be used
    z3_push!(c, use_shrine);
} 

TODO optimizations

• Multifaceted SoM gate $Stage == m =&gt; \ldots$ encoding is suboptimal
• Allow force multifaceted on instead of incremental always