# Answer Set Programming for Regular Inference
## 4 Experimental Results
### Compared Algorithms  
As already mentioned, our algorithm was compared with a SAT-based algorithm and several exact parallel algorithms. To make the paper self-contained let us briefly describe these algorithms. The SAT-based algorithm defines three types of binary variables, \(x_{uw},y_{apq}\), and \(z_{q}\), for \(w\in\text{Pref}(S)\), \(a\in\Sigma\), \(p,q\in Q\). Variable \(x_{uw}=1\)_iff_ state \(q\) is reachable by prefix \(w\), otherwise \(x_{uw}=0\). Variable \(y_{apq}=1\)_iff_ there exists a transition from state \(p\) to state \(q\) with symbol \(a\), otherwise \(y_{apq}=0\). Finally, \(z_{q}=1\)_iff_ state \(q\) is final, and \(z_{q}=0\) otherwise. The constraints involving these variables are as follows:  
1. All examples have to be accepted, while none of the counter-examples should be, which is described by \[\forall_{w\in S_{+}-\{\varepsilon\}}\sum_{q\in Q}x_{uw}z_{q}\geq 1,\] (25) \[\forall_{w\in S_{-}-\{\varepsilon\}}\sum_{q\in Q}x_{uw}z_{q}=0.\] (26)
2. All prefixes \(w=a\), \(w\in\text{Pref}(S),a\in\Sigma\), result from the transitions outgoing from state \(q_{0}\) \[\forall_{w=a}x_{uw}-y_{aqq}=0.\] (27)
3. For all states \(q\in Q\) reachable by prefixes \(w=va\), \(v,w\in\text{Pref}(S),a\in\Sigma\), there has to be some state \(r\) reachable by prefix \(v\), and there has to be an outgoing transition from \(r\) to \(q\) with symbol \(a\). By symmetry, if there exists a path for prefix \(v\) ending in some state \(r\) and there exists a transition from \(r\) to \(q\) with symbol \(a\) then there exists a path to state \(q\) with prefix \(w=va\). These conditions are expressed as \[\forall_{w=va}-x_{uw}+\sum_{r\in Q}x_{vr}y_{anq}\geq 0,\] (28) \[\forall_{q,r\in Q}x_{uw}-x_{vr}y_{anq}\geq 0.\] (29)  
Additionally, it holds that \(z_{q_{0}}=1\), when \(\varepsilon\in S_{+}\), \(z_{q_{0}}=0\), when \(\varepsilon\in S_{-}\), and \(z_{q_{0}}\) is not predefined when \(\varepsilon\
otin(S_{+}\cup S_{-})\). The solution to the presented problem formulation is sought by a SAT solver. Figure 2: Example solutions found by the ASP solver for problems a2 words33, a4 words28, a6 words31, and a8 words37. (**a**) Problem a2 words33; (**b**) Problem a4 words28; (**c**) Problem a6 words31; (**d**) Problem a8 words37. **Example 2**. : _Let us consider Example 1 again. In the SAT-based formulation we have the following variables \(x_{aq_{0}}\), \(x_{aq_{1}}\), \(\ldots\), \(x_{abcq_{1}}\), \(y_{aq_{0}q_{0}}\), \(y_{aq_{0}q_{1}}\), \(\ldots\), \(y_{cq_{1}q_{1}}\), \(z_{q_{0}}\), and \(z_{q_{1}}\). Constraints (25)-(29) remain unchanged. A set of assignments satisfying the constraints at hand is as follows: \(x_{aq_{1}}=1\), \(x_{abq_{1}}=1\), \(x_{cq_{0}}=1\), \(x_{abcq_{0}}=1\), \(y_{abq_{1}q_{1}}=1\), \(y_{cq_{0}q_{0}}=1\), \(y_{cq_{1}q_{0}}=1\), \(z_{q_{0}}=1\). All remaining variables are zeros. The resulting NFA is shown in Figure 3. Note that even though the set of transitions in Figure 3 is smaller than in Figure 1 both solutions are valid._  
Identification of a \(k\)-state NFA by means of the exact algorithms RA-PS1, RA-PS2, OA-PS1, and OA-PS2 is based on the SAT formulation given before. Assuming \(k\) is fixed we only need to determine the set of final states \(F\) and the transition function \(\delta\). Let us recall that a set of final states is _feasible iff_ the following conditions are satisfied: (i) \(F\
eq\emptyset\), (ii) \(q_{0}\in F\), if \(\epsilon\in S_{+}\), (iii) \(q_{0}\
otin F\), if \(\epsilon\in S_{-}\). Clearly, an NFA without final states cannot accept any word, and if the empty word \(\epsilon\) is in \(S_{+}\) (resp. \(S_{-}\)) the initial state \(q_{0}\) has to be final (resp. not final). Since every feasible set \(F\) may lead to an NFA consistent with the sample \(S\) (as the NFAs need not be unique), we distribute the different sets \(F\) among processes and try to identify the \(\delta\) function by means of a backtracking algorithm. While searching for the values of \(y_{aq}\) variables, we apply different search orders.