general.hpp File Reference

Plans regarding the tau function (see SAT-handbook article of OK) More...

Go to the source code of this file.

Detailed Description

Plans regarding the tau function (see SAT-handbook article of OK)

Connections to other modules
Handling of demos
  • See "Handling of demos" in ComputerAlgebra/plans/Maxima.hpp.
  • We must likely update the current file.
  • We should write a dedicated demos-file with the computations for OK's handbook-article on heuristics.
Cleanup BranchingTuples/Basic.mac
  • What to do with the computations under "Convexity considerations: line versions" ?
  • The point should be to demonstrate that certain functions are not convex; see ComputerAlgebra/Satisfiability/Lisp/BranchingTuples/demos/Basic.mac.
  • For example linear combination of distances, where the target is to minimise the variance, does not yield a convex optimisation problem, as shown in ComputerAlgebra/Satisfiability/Lisp/demos/FundamentsBranchingHeuristics.mac
  • So likely all these convexity considerations should move to the demos.
Reimplement the remaining functionality from Mupad/tau.mup in Maxima
  • tau : DONE
  • tree probability distributions:
    1. tpd_flatten : DONE
    2. tpd_moment : DONE
    3. tpd_tuples
    4. td_combine
    5. tpd_ccombine
    6. tpd_ccmoment
Details of computations
  • tauprob :
    1. Are there better scaling schemes?
  • tau_eps :
    1. Could epsilon be eliminated, and the computation always proceeds until dx is 0 (for the arithmetic)?
    2. Are there better lower bounds than tau_lo ?
  • Support typical applications to worst-case upper bounds:
    1. Given a parameter alpha and branching tuples depending on alpha, find the minimal tau-value depending on alpha, for a given domain.
    2. This is a very common task, and we should provide a convenient framework for this, with some nice demos (for the upper-bounds community).
    3. The common case seems to be a linear dependence on alpha, and then the domain can be computed via linear programming.
    4. We should provide a variety of optimisation methods.
    5. See the methods for quasi-convex optimisation discussed in [Eppstein, 2006, Quasiconvex Analysis of Multivariate Recurrence Equations for Backtracking Algorithms].
  • The other basic case is optimising a distance on a given tree, and again a convenient framework needs to be provided.
    1. See ComputerAlgebra/Satisfiability/Lisp/BranchingTuples/demos/Basic.mac.
    2. See "Mupad/tau.mup" above.
  • Likely this should go into its own submodule.
Investigations on approximations
  • Perhaps for k=3 it is true that for all eps > 0 and K > eps the integral on [eps,K]^3 of dtau_3 is positive?

Definition in file general.hpp.