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,2,3 > 1

4 > 2

5 > 3

6 > 2

7 > 3

8 > 5

9 > 6

10 > 6

11 > 6

12 > 8

20 > 15

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 lookahead 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]

2,3 > [0, 1]

4 > [2, 3]

5 > [10, 16]

6 > [4, 7]

7 > [40, 48]

8 > [92, 143]

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 clausesets

Here we look at the problem of searching for (special) hitting clausesets.

The fundamental propagator "hittingcls_propagator(n,L)", where n is the number of boolean variables in the hittingcls, and L is the list of (precise) clauselengths, is composed of constraints imposing the clauselengths and imposing the conflicts.

The constraint variables correspond to the literal occurrences, and have valueset {1,0,+1}.

Constraints for exact clauselengths:

Given the list L of constraintvariables and the clauselength m, the constraint is that exactly m of them have values <> 0.

Let l be the length of L.

Unsatisfiability iff more than m nonzeros exist, or more than l  m zeros exist.

So we need the number za of zeroassignments, and the number nza of nonzero assignments.

A total solution has nza = m and za = l  m.

If za = l  m, then value zero is to be removed from the other variables.

If nza = m, then all other variables have to be set to zero.

That's it, or?

Of course, these are special cases of more general constraints; but perhaps we first postpone them.

Constraints for the hitting property:

Given two clauses "C" and "D", a constraint specifies that we have at least one conflict.

The clauses are given by their list of constraintvariables (specifying the literal occurrences).

One needs to compute then the list of common booleanvariables.

The constraint is unsatisfiable iff for all these boolean variables the domains of their constraintvariables do not contain a clash anymore.

And the constraint is satisfied iff there exists a conflict.

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 constraintvariables have still the possibility to clash (but don't do yet).

The constraint is satisfied iff c >= 1.

And the constraint is unsatisfiable iff p = 0 (and c = 0).

A domain propagation happens iff p = 1 (and c = 0), in which case zero needs to be removed from the domains of the two constraintvariables involved; potentially then we have a conflict or both have valueset {1,+1}.
Definition in file Generators.hpp.