During my placement I have to use SAT/SMT solvers to formalize and solve scheduling problems, but I keep on making mistakes in my assertions so if anyone could help me a little it would be a great help.
So I'm trying to represent a 2 processors system with multiple tasks assigned with different length and arrival times (for that I choose to use arrays such as P1[x] represent the task done by processor 1 at time x or a constant Idle if no task can be processed at that time and T[x][y] represent the part y of the task x)
And to use those in a SMT solver I needed to formalize 5 conditions on my model : Unicity of each part of task, order of each tasks, existence of all parts, order of arrival, and limitation at 1 part of task at a time.
So the 5 assertions are :
Unicity :
$\forall x\exists T((P1[x]=T\implies\lnot\exists y((x\neq y \implies (P1[y]=T\lor P2[y]=T))\lor(x=y\implies P2[y]=T)))\lor(P2[x]=T\implies \lnot\exists y(x\neq y\implies (P2[y]=T\lor P1[y]=T)))$
Existence:
$\forall Task\exists x (P1[x]=Task\lor P2[x]=Task)$
Order:
$\forall x,y,t,a,b (((P1[x]=T[t][a]\lor P2[x]=T[t][a])\land (P1[y]=T[t][b]\lor P2[y]=T[t][b]))\implies (x<y <=> a<b))$
Arrival :
$\forall x ((P1[x]=T \lor P2[x]=T) \implies x<Arrival(T) $
Limitation :
$\forall x,t,a,b (P1[x]=T[t][a]\implies P2[x]\neq T[t][b])$
So I'd like to know if those formula are mathematically correct, and if there is an easiest way to describe them (even if I need to change my arrays for something else) because I don't feel right using such formulas... But I don't find any others by myself...