[fud2] Implment Sat Solver Based Planner

[jku20]

This implements a planner rustsat as an interface for minisat.

To do so, the planner makes the observation that an op which returns multiple states can be broken into a bunch of ops which return one state. The nomenclature I use in the code is to call these dependencies. Precisely, if state s1 can be made using op1, I say all of the inputs to op1 form a dependency of s1. Therefore over all the ops, each state gets a bunch of possible dependencies, different ways to make it, using different ops.

Dependencies are straightforward to encode in boolean logic. Let each op and state be variables. If that variable is true, that state is taken or that op is used. Let s1 be the variable representing a state with possible dependencies s2, s3 using op1 and s1, s4 using op2. This can be encoded as follows: $(s1 \land op1 \Rightarrow s2 \land s3) \land (s1 \land op2 \Rightarrow s1 \land s4)$.

Putting an op as a condition of the implication might feel counter-intuitive, but it is necessary. Using the encoding $(s1 \Rightarrow s2 \land s3 \land op1) \lor (s1 \Rightarrow s1 \land s4 \land op2)$ would allow a solution were ops are taken but never used, for example the following variables being true: $s1, op1, op2, s4$.

To respond to a request with given input states, output states, and required ops. First, each output state is conjoined together and added to the expression. Then for each possible state a file could be in, if that state is not an input (or an output*) and cannot be constructed with any ops, the state's negation is conjoined to the boolean expression, representing that the state can never be constructed. If the state can be constructed, taking the state implies one of the ops is used. This is then conjoined to the boolean expression. To encode the required ops, they are simply conjoined to the final expression.

As an example, say the same ops as above are used. The desired output is s1 and the input is s2, s3 and the required op is op1. The final encoding would be:
$(s1 \land op1 \Rightarrow s2 \land s3) \land (s1 \land op2 \Rightarrow s1 \land s4) \land op1 \land s1 \land \lnot s4 \land (s1 \Rightarrow op1 \land op2)$

*Without this, the encoding breaks in the case an output is also an input but there is a path to get to that output using an op.

[jku20]

It is worth noting, this planner currently cannot choose to take an op more than once. I think this is okay.