Plans on finding and handling splitting trees.
More...
Go to the source code of this file.
Detailed Description
Plans on finding and handling splitting trees.
 Todo:
 Connections
 Todo:
 Write tests

Optimal splitting trees:

We need test cases for satisfiable instances!

See the CS342script for already established optimal trees (which can be used as test data).
 Todo:
 optimal_splitting_tree and optimal_r_splitting_tree

Improving "branch and bound" for the version which only seeks to find a best tree (not more exhaustive statistics):

Perhaps a heuristic can be used which tries to choose the best variable first and the worst branch (this to get the bounds tigther for the second branch).

The problem seems to be that for the first branch currently we have only a very weak bound. But for that case the second branch had a very tight bound. So for that one could actually first consider the second branch whether it can produce the trivial tree, and if not then the upper bound for the first branch can be lowered. This looks reasonable in any case.

This looks like a combination of upper and *lower* bounds, which are explored in a more distributed fashion.

But likely this heuristic versions get more complicated, and should be realised by a different function.

Perhaps storing the trees also for the worst case.

Instead of minimising the number of overall nodes, that is, minimising the number of leaves (since every inner node has exactly two successors), one can also minimise the number of trueleafes (the number of clauses in the DNFrepresentation) or the number of falseleaves (the number of clauses in the CNFrepresentation).

Introduce an additional parameter d (from 0 to inf), and for depth < d then the orbits of the automorphism group acting on the set of 2n literals is computed, and instead of evaluated all 2n trees only one element of each orbit is chosen (evaluated appropriately).

See "Symmetries" in ComputerAlgebra/Satisfiability/Lisp/plans/general.hpp.

Alternatively, one keeps a repository of clausesets already processed, and does not process isomorphic cases; similarly to e,g, derived_hitting_cs_pred_isoelim.

The repository can comprise all of the clausesets considered, or only those considered at the current node.

Instead of just getting the minimal size, a variations return the complete distribution (for every occurring tree size the number of trees for that size).

DONE When searching only for the best case, then branches which cannot improve the current minimal size can be cut off.
 Todo:
 Processing splitting trees

Latex output of splitting trees by "tex_st" in

For the docu:

Use "\usepackage{pstricks,pstnode,psttree}".

For the outermost "pstree" preferably the optional argument "[nodesep=2pt]" is added (otherwise the edges are too close to the nodes).

Via "[nodesep=2pt,levelsep=20pt]" furthermore the distance between levels could be reduced.

And via "treemode=r" the tree grows from left to right.

The graphics is only viewable via the psfile (use dvips); for creating pdffiles, first create a psfile, and then apply ps2pdf.

Yet everything on one line  could we add nice indentation?

Resolution tree creation

Write a function which takes a splitting for an unsatisfiable clauseset F, and F as second argument, and produces a resolution tree.

Apply tree pruning if an unnecessary splitting was applied.

A little helper function is needed which returns for a partial assignment phi and a clauseset F the clauses of F falsified by phi.
 Todo:
 optimal_r_splitting_tree

Given an r_ksplitting tree for F, and F, counting the satisfying assignments.

With the current algorithm computing an optimal r_2splitting tree for weak_php_fcs(6,5) is hopeless. Hopefully, as described above, introducing also lower bounds enables us to process this.

DONE (amend_r_splitting_tree does the job, for each node : the assignments are not unique anyway, only the results) We need the notion of an "extended r_ksplitting tree", which at each node contains also the (forced) partial assignment leading to the reduced clauseset at this node (except for the case where an inconsistency has been found, since here this partial assignment is not welldefined).
Definition in file SplittingTrees.hpp.