dimod.generators.random_2in4sat#

random_2in4sat(variables: int | Sequence[Hashable], num_clauses: int, *, plant_solution: bool = False, seed: None | int | Generator = None) → BinaryQuadraticModel[source]#

Generate a random 2-in-4 satisfiability problem as a binary quadratic model.

2-in-4 satisfiability [1] is an NP-complete problem class that consists in satisfying a number of conjunctive clauses of four literals (variables, or their negations). For valid solutions, two of the literals in each clause should +1 and the other two should be -1.

Each clause contributes -2 to the energy when the clause is satisfied, and at least 0 when unsatisfied. The energy \(H(s)\) for a spin assignment \(s\) is thus lower bounded by \(E_{SAT}=-2\)num_clauses, this lower bound matches the ground state energy in satisfiable instances. The number of violated clauses is at most \((H(s) - E_{SAT})/2\).

Parameters:

  • num_variables – The number of variables in the problem.

  • num_clauses – The number of clauses. Each clause contains three literals.

  • plant_solution – Create literals uniformly subject to the constraint that the all 1 (and all -1) are ground states satisfying all clauses.

  • seed – Passed to numpy.random.default_rng(), which is used to generate the clauses and the variable negations.

Returns:

A binary quadratic model with spin variables.

Note

The clauses are randomly sampled from the space of 4-variable clauses with replacement which can result in collisions. However, collisions are allowed in standard problem definitions, are absent with high probability in interesting cases, and are almost always harmless when they do occur.

Planting of a not all 1 ground state can be achieved with a spin-reversal transform without loss of generality. Planting can significantly modify the hardness of optimization problems. However, for large problems planting of a solution can be achieved (in the SAT phase) without modification of the hardness qualities of the instance class. [2]