code: import org.sat4j.specs.TimeoutException;
  
  import java.util.*;
  
  public class BacktrackingSolver {
  
  	private APTA apta;
  	private int size;
  	private long startTime;
  	private long timeout;
  	private boolean findAllMode;
  	private Set<Automaton> answer;
  
  	public BacktrackingSolver(APTA apta, int size, long timeout, boolean findAllMode) {
  		this.apta = apta;
  		this.size = size;
  		this.startTime = System.currentTimeMillis();
  		this.timeout = timeout;
  		this.findAllMode = findAllMode;
  	}
  
  	public boolean problemIsBacktrackinging() throws TimeoutException {
  		List<Transition> frontier = frontierInit();
  		Automaton automaton = new Automaton(size);
  		answer = backtracking(automaton, frontier);
  		return !answer.isEmpty();
  	}
  
  	public Set<Automaton> getAnswer() {
  		return answer;
  	}
  
  	private Set<Automaton> backtracking(Automaton automaton, List<Transition> frontier) throws TimeoutException {
  		Set<Automaton> automatons = new HashSet<>();
  		if ((System.currentTimeMillis() - startTime) / 1000. > timeout) {
  			throw new TimeoutException();
  			//return automatons;
  		}
  		Transition tr = frontier.get(0);
  		for (int destination = 0; destination < size; destination++) {
  			if (destination > 1 && automaton.getState(destination - 1).getParents().isEmpty()) {
  				break;
  			}
  			Automaton newAutomaton = new Automaton(automaton);
  			newAutomaton.getState(tr.stateFromInDFA).addChild(tr.label, newAutomaton.getState(destination));
  			if (newAutomaton.getState(destination).getStatus() == Node.Status.COMMON) {
  				newAutomaton.getState(destination).setStatus(tr.status);
  			} else {
  				if (newAutomaton.getState(destination).isAcceptable() && tr.status == Node.Status.REJECTABLE) {
  					continue;
  				}
  				if (newAutomaton.getState(destination).isRejectable() && tr.status == Node.Status.ACCEPTABLE) {
  					continue;
  				}
  			}
  
  			List<Transition> newFrontier = findNewFrontier(frontier, newAutomaton);
  			if (newFrontier != null) {
  				if (newFrontier.isEmpty()) {
  					automatons.addAll(makeComplete(newAutomaton));
  					if (!findAllMode) {
  						return automatons;
  					}
  				} else {
  					Set<Automaton> newAutomatons = backtracking(newAutomaton, newFrontier);
  					if (!newAutomatons.isEmpty()) {
  						if (!findAllMode) {
  							return newAutomatons;
  						}
  						automatons.addAll(newAutomatons);
  					}
  				}
  			}
  		}
  		return automatons;
  	}
  
  	private Set<Automaton> makeComplete(Automaton automaton) {
  		Set<Automaton> ans = new HashSet<>();
  		Automaton newAutomaton = new Automaton(automaton);
  		boolean complete = true;
  		for (Node node : newAutomaton.getStates()) {
  			for (String label : apta.getAlphabet()) {
  				if (node.getChild(label) == null) {
  					complete = false;
  //					for (int i = 0; i < newAutomaton.size(); i++) {
  //						node.addChild(label, newAutomaton.getState(i));q
  //						ans.addAll(makeComplete(newAutomaton));
  //					}
  					node.addChild(label, node);
  					ans.add(newAutomaton);
  				}
  			}
  		}
  		if (complete) {
  			ans.add(newAutomaton);
  		}
  		return ans;
  	}
  
  	private List<Transition> frontierInit() {
  		List<Transition> frontier = new ArrayList<>();
  		Node root = apta.getRoot();
  		String label;
  		Node child;
  		for (Map.Entry<String, Node> childEntry : root.getChildren().entrySet()) {
  			label = childEntry.getKey();
  			child = childEntry.getValue();
  			frontier.add(new Transition(root.getNumber(), child.getNumber(), label, 0, child.getStatus()));
  		}
  		return frontier;
  	}
  
  	private List<Transition> findNewFrontier(List<Transition> frontier, Automaton automaton) {
  		List<Transition> newFrontier = new ArrayList<>();
  		List<Transition> newFrontierPart;
  		Node fromDFA;
  		Node toDFA;
  		Node toAPTA;
  		for (Transition tr : frontier) {
  			fromDFA = automaton.getState(tr.stateFromInDFA);
  			toDFA = fromDFA.getChild(tr.label);
  			toAPTA = apta.getNode(tr.to);
  			if (toDFA != null) {
  				if (toDFA.getStatus() == Node.Status.COMMON) {
  					toDFA.setStatus(toAPTA.getStatus());
  				} else {
  					if (toDFA.isAcceptable() && toAPTA.isRejectable()) {
  						return null;
  					}
  					if (toDFA.isRejectable() && toAPTA.isAcceptable()) {
  						return null;
  					}
  				}
  				newFrontierPart = findNewFrontierDFS(toAPTA, toDFA);
  				if (newFrontierPart == null) {
  					return null;
  				}
  				newFrontier.addAll(newFrontierPart);
  			} else {
  				newFrontier.add(tr);
  			}
  		}
  		return newFrontier;
  	}
  
  	private List<Transition> findNewFrontierDFS(Node APTANode, Node DFANode) {
  		List<Transition> frontierPart = new ArrayList<>();
  		String label;
  		Node APTAto;
  		Node DFAto;
  		for (Map.Entry<String, Node> APTANodeEntry : APTANode.getChildren().entrySet()) {
  			label = APTANodeEntry.getKey();
  			APTAto = APTANodeEntry.getValue();
  			DFAto = DFANode.getChild(label);
  			if (DFAto == null) {
  				frontierPart.add(new Transition(APTANode.getNumber(), APTAto.getNumber(), label, DFANode.getNumber(), APTAto.getStatus()));
  				continue;
  			}
  			if (DFAto.getStatus() == Node.Status.COMMON) {
  				DFAto.setStatus(APTAto.getStatus());
  			} else {
  				if (DFAto.isAcceptable() && APTAto.isRejectable()) {
  					return null;
  				}
  				if (DFAto.isRejectable() && APTAto.isAcceptable()) {
  					return null;
  				}
  			}
  			List<Transition> recFrontier = findNewFrontierDFS(APTAto, DFAto);
  			if (recFrontier == null) {
  				return null;
  			}
  			frontierPart.addAll(recFrontier);
  		}
  		return frontierPart;
  	}
  
  	private class Transition {
  		int from;
  		int to;
  		String label;
  		int stateFromInDFA;
  		Node.Status status;
  
  		Transition(int from, int to, String label, int stateFromInDFA, Node.Status status) {
  			this.from = from;
  			this.to = to;
  			this.label = label;
  			this.stateFromInDFA = stateFromInDFA;
  			this.status = status;
  		}
  	}
  }
  