About D-wave hybrid to solve SAT problem
Hello D - wave :
We all know that D-wave has its unique advantages in solving large-scale problems. When we use D-wave to solve SAT problems, we first convert our problems into CNF files and use D-wave hybrid to solve them. However, I find that we can only solve small problems with hundreds of variables. When the number of variables is 1344 and the number of constraints is 5984, I cannot output the solution. I'd like to know what's going on, or which parameters in ocean we can tweak to take advantage of quantum annealing and solve the problem.
Here is a section of my code related to the D-wave solution, all.cnf is the file I am asking to solve (contains 1344 variables, 5984 constraints).
cnf_file_path = "./all.cnf"
strip_file_spaces(cnf_file_path)
with open('./current_file.cnf', 'r') as file_:
csp = dwavebinarycsp.cnf.load_cnf(file_)
#csp = dwavebinarycsp.
print('# Variables', len(csp.variables), '- # Constraints', len(csp), )
bqm = dwavebinarycsp.stitch(csp)
res_set1 = set()
for i in range(5000):
sampler = LeapHybridSampler(profile='0927d')
response = sampler.sample(bqm)
Comments
Hi Kin,
You might want to try using LeapHybridCQMSampler instead. We have seen really good results by using CQM solver to solve SAT problems.
To formulate the problem as a CQM, you can add each clause as a constraint and no objective function.
If you have not used the CQM solver before, following resources might help you get started:
Let us know if you have any further questions.
Please sign in to leave a comment.