About D-wave hybrid to solve SAT problem

h m

September 13, 2024 03:12

Hello D - wave :

I am working on solving a SAT (Satisfiability) problem using D-Wave's hybrid solvers, but I have encountered an issue related to constraint satisfaction. Specifically, when attempting to build the Binary Quadratic Model (BQM) for my constraints, I receive the following error:

dwavebinarycsp.exceptions.ImpossibleBQM: No penalty model can be built for constraint Constraint.from_configurations(frozenset({(0, 0, 0, 1, 1, 1, 1, 1), (0, 0, 1, 0, 1, 1, 1, 0), (1, 0, 0, 1, 0, 1, 1, 1), (0, 0, 0, 1, 0, 0, 0, 1), (1, 1, 0, 0, 0, 0, 0, 1), (1, 1, 0, 0, 1, 1, 1, 1), (1, 1, 0, 0, 0, 0, 1, 0), (1, 1, 1, 0, 1, 1, 1, 0), (1, 1, 1, 1, 0, 1, 1, 0), (1, 1, 1, 0, 1, 0, 0, 1), (1, 1, 1, 0, 1, 0, 1, 0), (0, 1, 1, 1, 0, 0, 1, 1), (1, 1, 0, 0, 0, 1, 0, 1), (0, 0, 0, 1, 0, 1, 0, 0), (1, 1, 1, 1, 1, 1, 0, 0), (1, 1, 1, 0, 1, 1, 0, 1), (0, 1, 1, 0, 1, 1, 0, 1), (0, 0, 1, 1, 0, 1, 0, 1), (1, 0, 0, 1, 1, 1, 0, 1), (1, 1, 0, 1, 1, 0, 0, 0), (0, 1, 0, 0, 1, 0, 1, 1), (0, 0, 0, 1, 0, 1, 1, 1), (1, 0, 1, 0, 1, 1, 1, 0), (1, 1, 1, 1, 1, 1, 1, 1), (1, 0, 1, 1, 1, 1, 1, 0), (1, 1, 0, 1, 0, 0, 1, 0), (0, 0, 1, 1, 1, 1, 0, 0), (0, 1, 1, 0, 0, 0, 1, 1), (0, 1, 1, 1, 1, 1, 0, 0), (0, 1, 0, 1, 1, 1, 0, 0), (1, 0, 0, 0, 0, 1, 1, 0), (1, 1, 0, 0, 1, 0, 1, 1), (0, 1, 0, 1, 0, 0, 1, 0), (1, 0, 0, 0, 0, 0, 0, 1), (0, 1, 1, 1, 1, 0, 1, 1), (1, 0, 1, 1, 1, 1, 0, 1), (0, 0, 1, 1, 1, 1, 1, 1), (1, 0, 1, 1, 0, 0, 1, 0), (0, 1, 0, 0, 1, 1, 0, 0), (1, 0, 0, 1, 0, 0, 0, 0), (1, 0, 1, 0, 0, 1, 0, 1), (1, 1, 0, 1, 0, 0, 0, 1), (1, 0, 1, 0, 0, 1, 1, 0), (1, 0, 0, 0, 0, 1, 0, 1), (0, 1, 0, 1, 0, 0, 0, 1), (1, 1, 0, 1, 1, 1, 0, 0), (0, 1, 1, 1, 0, 1, 0, 0), (0, 0, 1, 0, 0, 0, 0, 1), (1, 0, 0, 0, 1, 0, 0, 0), (1, 0, 1, 1, 0, 0, 0, 1), (0, 1, 0, 0, 0, 0, 1, 0), (1, 1, 0, 1, 1, 0, 1, 0), (1, 0, 0, 0, 1, 0, 1, 1), (1, 0, 1, 1, 1, 0, 1, 0), (0, 1, 0, 1, 1, 0, 0, 0), (0, 0, 0, 0, 1, 0, 1, 1), (0, 0, 1, 1, 1, 0, 1, 0), (0, 0, 0, 0, 0, 0, 1, 0), (1, 1, 0, 1, 0, 1, 0, 0), (0, 0, 0, 1, 0, 0, 1, 0), (0, 1, 1, 1, 1, 1, 1, 0), (0, 1, 1, 0, 0, 1, 0, 1), (0, 1, 0, 0, 0, 0, 0, 1), (1, 0, 1, 1, 0, 1, 1, 0), (0, 0, 0, 1, 1, 0, 1, 1), (0, 0, 1, 0, 0, 1, 1, 1), (0, 0, 0, 0, 0, 1, 0, 1), (1, 0, 0, 1, 1, 0, 1, 0), (0, 0, 0, 0, 0, 1, 1, 0), (1, 0, 1, 0, 0, 0, 0, 1), (1, 1, 0, 1, 1, 1, 1, 1), (1, 1, 1, 1, 0, 0, 0, 1), (1, 1, 1, 1, 0, 0, 1, 0), (0, 1, 1, 0, 1, 0, 0, 1), (1, 0, 0, 1, 1, 1, 1, 0), (1, 0, 1, 1, 0, 1, 0, 1), (1, 1, 1, 1, 0, 1, 0, 1), (0, 0, 0, 0, 1, 1, 0, 0), (1, 0, 0, 1, 1, 0, 0, 1), (1, 1, 1, 0, 0, 0, 1, 0), (1, 1, 1, 1, 1, 0, 0, 0), (0, 0, 1, 1, 0, 0, 1, 1), (1, 0, 1, 0, 1, 0, 1, 0), (1, 1, 1, 0, 0, 1, 0, 1), (1, 1, 1, 1, 1, 0, 1, 1), (0, 1, 0, 0, 0, 1, 0, 0), (1, 1, 1, 0, 0, 1, 1, 0), (1, 0, 0, 1, 0, 1, 0, 1), (0, 0, 1, 0, 1, 1, 0, 1), (1, 0, 0, 0, 1, 1, 0, 1), (1, 0, 0, 1, 0, 1, 1, 0), (1, 1, 0, 0, 1, 1, 1, 0), (0, 1, 0, 1, 0, 1, 0, 1), (1, 0, 0, 0, 0, 0, 1, 0), (1, 0, 1, 0, 1, 0, 0, 1), (0, 0, 1, 0, 1, 0, 0, 0), (1, 1, 0, 0, 0, 1, 0, 0), (1, 1, 0, 0, 1, 1, 0, 1), (0, 1, 1, 0, 1, 1, 0, 0), (0, 0, 1, 1, 0, 1, 0, 0), (1, 0, 1, 0, 0, 0, 1, 1), (1, 1, 1, 0, 1, 1, 0, 0), (0, 0, 1, 0, 0, 0, 1, 0), (0, 1, 1, 1, 0, 0, 0, 1), (0, 1, 0, 0, 1, 0, 1, 0), (1, 1, 1, 1, 1, 1, 1, 0), (0, 0, 1, 0, 1, 1, 1, 1), (0, 1, 0, 1, 1, 1, 1, 1), (1, 1, 0, 0, 0, 0, 1, 1), (0, 1, 1, 0, 0, 0, 1, 0), (1, 1, 0, 0, 1, 0, 1, 0), (1, 0, 0, 1, 0, 0, 1, 1), (0, 0, 0, 1, 0, 1, 0, 1), (0, 1, 1, 0, 0, 1, 1, 0), (1, 0, 1, 0, 1, 1, 0, 0), (1, 1, 0, 0, 0, 1, 1, 1), (1, 1, 1, 1, 1, 1, 0, 1), (1, 0, 1, 1, 1, 1, 0, 0), (0, 1, 1, 0, 1, 1, 1, 1), (0, 0, 1, 1, 0, 1, 1, 1), (1, 1, 0, 1, 0, 0, 0, 0), (0, 1, 1, 0, 0, 0, 0, 1), (0, 1, 1, 1, 0, 1, 1, 1), (1, 0, 0, 0, 0, 1, 0, 0), (1, 1, 0, 0, 1, 0, 0, 1), (0, 0, 0, 0, 0, 0, 0, 1), (0, 0, 0, 1, 1, 0, 0, 0), (0, 0, 1, 1, 0, 0, 0, 0), (0, 1, 0, 1, 0, 0, 0, 0), (0, 0, 1, 0, 1, 0, 1, 0), (0, 1, 1, 0, 1, 0, 1, 0), (1, 0, 1, 0, 1, 1, 1, 1), (1, 0, 1, 1, 0, 0, 0, 0), (0, 1, 0, 1, 1, 0, 1, 1), (1, 0, 0, 0, 1, 0, 1, 0), (1, 1, 0, 1, 0, 1, 1, 1), (0, 0, 0, 0, 1, 0, 1, 0), (0, 1, 0, 0, 1, 1, 0, 1), (1, 0, 0, 0, 1, 1, 1, 0), (0, 1, 0, 0, 1, 1, 1, 0), (0, 1, 0, 0, 0, 0, 0, 0), (0, 1, 0, 1, 0, 1, 1, 0), (0, 0, 0, 1, 1, 0, 1, 0), (1, 0, 1, 1, 1, 0, 0, 0), (0, 0, 1, 0, 0, 1, 1, 0), (0, 0, 0, 0, 0, 1, 0, 0), (1, 0, 1, 0, 0, 0, 0, 0), (1, 1, 0, 1, 1, 1, 1, 0), (0, 0, 0, 0, 1, 0, 0, 1), (0, 0, 1, 1, 1, 0, 0, 0), (0, 0, 0, 1, 1, 1, 0, 1), (0, 1, 1, 1, 1, 0, 0, 0), (0, 0, 0, 1, 1, 1, 1, 0), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 1, 0, 0, 0, 0), (1, 1, 0, 0, 0, 0, 0, 0), (1, 1, 1, 1, 0, 1, 0, 0), (1, 0, 1, 1, 0, 1, 0, 0), (1, 0, 1, 1, 1, 0, 1, 1), (1, 1, 1, 0, 1, 0, 0, 0), (0, 0, 1, 0, 0, 1, 0, 1), (0, 1, 1, 1, 0, 0, 1, 0), (1, 0, 0, 1, 1, 0, 0, 0), (0, 0, 1, 1, 1, 0, 1, 1), (1, 1, 1, 0, 0, 0, 0, 1), (0, 1, 0, 0, 0, 1, 1, 1), (0, 0, 0, 1, 0, 0, 1, 1), (0, 1, 1, 1, 1, 0, 0, 1), (0, 1, 1, 1, 1, 1, 1, 1), (1, 0, 0, 1, 1, 1, 0, 0), (1, 1, 1, 0, 0, 1, 0, 0), (1, 1, 1, 1, 1, 0, 1, 0), (0, 0, 1, 0, 1, 1, 0, 0), (0, 1, 0, 0, 1, 0, 0, 1), (0, 0, 0, 0, 0, 1, 1, 1), (1, 1, 1, 1, 0, 0, 1, 1), (0, 0, 0, 1, 0, 1, 1, 0), (1, 0, 1, 0, 1, 0, 0, 0), (1, 1, 1, 0, 1, 1, 1, 1), (1, 0, 0, 1, 1, 1, 1, 1), (1, 1, 1, 1, 0, 1, 1, 1), (1, 1, 1, 0, 1, 0, 1, 1), (1, 0, 1, 0, 0, 0, 1, 0), (1, 0, 0, 0, 0, 0, 0, 0), (0, 1, 1, 1, 1, 0, 1, 0), (0, 0, 1, 1, 1, 1, 1, 0), (1, 0, 1, 0, 0, 1, 0, 0), (1, 1, 1, 0, 0, 1, 1, 1), (0, 1, 0, 1, 1, 1, 1, 0), (1, 1, 0, 1, 1, 0, 0, 1), (1, 0, 0, 0, 0, 0, 1, 1), (0, 0, 1, 0, 0, 0, 0, 0), (1, 0, 1, 1, 1, 1, 1, 1), (1, 1, 0, 1, 0, 0, 1, 1), (0, 0, 1, 1, 1, 1, 0, 1), (0, 0, 1, 0, 1, 0, 0, 1), (0, 1, 1, 1, 1, 1, 0, 1), (1, 0, 0, 1, 0, 0, 1, 0), (1, 1, 0, 0, 0, 1, 1, 0), (0, 1, 0, 1, 1, 1, 0, 1), (1, 0, 0, 0, 0, 1, 1, 1), (0, 1, 1, 0, 1, 1, 1, 0), (0, 0, 1, 1, 0, 1, 1, 0), (0, 1, 0, 1, 0, 0, 1, 1), (0, 1, 1, 0, 0, 0, 0, 0), (0, 1, 1, 1, 0, 1, 1, 0), (0, 0, 1, 0, 0, 0, 1, 1), (1, 1, 0, 0, 1, 0, 0, 0), (1, 0, 1, 1, 0, 0, 1, 1), (1, 0, 0, 1, 0, 0, 0, 1), (0, 1, 1, 0, 0, 1, 0, 0), (1, 0, 1, 0, 0, 1, 1, 1), (1, 1, 0, 1, 1, 1, 0, 1), (0, 1, 1, 1, 0, 1, 0, 1), (1, 1, 1, 1, 0, 0, 0, 0), (0, 1, 0, 1, 1, 0, 1, 0), (1, 0, 0, 0, 1, 0, 0, 1), (1, 1, 0, 1, 0, 1, 1, 0), (0, 1, 1, 0, 0, 1, 1, 1), (0, 1, 0, 0, 0, 0, 1, 1), (0, 1, 1, 0, 1, 0, 0, 0), (1, 0, 1, 0, 1, 1, 0, 1), (1, 1, 0, 1, 1, 0, 1, 1), (0, 1, 0, 1, 1, 0, 0, 1), (0, 0, 0, 1, 1, 0, 0, 1), (0, 0, 1, 1, 0, 0, 0, 1), (0, 0, 0, 0, 0, 0, 1, 1), (0, 0, 1, 1, 0, 0, 1, 0), (0, 0, 1, 0, 1, 0, 1, 1), (1, 1, 0, 1, 0, 1, 0, 1), (0, 1, 1, 0, 1, 0, 1, 1), (1, 0, 1, 1, 0, 1, 1, 1), (0, 0, 0, 0, 1, 0, 0, 0), (0, 0, 0, 1, 1, 1, 0, 0), (1, 0, 0, 1, 0, 1, 0, 0), (1, 0, 0, 0, 1, 1, 0, 0), (0, 0, 0, 0, 1, 1, 1, 0), (1, 0, 0, 1, 1, 0, 1, 1), (0, 1, 0, 1, 0, 1, 0, 0), (0, 0, 1, 0, 0, 1, 0, 0), (1, 1, 1, 0, 0, 0, 0, 0), (0, 1, 0, 0, 0, 1, 1, 0), (1, 0, 0, 0, 1, 1, 1, 1), (1, 1, 0, 0, 1, 1, 0, 0), (0, 0, 0, 0, 1, 1, 0, 1), (0, 1, 0, 0, 1, 1, 1, 1), (0, 1, 0, 1, 0, 1, 1, 1), (1, 1, 1, 0, 0, 0, 1, 1), (1, 1, 1, 1, 1, 0, 0, 1), (1, 0, 1, 1, 1, 0, 0, 1), (0, 1, 0, 0, 1, 0, 0, 0), (0, 1, 1, 1, 0, 0, 0, 0), (1, 0, 1, 0, 1, 0, 1, 1), (0, 0, 1, 1, 1, 0, 0, 1), (0, 1, 0, 0, 0, 1, 0, 1)}), (1, 2, 3, 4, 5, 6, 7, 8), Vartype.BINARY, name='Constraint')

Here is a section of my code related to the D-wave solution,Problem-Round2-Active2.cnf is the file I am asking to solve (contains 1344 variables, 5984 constraints).

with open('.\cnf\Problem-Round2-Active2.cnf', 'r') as file_:
  csp = dwavebinarycsp.cnf.load_cnf(file_)
  print('# Variables', len(csp.variables), '- # Constraints', len(csp), )
  bqm = dwavebinarycsp.stitch(csp)#
  for i in range(3):
    sampler = LeapHybridBQMSampler()##
    response = sampler.sample(bqm)      ##

    for sample, energy in response.data(['sample', 'energy']):
        is_satisfiable = csp.check(sample)
        if not is_satisfiable: continue
        print_samples(sample, energy, is_satisfiable)

Comments

1 comment

David J (Report)
September 24, 2024 16:16

Hello,

Thank you for reaching out to us with your inquiry.

This error message indicates that at least one of your constraints cannot be translated into a penalty model.

This is probably because by default the stitch function only builds penalty models of up to 8 variables.

Increasing the maximum number of variables (controlled by max_graph_size keyword argument to stitch) may help.

Please let us know if you have any questions.

0

Comment actions Permalink

Please sign in to leave a comment.

About D-wave hybrid to solve SAT problem

Comments

Didn't find what you were looking for?