dimod.generators.random_nae3sat#

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

Generate a random not-all-equal 3-satisfiability problem as a binary quadratic model.

Not-all-equal 3-satisfiability (NAE3SAT) is an NP-complete problem class that consists in satisfying a number of conjunctive clauses of three literals (variables, or their negations). For valid solutions, the literals in each clause should be not-all-equal; i.e. any assignment of values except (+1, +1, +1) or (-1, -1, -1) are valid for each clause.

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

NAE3SAT problems have been studied with the D-Wave quantum annealer [1].

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.

Example

Generate a NAE3SAT problem with a given clause-to-variable ratio (rho).

>>> num_variables = 75
>>> rho = 2.1
>>> bqm = dimod.generators.random_nae3sat(num_variables, round(num_variables*rho))

Note

The clauses are randomly sampled from the space of 3-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 solution state can be achieved with a spin-reversal transform without loss of generality. Planting can significantly modify the hardness of optimization problems.