# Evolutionary System Design with Answer Set Programming
## 4 Encoding the System Synthesis Problem with ASP Modulo Difference Constraints
### General Problem Encoding  
Listing 2 shows the succinct binding encoding that consists of one choice rule assigning exactly one resource to each task on which it can be mapped. Atoms over predicate bind/2 describe the binding \(b\). That is, bind(\(t,r\)) represents that \(b(t)=r\) for task \(t\) and resource \(r\). Bindings can only be chosen among possible mappings and are therefore valid. For instance, facts bind(t1,r1), bind(t2,r3), bind(t3,r3), and bind(t4,r1) capture the binding of the parent implementation in Figure 2.  
In Listing 3, we find the routing encoding. The routing \(r\) is captured via atoms over predicate route/3. In more detail, for every atom \(\texttt{route}((t,t^{\prime}),u,u^{\prime})\), we have \((u,u^{\prime})\in r((t,t^{\prime}))\) for dependency \((t,t^{\prime})\) and link \((u,u^{\prime})\). Choice rules in Lines 3 and 4 allow every resource in the network at most one outgoing route and at most one ingoing route per communication, respectively. As a result, every communication now has possibly disconnected paths or cyclic routes; however, we ensure that there is no branching. That is, at this point, routes are possibly disconnected or are cycles. Lines 6 to 10 enforce that for each communication, routes are connected and start and end at the correct resources. First, we require that routes are connected by recursively deriving resources that are visited via routes connected to the resource with the sending task. Then, we state that no route may end at a resource that is not visited, i.e., not connected to the sender of the communication. Second, we select the resource with the receiving task and require this resource to be visited and disallow routes originating from there. This expresses that the communication arrives at the target location, and we stop once this is achieved. ```
1 task(t1).task(t2).task(t3).task(t4). 2 send(t1,t2).send(t1,t3).send(t2,t4).send(t3,t4). 4 link(r1,r5).link(r5,r1).link(r2,r6).link(r6,r2). 5 link(r3,r7).link(r7,r3).link(r4,r8).link(r8,r4). 6 link(r5,r6).link(r6,r5).link(r5,r7).link(r7,r5). 7 link(r6,r8).link(r8,r6).link(r7,r8).link(r8,r7). 9 cost(r1,3).cost(r2,1). 10 cost(r3,5).cost(r4,2). 11 cost(r5,1).cost(r6,1). 12 cost(r7,1).cost(r8,1). 14 static_energy(r1,5).static_energy(r2,3). 15 static_energy(r3,5).static_energy(r4,2). 16 static_energy(r5,1).static_energy(r6,1). 17 static_energy(r7,1).static_energy(r8,1). 19 mapping(r1,t1).mapping(r1,t4). 20 mapping(r2,t2).mapping(r3,t2).mapping(r3,t3). 22 mapping(r4,t1).mapping(r4,t4). 24 execution(r1,t1,2).execution(r1,t4,1). 25 execution(r2,t2,2).execution(r3,t3,3). 26 execution(r4,t1,3).execution(r4,t4,1). 27 execution(r4,t1,5).dynamic_energy(r1,t4,4). 29 dynamic_energy(r2,t2,3). 31 dynamic_energy(r3,t2,4).dynamic_energy(r3,t3,6). 32 dynamic_energy(r4,t1,3).dynamic_energy(r4,t4,1). 34 routing_delay(1). 35 routing_energy(1). 36 period(20). ```  
Listing 2 Binding encoding. ```
1{bind(T,R):mapping(R,T)}1:-task(T). ```  
Listing 3 Routing encoding. ```
1 resource(R;R'):-link(R,R'). 3{route((T,T'),R,R'):link(R,R')}1:-resource(R),send(T,T'). 4{route((T,T'),R,R'):link(R,R')}1:-resource(R'),send(T,T'). 5 visit((T,T'),R):-send(T,T'),bind(T,R). 6 visit(C,R'):-visit(C,R),route(C,R,R'). 7:-route(C,,R),notvisit(C,R). 8:-send(T,T'),bind(T',R),notvisit((T,T'),R). 9:-send(T,T'),bind(T',R),route((T,T'),R,_). ```  
**Listing 3**Routing encoding. Because we may only choose our routing among links, Condition 1 is trivially satisfied. Condition 2 is met as we may not start a route from the target resource of a communication, and if that is the same as the source resource, we have no route. Finally, Condition 3 is satisfied, firstly because routing may only take place over visited resources, and the only resource that is visited without condition is the resource the sending task is bound to;secondly, the route ends at the receiving task's resource because it has to be visited, but no further routing from that point is allowed. Therefore, routings produced by this encoding are valid.