search

abau / co4

COmplexity COncerned COnstraint COmpiler
GNU General Public License v3.0
2 stars 3 forks source link

assignments should look at (no. of) variables in rules #89

Closed jwaldmann closed 10 years ago

jwaldmann commented 10 years ago

In principle, given a domain with k elements and a rule with n variables, there should be exactly k^n many labeled variants of that rule. The proof looks as if n would be chosen globally as the maximal number of variables in some rule.

Yes, that is what is happening at the moment. Since CO4 has caching/hash consing throughout, it hopefully will not waste space - but time (for the cache lookups).

abau commented 10 years ago

fixed by https://github.com/apunktbau/co4/commit/3b7d5d7a8ae6235df429acd9b17428f9a8e4efa3 .

This seems to have no effect for the SAT solver, but the resulting proof becomes shorter.