Experiment with query-driven unit propagation rules in Viatra Solver

[bergmanngabor]

Assume a well-formedness constraint with violation pattern { constraint1(x,y,z); constraint2(x,y,z); constraint3(x,y,z); } If, for given tuple (a,b,c), we have both constraint1(a,b,c) and constraint2(a,b,c) hold with certainty 1, then constraint3(a,b,c) must have a 3VL truth value of 0; so if it is currently considered unknown (1/2), then a unit propagation rule can set it to 0.

The solver will remain sane by adding any or all of similarly created unit propagation rules. (Of course not all of them have to be added, if they have a high cost, or jeopardize termination etc.)

Examples of setting a truth value to 0:

• For existence constraints, we can learn that the object does not exist
• For edge constraint, we can learn that the edge of the given type, source and target does not exist
• For node type constraints, we can learn that the object does not exhibit that type
• For equality or inequality constraints, we can learn that there is in fact an inequality or equality
• For an unflattened positive pattern call constraint, we learn that the pattern does not hold - in essence we gain yet another well-formedness constraint
• For a negative pattern call constraint, we learn that the pattern must hold (for some values of the _ parameters). In the special case where the pattern has a single body only, we learn that the constraints in those body must hold.