OKlibrary  0.2.1.6
Generators.hpp File Reference

Plans regarding generators for constraint problems. More...

Go to the source code of this file.


Detailed Description

Plans regarding generators for constraint problems.

More precisely, for specific problems propagators and instances of the general backtracking algorithms are constructed.

Todo:
Write tests
Todo:
Concept of a "propagator"
Todo:
"n Queens"
  • See Configurations/NQueens/plans/general.hpp.
  • Write a generator for boolean CNF (perhaps also in this module).
  • Write a checker for the solutions.
  • Especially when all solutions are to be determined, symmetry considerations seem necessary.
  • Application of "constraint_backtracking" (from ComputerAlgebra/Satisfiability/Lisp/Backtracking/ConstraintSatisfaction.mac) seems rather successful (at least regarding the number of nodes; the following shows n -> #nodes):
    1. 1,2,3 -> 1
    2. 4 -> 2
    3. 5 -> 3
    4. 6 -> 2
    5. 7 -> 3
    6. 8 -> 5
    7. 9 -> 6
    8. 10 -> 6
    9. 11 -> 6
    10. 12 -> 8
    11. 20 -> 15
    12. 30 -> 25
    (This table should be filled out, and linear regression performed.)
  • Could one show that we have actually a polytime procedure ? (It seems that a solution exists if n <> 2,3).
  • With a C++ implementation one could investigate larger n.
  • What is the performance of constraint solvers on this problem?
  • The above good performance of "constraint_backtracking" is likely just due to the look-ahead and the ordering heuristics. (One should have a look at the trees: How much branching is there?). This will likely break down when finding (or counting) all solutions.
  • Results of "constraint_backtracking_counting" (from ComputerAlgebra/Satisfiability/Lisp/Backtracking/ConstraintSatisfaction.mac) (the number of solutions and the number of nodes):
    1. 1 -> [1, 1]
    2. 2,3 -> [0, 1]
    3. 4 -> [2, 3]
    4. 5 -> [10, 16]
    5. 6 -> [4, 7]
    6. 7 -> [40, 48]
    7. 8 -> [92, 143]
    8. 9 -> [352, 632]
    (This problem has only total solutions, and thus the weakness of the general approach, that only total assignments can be taken into account, is irrelevant here.)
  • Of course, one could go here for optimal splitting trees.
Todo:
Hitting clause-sets
  • Here we look at the problem of searching for (special) hitting clause-sets.
  • The fundamental propagator "hittingcls_propagator(n,L)", where n is the number of boolean variables in the hitting-cls, and L is the list of (precise) clause-lengths, is composed of constraints imposing the clause-lengths and imposing the conflicts.
  • The constraint variables correspond to the literal occurrences, and have value-set {-1,0,+1}.
  • Constraints for exact clause-lengths:
    1. Given the list L of constraint-variables and the clause-length m, the constraint is that exactly m of them have values <> 0.
    2. Let l be the length of L.
    3. Unsatisfiability iff more than m non-zeros exist, or more than l - m zeros exist.
    4. So we need the number za of zero-assignments, and the number nza of non-zero assignments.
    5. A total solution has nza = m and za = l - m.
    6. If za = l - m, then value zero is to be removed from the other variables.
    7. If nza = m, then all other variables have to be set to zero.
    8. That's it, or?
    9. Of course, these are special cases of more general constraints; but perhaps we first postpone them.
  • Constraints for the hitting property:
    1. Given two clauses "C" and "D", a constraint specifies that we have at least one conflict.
    2. The clauses are given by their list of constraint-variables (specifying the literal occurrences).
    3. One needs to compute then the list of common boolean-variables.
    4. The constraint is unsatisfiable iff for all these boolean variables the domains of their constraint-variables do not contain a clash anymore.
    5. And the constraint is satisfied iff there exists a conflict.
    6. So we need to compute the value c of conflicts and the value p of open potential conflicts, the number of boolean variables for which the constraint-variables have still the possibility to clash (but don't do yet).
    7. The constraint is satisfied iff c >= 1.
    8. And the constraint is unsatisfiable iff p = 0 (and c = 0).
    9. A domain propagation happens iff p = 1 (and c = 0), in which case zero needs to be removed from the domains of the two constraint-variables involved; potentially then we have a conflict or both have value-set {-1,+1}.

Definition in file Generators.hpp.