SMT Generation

generate(graph, feasible_configurations, decision_variables, linear_energy_ranges, quadratic_energy_ranges, min_classical_gap, smt_solver_name=None)[source]

Generates the Ising model that induces the given feasible configurations. The code is based on the papers 1 and 2.

  • graph (nx.Graph) – The target graph on which the Ising model is to be built.

  • feasible_configurations (dict) – The set of feasible configurations of the decision variables. The key is a feasible configuration as a tuple of spins, the values are the associated energy.

  • decision_variables (list/tuple) – Which variables in the graph are assigned as decision variables.

  • linear_energy_ranges (dict, optional) – A dict of the form {v: (min, max), …} where min and max are the range of values allowed to v.

  • quadratic_energy_ranges (dict) – A dict of the form {(u, v): (min, max), …} where min and max are the range of values allowed to (u, v).

  • min_classical_gap (float) – The minimum energy gap between the highest feasible state and the lowest infeasible state.

  • smt_solver_name (str/None) – The name of the smt solver. Must be a solver available to pysmt. If None, uses the pysmt default.


A 4-tuple containing:

dict: The linear biases of the Ising problem.

dict: The quadratic biases of the Ising problem.


float: The classical energy gap between ground and the first excited state.

Return type



ImpossiblePenaltyModel – If the penalty model cannot be built. Normally due to a non-zero infeasible gap.


Bian et al., “Discrete optimization using quantum annealing on sparse Ising models”,


Z. Bian, F. Chudak, R. Israel, B. Lackey, W. G. Macready, and A. Roy “Mapping constrained optimization problems to quantum annealing with application to fault diagnosis”