CN118504486B

CN118504486B - Method for adapting constraint solver, electronic equipment and storage medium

Info

Publication number: CN118504486B
Application number: CN202410981947.9A
Authority: CN
Inventors: 倪恩志; 石光辉; 陈颖
Original assignee: Chengdu Rongjian Software Technology Co ltd; Shanghai Hejian Industrial Software Group Co Ltd
Current assignee: Chengdu Rongjian Software Technology Co ltd; Shanghai Hejian Industrial Software Group Co Ltd
Priority date: 2024-07-22
Filing date: 2024-07-22
Publication date: 2024-09-27
Anticipated expiration: 2044-07-22
Also published as: CN118504486A

Abstract

The invention relates to the field of chip verification, in particular to a method, electronic equipment and a storage medium for adapting constraint solvers, which are used for converting constraint expressions to be adapted into a tree structure through presetting constraint solvers of different types and operation types of the adaptation, adapting the obtained operation types to the preset constraint solvers of different types in the process of traversing the tree structure, replacing the maximum subtree of the adaptation with a node of an intermediate variable, and then continuing traversing the adaptation, so that the constraint expressions are finally disassembled into sub-constraints of a plurality of adaptation different constraint solvers, wherein the sub-constraint obtained by each constraint solver is the operation type good for the current constraint solver, and the solving efficiency of the constraint solver and the accuracy of a solving result are improved.

Description

Method for adapting constraint solver, electronic equipment and storage medium

Technical Field

The present invention relates to the field of chip verification, and in particular, to a method for adapting a constraint solver, an electronic device, and a storage medium.

Background

In the field of chip verification, constraint satisfaction problems are often encountered, particularly in various scenarios that ensure functional correctness and performance metrics of a design conform to predefined specifications, such as boolean functional relationships or other logical relationships between logic gates, combinational logic circuits, and sequential logic circuits that need to be satisfied in logic function verification, or constraints designed to ensure minimum pitch or avoid shorts in place and route stages, by checking whether delay constraints on all signal paths are satisfied in sequential constraints. And design constraint satisfaction problems in low power consumption verification, formal verification, or random constraints. Many problems in the field of chip verification can be converted into constraint problems, so that a general constraint solver is adopted for solving.

Common solvers applied to constraint problem solving are SAT (Boolean satisfiability problem) solvers, SMT (Satisfiability modulo theories) solvers, CSP (Constraint satisfaction problem) solvers, and BDD (Binary decision diagram) -based solvers, each of which has differences in solving the problem. Wherein the SAT solver is adept at solving bit operations; SMT solvers are adept at solving combined problems, such as arithmetic, boolean logic, array, etc. combined constraint problems; CSP solvers are adept at arithmetic operations, relational operations, collective relational operations, etc.; BDD solvers are adept at dealing with the representation and optimization problems of boolean functions.

At present, when constraint problems are processed, corresponding constraint problems are generally classified into different operation categories in advance according to operation types, then a proper target solver is matched according to the operation categories, and the target solver is used for solving. When each constraint expression in a complex constraint problem comprises different operation types, classifying according to a preset priority rule, classifying the expressions into corresponding categories, and solving through a corresponding target solver. However, when an operation type which is not good for the target solver exists in the constraint expression, the solving efficiency of the target solver is low, and the solving result is inaccurate. Therefore, a method for improving the computational efficiency and accuracy of constraint solvers is needed.

Disclosure of Invention

Aiming at the technical problems, the invention adopts the following technical scheme: a method of adapting a constraint solver, the method comprising the steps of:

S100, acquiring N types of constraint solver sequences CS to be adapted and the operation types of the N types of constraint solver sequences CS to be adapted; wherein cs= { CS ₁,CS₂,…,CS_i,…,CS_N},CS_i is an i-th type constraint solver in CS, and the value range of i is 1 to N.

S200, obtaining a constraint expression exp of the constraint solver to be adapted.

S300, constructing a tree structure tree of the constraint expression according to exp.

S400, traversing the tree to obtain an operation type, and obtaining a constraint condition P= { P ₁,P₂,…,P_i,…,P_N},P_i adapting to each type of constraint solver as a constraint sub-condition adapting to CS _i; p _i=(V,VM_i,VMC(i),CC_i, CF), V is the original variable set of all variables in exp, VM _i is the current intermediate variable set generated by adapting CS _i, VMC (i) is the other intermediate variable set of all constraint solvers except CS _i in CS, CC _i is the new sub-constraint set generated by CS _i, and CF is the remaining constraint set that cannot be matched by the N-type constraint solvers; the generating step of the j-th current intermediate variable VM _ij and the new child constraint CC _ij thereof in P _i comprises the following steps:

S410, acquiring the tree' -with the last updated tree structure.

S420, traversing upwards from the leaf node of the tree', acquiring an adapted maximum subtree subtree _i according to the operation type of the traversed adapted CS _i, and obtaining a j-th sub-expression subexp _ij of the CS _i according to subtree _i.

S430, the j-th current intermediate variable VM _ij of CS _i is created.

S440, replacing subtree _i in the tree 'with a node bound with the VM _ij to obtain an updated tree structure tree'.

S450, generating the new child constraint CC _ij of CS _i from VMs _ij and subexp _ij.

The present invention also provides a non-transitory computer readable storage medium having stored therein at least one instruction or at least one program loaded and executed by a processor to implement the above-described method.

Furthermore, the invention also provides an electronic device comprising a processor and the non-transitory computer readable storage medium.

The invention has at least the following beneficial effects:

The invention provides a method, electronic equipment and storage medium for adapting constraint solvers, which are used for presetting constraint solvers of different types and adaptive operation types thereof, adapting the operation types of sub-expressions of constraint expressions to different constraint solvers, disassembling the constraint expressions into a plurality of sub-constraints of the different constraint solvers, wherein the sub-constraint obtained by each constraint solver is the good operation type of the current constraint solver, and improving the solving efficiency of the constraint solver and the accuracy of solving results.

Drawings

In order to more clearly illustrate the technical solutions of the embodiments of the present invention, the drawings required for the description of the embodiments will be briefly described below, and it is apparent that the drawings in the following description are only some embodiments of the present invention, and other drawings may be obtained according to these drawings without inventive effort for a person skilled in the art.

FIG. 1 is a flow chart of a method for adapting a constraint solver according to a first embodiment of the present invention;

FIG. 2 is a flow chart of a comparison of the traversing tree structure according to the first embodiment of the present invention;

Fig. 3 is a flowchart of a method for adapting a constraint solver according to a second embodiment of the present invention.

Detailed Description

The following description of the embodiments of the present invention will be made clearly and completely with reference to the accompanying drawings, in which it is apparent that the embodiments described are only some embodiments of the present invention, but not all embodiments. All other embodiments, which can be made by those skilled in the art based on the embodiments of the invention without making any inventive effort, are intended to be within the scope of the invention.

Example 1

Referring to fig. 1, a flow chart of a method of adapting a constraint solver is shown, the method comprising the steps of:

Optionally, the constraint solver is one of a SAT (Boolean satisfiability problem) solver, a SMT (Satisfiability modulo theories) solver, a CSP (Constraint satisfaction problem) solver, or a BDD (Binary decision diagram) -based solver. Other types of solvers of the prior art are within the scope of the present invention.

Wherein the types of constraint solvers are different in CS.

Wherein the adapted operation type refers to the operation type good for the constraint solver.

Optionally, the SAT solver is adapted to a bit operation, and the non-adapted operation is selected from the group consisting of an arithmetic operation, a relational operation and an arithmetic operation. The CSP solver is adapted to arithmetic operations, relational operations and collective relational operations, and the non-adapted operation type is bit operation. The operation types which are adapted by the SAT solver and the CSP solver are logic operations. In the prior art, other constraint solvers and the adaptive operation types thereof also fall within the protection scope of the invention.

The constraint problems include variables, constants, and constraint expressions, among others. Wherein the variables are signed or unsigned bit vectors having a fixed bit width.

Wherein the constraint expression includes an operand and an operator, the operand being a constant or a variable.

Optionally, the operator is one or more of a logical operator, a bit operator, an arithmetic operator, a relational operator, an if-then-else operator, a collective relational operator. Other operators included in the expressions in the prior art are also within the scope of the present invention.

As one example, the constraint problem is: x is a random variable of an 8-bit vector, and the constraint expression is: x >0& & x <11.

It should be noted that S300 converts the text form expression exp into the structured form expression tree, which is more beneficial to computer processing.

Wherein each node in the tree is an operand or an operator, and the edges between the nodes are relationships between the nodes.

In the prior art, the method for constructing the tree structure according to the expression falls into the protection scope of the invention.

S400, traversing the tree to obtain an operation type, and obtaining a constraint condition P= { P ₁,P₂,…,P_i,…,P_N},P_i adapting to each type of constraint solver as a constraint sub-condition adapting to CS _i; p _i=(V,VM_i,VMC(i),CC_i, CF), V is the original variable set of all variables in exp, VM _i is the current intermediate variable set generated by adapting CS _i, VMC (i) is the other intermediate variable set of all constraint solvers except CS _i in CS, CC _i is the new sub-constraint set generated by CS _i, and CF is the remaining constraint set that cannot be matched by all N-type constraint solvers.

And matching the operation type of the sub-expression corresponding to the maximum subtree obtained by traversing the tree to a constraint solver which is good at processing the current operation type.

Wherein P _i may be null. When traversing the tree, if the operation type of the adaptation CS _i does not exist in the tree, P _i is null.

The original variable set V of all the sub constraint conditions in P is the same, and all variables in exp are all variables. After traversing the tree, V is obtained.

Wherein each intermediate variable in VM _i is created when the current constraint solver is adapted. Each intermediate variable in VM _i has a corresponding new child constraint in CC _i, and the number of elements in VM _i is equal to the number of elements in CC _i. The new child constraint in VM _i is defined as the mapping of the child expressions in each current intermediate variable and its alternate exp.

Wherein, when the subtree in which VM _rp is located in VMC (i) is replaced by VM _ij in VM _i, VM _rp includes VM _rp in CC _ij for adapting to the p-th current intermediate variable VM _rp generated by class r constraint solver CS _r. By analogy, all intermediate variables produced appear in all adapted sub-expressions, and therefore all variables and intermediate variables are included in constraint P _i of adaptation CS _i: v, VM _i, VMC (i). Similarly, all variables and intermediate variables are included in constraint sub-conditions that are adapted to other constraint solvers.

Each remaining constraint in the remaining constraint set CF is a constraint corresponding to an operation type that cannot be adapted after the N types of constraint solvers are respectively adapted. The remaining constraint set for all sub-constraints in P is the same.

Further, the adaptation step of the j-th current intermediate variable VM _ij and the new-child constraint CC _ij in P _i includes:

S410, obtaining the tree' of the tree structure updated in the last adapting process.

During the traversal, each adaptation is performed on the basis of the last updated tree structure.

Wherein, subtree _i the step of obtaining includes:

s421, traversing upwards from the leaf node along the path to the root node, and continuing traversing upwards when the operation type of the traversed node is adapted to CS _i; when the operation type to which the traversed operator node belongs does not adapt to the CS _i, the operation node is rolled back to the adapting CS _i of the previous traversal, and the traversal is continued on the other branch after the operation node is rolled back. The judging method of the operation type of the node comprises the following steps: when traversing to the operator node, determining the operation type according to the operator node.

S422, after traversing all potential paths, finishing the traversal, and obtaining subtree _i.

After traversing the entire tree, the largest subtrees of the multiple adaptation CS _i can be obtained.

In the prior art, other methods of obtaining subtree _i fall within the scope of the present invention.

S430, the j-th current intermediate variable VM _ij of CS _i is created.

Wherein the node bound to VM _ij is a leaf node in the tree ". Nodes in the tree "include variables, operators, and intermediate variables.

Optionally, VM _ij and CC _ij satisfy: CC _ij:=VM_ij==subexp_ij. Where "=" is a definition symbol, i.e., defining the constraint on CC _ij as "VM _ij==subexp_ij","VM_ij==subexp_ij" means subexp _ij by VM _ij. Other methods of defining constraints according to VM _ij and subexp _ij are within the scope of the invention.

As one example, when the sub-expression represented by VM _ij is "a| (b & c)", CC _ij satisfies: CC _ij:=VM_ij = a| (b & c).

As a preferred embodiment, S400 further includes:

s470, acquiring a residual constraint set CF, wherein the step of acquiring the h residual constraint CF _ih comprises the following steps:

S471, when traversing upwards from the leaf node of the tree', obtaining the target operation type of the traversed node, and when the target operation type is not matched with the N-type constraint solver, obtaining the h-th discomfort sub tree Usubtree _ih; and according to Usubtree _ih, the h-th discomfort gamete expression Usubexp _ih is obtained. The judging method of the target operation type of the node comprises the following steps: when traversing to the operator node, determining the target operation type according to the operator node.

S472, creating an h intermediate variable VF _h.

And S473, generating the h residual constraint CF _ih of the CF according to the VFs _h and Usubexp _ih.

In the prior art, other methods for obtaining the remaining constraint set fall within the protection scope of the present invention.

As a preferred embodiment, S400 further includes: and when the operation type of the traversed current operator is matched with the L-type constraint solver and the last matched constraint solver is one of the L-type constraint solvers, the current operator is matched with the last matched constraint solver.

It will be appreciated that during the traversal process, the adapted largest sub-tree subtree _i is replaced with the intermediate variable VM _ij and the tree structure tree "is updated, and the traversal is based on the tree" when traversing the next node. And after all traversals are completed, all constraint conditions of all constraint solvers of exp adaptation are obtained.

As an example, cs= { CS ₁,CS₂ }, where CS ₁ is a SAT solver, CS ₂ is a CSP solver, CS ₁ adapted operations are bit operations and logical operations, the operations that CS ₂ adapts are arithmetic operations, relational operations, collective relational operations, and logical operations. The constraint expression is: g- > ((x+ (y x z)) > (a| (b & c))), the tree structure of the constraint expression is a tree, see fig. 2 (a), which shows the tree. First, CS ₁ is adapted, and traversal is performed upwards from the leaf node of the tree, so that the sub-expression corresponding to the largest sub-tree subtree ₁,subtree₁ of the adapted CS ₁ is "a| (b & c)". the first intermediate variable VM ₁₁ of CS ₁ is created, replaced subtree ₁ with VM ₁₁, And updating the tree structure to obtain tree', and generating a first new child constraint according to VM ₁₁ and subtree ₁: CC ₁₁:=VM₁₁ = (a| (b & c)). the tree structure of tree 'is shown in fig. 2 (b), and then the adaptation CS ₂ traverses up from the leaf node of tree', resulting in the sub-expression corresponding to the largest sub-tree subtree ₂,subtree₂ of the adaptation CS ₂ being "((x+ (y×z)) > VM ₁₁". The first intermediate variable VM ₂₁ of CS ₂ is created, replaced subtree ₂ with VM ₂₁, and updating the tree structure to obtain a tree ", generating a first new child constraint according to VM ₂₁ and subtree ₂: CC ₂₁:=VM₂₁==((x+(y×z)) > VM₁₁. tree "as shown in fig. 2 (c), since the last operator left is" - > ", the type of operation of this logical operation is adapted to both CS ₁ and CS ₂, since the last adapted constraint solver is CS ₂, In order to optimize the algorithm, at this time, i.e. continue to adapt CS ₂, the tree's leaf node is traversed upwards, resulting in the sub-expression corresponding to the largest sub-tree subtree ₃,subtree₃ of the adapted CS ₂ being "g- > VM ₂₁". A second intermediate variable VM ₂₂ of CS ₂ is created, replaced subtree ₃ with VM ₂₂, Finally, replacing the tree structure with a node, and generating a second new child constraint according to the VMs ₂₂ and subtree ₃: CC ₂₂:=VM₂₂==g->VM₂₁. After the traversal is completed, constraint conditions P= { P ₁,P₂ } of each type of constraint solver are adapted, wherein ,P₁=(V,VM₁,VM₂,CC₁,CF),P₂=(V,VM₂,VM₁,CC₂,CF). is obtained, and the original variable set is obtained V={a,b,c,x,y,z,g},VM₁={VM₁₁},VM₂={VM₂₁,VM₂₂},CC₁={CC₁₁},CC₂={CC₂₁,CC₂₂},CF=。

In summary, the present invention provides a method for adapting a constraint solver, which is to preset constraint solvers of different types and operation types thereof, convert constraint expressions to be adapted into a tree structure, adapt the obtained operation types to the preset constraint solvers of different types in the process of traversing the tree structure, replace the maximum subtree of adaptation with a node of an intermediate variable, and then continue traversing adaptation, so as to finally complete the disassembly of the constraint expressions into sub-constraints of a plurality of different constraint solvers, wherein the sub-constraint obtained by each constraint solver is the operation type good for the current constraint solver, thereby improving the solving efficiency of the constraint solver and the accuracy of the solving result.

An embodiment of the present invention also provides a non-transitory computer readable storage medium, which may be disposed in an electronic device, to store at least one instruction or at least one program related to implementing a method in the method embodiment, where the at least one instruction or the at least one program is loaded and executed by the processor to implement the method provided in the above embodiment.

An embodiment of the present invention also provides an electronic device including a processor and the aforementioned non-transitory computer-readable storage medium.

An embodiment of the invention also provides a computer program product comprising program code for causing an electronic device to carry out the steps of the method according to various exemplary embodiments of the invention as described in the specification, when said program product is run on the electronic device.

According to the method provided by the embodiment of the invention, the solving efficiency and the solving accuracy of each solver can be improved, but a dependency relationship possibly exists among a plurality of sub-constraints adapted by different constraint solvers, and when N constraint solvers jointly solve the same constraint expression, mutual waiting among the sub-constraints possibly occurs, so that the calculating efficiency is low. Therefore, on the basis of the first embodiment, the invention also provides a second embodiment, which optimizes the cooperative process of the N constraint solvers and improves the calculation efficiency.

Example two

Referring to fig. 3, a flow chart of a collaborative method based on a plurality of constraint solvers is shown, the method comprising:

and P100, acquiring N types of constraint solvers CS.

Alternatively, the constraint solver may also be the core algorithm of the constraint solver.

P200, obtaining constraint conditions P of each type of constraint solver in the constraint expression exp adaptation CS, wherein the constraint conditions of each type of constraint solver comprise an original variable set V of all variables in exp, a current intermediate variable set VM generated by the adaptation current constraint solver, other intermediate variable sets VMC of all constraint solvers except the current constraint solver, an new sub-constraint set CC generated by the current constraint solver and a residual constraint set CF which cannot be matched by N types of constraint solvers.

It should be noted that, in the first embodiment, the constraint solver CS, the constraint expression exp, the constraint condition P, and the obtaining steps thereof are applicable to the second embodiment, and are not described in detail.

As can be seen from the first embodiment, the step of obtaining the j-th current intermediate variable VM _ij in the VM _i of the i-th constraint solver CS _i includes: when the operation type of sub-expression subexp _ij of exp matches the operation type of the good-quality operation type bound to class i constraint solver CS _i, the step of replacing subexp _ij with the j-th new child constraint CC _ij in CC _i of VM _ij.CS_i includes: new child constraints CC _ij for CS _i are generated from subexp _ij and VM _ij.

P300, calculating exp according to P, comprising the following steps:

And P310, selecting candidate variables from V and respective VM by each type of constraint solver in CS to obtain candidate variables of each type of constraint solver.

Wherein the step of choosing candidate variables is done inside the respective constraint solver. The candidate variables chosen by each constraint solver are either the original variables in the original set of variables or the intermediate variables in the current set of intermediate variables.

Optionally, each type of constraint solver picks candidate variables according to preset internal rules. The internal rules are rules of selecting variables in the respective internal parts of constraint solvers of each type preset in advance by a user.

P320, the cooperative scheduler selects L target candidate variables from all candidate variables of CS, and respectively obtains random values of the L target candidate variables, wherein L is greater than or equal to 1, and L is less than or equal to N.

Optionally, the collaborative scheduler is configured to collaborative solve a plurality of constraint solvers, and is a pre-designed reusable software structure framework, where the framework is responsible for scheduling each constraint solver to perform collaborative calculation solution.

Optionally, the co-scheduler picks the target candidate variable according to a preset global rule. The global rule is a rule preset in advance for selecting a target candidate variable from candidate variables of all constraint solvers again. Optionally, the global rule includes a frequency of occurrence of the candidate variable, a range of values of the candidate variable. Other rules for selecting target candidate variables in the prior art fall within the scope of the present invention.

And P330, adding the L target candidate variables and random values thereof into the to-be-propagated list bList.

And P340, when the target candidate variable in bList is empty, obtaining a collaborative calculation result of exp, and ending the cycle.

It should be noted that when the target candidate variable in bList is empty, it is noted that all the original variables of V in P310 and all the intermediate variables of all the constraint solvers have been selected and propagated, and all the variables have obtained corresponding values, so that a collaborative calculation result of exp can be obtained.

P350, each constraint solver propagates bList within the respective CC and CF ranges when the target candidate variable in bList is not null.

It will be appreciated that by propagating bList, it can be ensured that, in the range of each of the respective CCs and CFs of each constraint solver, when the value of the target candidate variable changes, all other variables affected by the change and constraint conditions can be updated accordingly, thereby achieving a state in which the whole system satisfies all constraints. According to the cooperative method, the target candidate variable and the random value thereof are selected through the cooperative scheduler, so that N constraint solvers can perform cooperative calculation, and the calculation efficiency is improved.

The prior art propagation mechanisms for propagating values of variables fall within the scope of the present invention.

It will be appreciated that when the value of a variable is propagated updated, the effect of the updated value of the variable on the constraints and other variables associated therewith is examined. If the updated values do not satisfy the current constraint, the values of other variables associated therewith are adjusted to re-satisfy the current constraint, and the process proceeds recursively until a steady state is reached, i.e., all constraints are satisfied, or no solution is determined.

As a preferred embodiment, the P350 further includes the step of the i-th constraint solver CS _i propagating the t-th target candidate variable var _t and its r-th random value data _r:

And P351, returning to the cooperative scheduler when conflict occurs in the CS _i propagation process, and calling the rollback function of the CS _i by the cooperative scheduler to execute the steps P3511-P3513 for rollback.

Where a conflict refers to a change or assignment of a variable value that violates other existing constraints. Conflicts include multiple conflict types, for example, a logical conflict may occur when a variable's value results in a directly related constraint no longer being established.

Wherein each constraint solver has three functions, the first function is to pick candidate variables, the second function is a propagation function, and the third function is a rollback function.

P3511, obtain the current value range rang _t of var _t.

Where data _r is the random value of var _t and rang _t is all possible values that var _t could theoretically take. During propagation, if the value of var _t is determined, the actual scaling down rang _t is scaled down to data _r. When data _r fails to propagate, it is stated that data _r cannot meet the constraint and needs to be excluded from rang _t.

P3512, data _r is excluded from rang _t, resulting in an updated value range rang _t' for var _t.

P3513, when rang _t' is not null, reverting to S310; otherwise, the rollback is unsuccessful, the calculation fails, and the loop of S300 is exited.

It should be noted that if rang _t' is null, it indicates that no possible value can satisfy all relevant constraints, i.e., the constraint expression has no solution, and thus the calculation fails. The calculation amount can be reduced and the calculation efficiency can be improved by determining the value of each variable in the rollback mode.

Other rollback methods for conflict in the prior art fall within the protection scope of the present invention.

As a preferred embodiment, the P350 further includes the step of propagating the t-th target candidate variable var _t and its r-th random value data _r of the i-th constraint solver CS _i:

p352, when no conflict occurs in the CS _i propagation process, comprises the following steps:

p3521 checks V, CS _i whether there is a change in the current value range of the variable in the current intermediate variable set VM _i, the other intermediate variable sets VMC (i) of all constraint solvers except CS _i.

When the data _r of the var _t changes, the value fields of other variables directly or indirectly dependent on the var _t change. That is, when the random value data _r of var _t is determined, the constraint conditions associated with the values are re-evaluated, and the legal value ranges of other variables depending on the constraints are affected. The propagation of data _r not only updates the actual value of var _t, but more importantly adjusts the value fields of the variables in all constraints by propagation.

P3522, if present, acquires the intersection of the value ranges before and after the change.

If the intersection is not null, then var _t and rang _t are added to the to-be-propagated list and P350 is returned. The obtained values of the variables meeting the constraint are synchronized to all constraint solvers in the mode.

Other methods of synchronizing variable values in the prior art fall within the scope of the present invention.

As a preferred embodiment, P352 further comprises:

If the intersection is empty, P3524 determines that a collision occurs, and the rollback process is performed according to P351.

As a preferred embodiment, P350 further comprises:

P353, the co-scheduler excludes bList the target candidate variable for which the value has been determined, and returns to S310. For example, the following two cases are those in which a candidate variable worth targeting has been determined: first, when the random value of the current variable is successfully propagated, the value range of the current variable is the random value successfully propagated. Second, the range of a variable is reduced to a single value during propagation. It has been determined that the value of the current variable satisfies all constraints and therefore no further propagation is required.

In summary, the present invention provides a collaborative method based on a plurality of constraint solvers, which selects candidate variables through each constraint solver, then selects a target candidate variable from all candidate variables again through a collaborative scheduler, obtains a random value of the target candidate variable, adds the target candidate variable and the random value thereof into a propagation list, and propagates bList in the range of each new added sub-constraint set and the residual constraint set. The collaborative method can enable all constraint solvers to cooperatively calculate, and improves the efficiency and accuracy of calculating constraint expressions.

Embodiments of the present invention also provide a non-transitory computer readable storage medium that may be disposed in an electronic device to store at least one instruction or at least one program for implementing one of the methods embodiments, the at least one instruction or the at least one program being loaded and executed by the processor to implement the methods provided by the embodiments described above.

Embodiments of the present invention also provide an electronic device comprising a processor and the aforementioned non-transitory computer-readable storage medium.

Embodiments of the present invention also provide a computer program product comprising program code for causing an electronic device to carry out the steps of the method according to the various exemplary embodiments of the invention as described in the specification, when said program product is run on the electronic device.

While certain specific embodiments of the invention have been described in detail by way of example, it will be appreciated by those skilled in the art that the above examples are for illustration only and are not intended to limit the scope of the invention. Those skilled in the art will also appreciate that many modifications may be made to the embodiments without departing from the scope and spirit of the invention. The scope of the present disclosure is defined by the appended claims.

Claims

1. A method of adapting a constraint solver, the method comprising the steps of:

S100, acquiring N types of constraint solver sequences CS to be adapted and the operation types of the N types of constraint solver sequences CS to be adapted; wherein cs= { CS ₁,CS₂,…,CS_i,…,CS_N},CS_i is an i-th type constraint solver in CS, and the value range of i is 1 to N;

s200, obtaining a constraint expression exp of a constraint solver to be adapted;

s300, constructing a tree structure tree of the constraint expression according to exp;

s410, acquiring a tree' -of a tree structure updated last time;

S420, traversing upwards from leaf nodes of tree', acquiring an adapted maximum subtree subtree _i according to the operation type of the traversed adapted CS _i, and obtaining a j-th sub-expression subexp _ij of CS _i according to subtree _i;

s430, creating a j-th current intermediate variable VM _ij of the CS _i;

S440, replacing subtree _i in the tree 'with a node bound with the VM _ij to obtain an updated tree structure tree';

S450, generating a new amplicon constraint CC _ij of CS _i according to VM _ij and VM subexp _ij;

Wherein the method further comprises:

S471, when traversing upwards from the leaf node of the tree', obtaining the target operation type of the traversed node, and when the target operation type is not matched with the N-type constraint solver, obtaining the h-th discomfort sub tree Usubtree _ih; and obtaining an h discomfort gamete expression Usubexp _ih according to Usubtree _ih;

s472, creating an h intermediate variable VF _h;

S473, generating an h residual constraint CF _ih of the CF according to Usubexp _ih;

Wherein S420 further comprises: subtree _i acquisition:

S421, traversing upwards from the leaf node along the path to the root node, and continuing traversing upwards when the operation type of the traversed operator node is adapted to CS _i; when the operation type of the traversed operator node is not suitable for CS _i, returning to the operator node of the adapting CS _i of the previous traversal, and continuing to traverse on the other branch after returning;

2. The method of claim 1, wherein S450 further comprises:

VM _ij and CC _ij satisfy: CC _ij:=VM_ij==subexp_ij; wherein "=" is a definition symbol.

3. The method of claim 1, wherein S400 further comprises: and when the operation type of the traversed current operator is matched with the L-type constraint solver and the last matched constraint solver is one of the L-type constraint solvers, the current operator is matched with the last matched constraint solver.

4. The method of claim 1, wherein the original set of variables V for all sub-constraints in P are the same, all variables in exp.

5. The method of claim 1, wherein the constraint expression in S200 comprises an operand and an operator, the operand being a constant or a variable.

6. The method of claim 5, wherein S421 further comprises: the judging method of the operation type of the node is as follows: when traversing to the operator node, determining the operation type according to the operator node.

7. A non-transitory computer readable storage medium having stored therein at least one instruction or at least one program, wherein the at least one instruction or the at least one program is loaded and executed by a processor to implement the method of any one of claims 1-6.

8. An electronic device comprising a processor and the non-transitory computer readable storage medium of claim 7.