dwavesystems / dwavebinarycsp

Map constraint satisfaction problems with binary variables to binary quadratic models.
https://docs.ocean.dwavesys.com/projects/binarycsp/en/latest
Apache License 2.0
21 stars 28 forks source link

Clarification about use of configurations within constraints #107

Open roveri-marco opened 3 years ago

roveri-marco commented 3 years ago

Description This is not a bug, but a request of clarification.

We are currently working on a possible extension of the package that changes the internal representation of the Constraint to leverage on And Inverter Graphs (AIG) to leverage on the possibility to easily check equality among constraints and to compose constraints in an efficient manner to build a Constraint Satisfaction Problem (CSP). While doing this, we noticed that the stitch used to build a binary quadratic model (BQM) from binary constraints strongly relies on Constraint internally storing the models (truth assignments) of the constraint itself. Since the objective of this stitcher seems to be the check for satisfiability (SAT) of the CSP we do not understand the reason for storing the models of the constraints. Indeed, for the AIG representation one has to extract the models of the formula itself, and this might be as costly as solving the SAT instance.

Can you explain the reason for this choice? Is there a way to avoid this and still build the BQM from the CSP?

Any advice would be helpful.

Additional Context This is part of a collaboration between the group I belong to and D-WAVE team.

cc: @CatherineCMcGeoch @roberto.sebastiani@unitn.it @roveri-marco

arcondello commented 3 years ago

Hi @roveri-marco,

It is true that the current design on penaltymodel encodes the constraint verbosely as a truth table. This is because of the way that penaltymodel constructs the constraints.

For the current implementation there is no way to avoid it, but I would be interested in discussing how it might be redesigned.

roveri-marco commented 3 years ago

Hi @arcondello,

Thanks for the comment. I'll check more in details how the construction in the penaltymodel operates, then we may discuss how to re-design it.