Learning.hpp File Reference

Plans regarding (pure) learning algorithms. More...

Go to the source code of this file.

Detailed Description

Plans regarding (pure) learning algorithms.

  • Write a version of basic_learning which uses the most basic conflict analysis:
    1. In some order go through phi and remove assignments which are not needed to produce the conflict.
    2. For that, phi must become a list (with new decision variables appended to the end).
    3. The two most natural orders are the given one and the reverse order.
    4. Since we are always doing a complete restart, it seems best to use the given order, so that we try hardest to remove the first decision variable (in order to get a different new beginning).
    5. We might use a different (stronger) reduction here.
    6. If one would do "intelligent backtracking", then it seems sensible to backtrack to the first decision variable in the given order which is not used in the conflict clause.
  • The basic statistics is the number of learned clauses.
  • A variation of the algorithm returns the set of learned clauses.
  • We should run experiments on heuristics:
    1. The goal is to minimise the number of learned clauses.
    2. A first guess is satisfiability-orientation.
    3. On the other hand, like for ordinary DLL-algorithms, one can seek to maximise the number of new clauses (for stronger reductions).
    4. This seems sensible, since it (greedily) tries to make the learned clause as short as possible (by having more inferred literals).
    5. In the current framework the heuristics just sees the total clause-sets, without knowing which clauses have been learned.
    6. We should first see what can be gained within this restricted framework.
  • A variation of this algorithm does not stop with the first satisfying assignment found, but continues (and outputs all satisfying (partial) assignments found).
    1. This realises again a CNF -> DNF translation, but this time in general not producing a hitting DNF.
    2. The satisfying assignment is phi together with the enforced assignments.
    3. Outputting only phi yields a somewhat reduced representation, but likely this doesn't matter much, since the dominant factor is the number of phi's returned.
    4. Of course, from the produced satisfying assignment one can remove assignments which are not needed for the satisfaction. Removal of inferred variables should be only sensible if before the corresponding decision variable has been removed.
    5. A DNF-clause-set G is equivalent to a CNF-clause-set F iff every clause of G is a transversal of F and if union(F,comp_cs(G)) is unsatisfiable.
      • The first condition is easily checkable, and for DLL-algorithms also the second condition is easily checkable, since F can be replaced by a hitting clause-set F' which is easily checked to be implied, and then union(F',G) is an unsatisfiable hitting clause-set.
      • Now let G be the DNF-clause-set obtain by basic_learning; is it now checkable in poly-time whether G is equivalent to F?
      • For example, if F0 (as in the algorithm) is the extension of F by the learned clauses, is then perhaps {} in r(union(F0, comp_cs(G)) ??
      • We need to test this.
Intelligent conflict-analysis
  • Perhaps we make it the responsibility of an augmented reduction to deliver with each derived assignment the decision variables responsible for it.
  • This is "eager conflict-analysis".
  • Then from the falsified clause we directly obtain the conflict-clause containing only the responsible decision variables.
  • A "cheaper variant" delivers for the set of derived assignments (by the reduction) only an implication-dag, and then, when the conflict occurs, we need to analyse it further.
  • This is "lazy conflict-analysis" as used currently in practice.

Definition in file Learning.hpp.