general.hpp File Reference

Plans for SAT at Maxima/Lisp level in general. More...

Go to the source code of this file.

Detailed Description

Plans for SAT at Maxima/Lisp level in general.

Relations to other modules
Update plans:
  • See "Clause-lists instead of clause-sets" below.
  • See "Better general naming conventions" below.
MaxSAT, weighted MaxSAT, and partial MaxSAT
  • We have the following definitions:
    • A MaxSAT problem, given a clause-set, is the problem of finding an assignment that maximises the number of satisfied clauses.
    • A weighted MaxSAT problem, given a clause-set and a mapping from the clauses to positive-integer weights, is the problem of finding an assignment which maximises the sum of the weights of the satisfied clauses.
    • A partial MaxSAT problem, given a clause-set and a partitioning of the clause-set into "hard" and "soft" clauses, is the problem of finding an assignment which satisfies all of the "hard" clauses, and maximises the number of satisfied "soft" clauses.
    • A weighted partial MaxSAT problem, given a clause-set, a partitioning of the clause-set into "hard" and "soft" clauses, and map from "soft" clauses to positive-integer weights, is the problem of finding a total assignment which satisfies all "hard" clauses, and maximises the sum of the weights of the satisfied "soft" clauses.
    • Such definitions are also provided in [The First and Second Max-SAT Evaluations; Josep Argerlich, Chu-Min Li, Felip ManyĆ” and Jordi Planes].
    • MaxSAT competitions are available at http://maxsat.ia.udl.cat/ .
  • Note that in all cases where we "maximise the X of the satisfied clauses", we could also consider that we "minimise the X of the falsified clauses". This is likely better since falsified clauses are more appropriate for CNF (the standard).
  • The following tools currently utilise translations to (weighted, partial or standard) MaxSAT:
  • For MaxSAT solvers, see
    • maxsatz under "Satz",
    • "MiniMaxSAT", and
    • "Maxsat"
    in Buildsystem/ExternalSources/SpecialBuilds/plans/SAT.hpp.
  • We need data-structures at the Lisp-level to handle these concepts:
    • For MaxSAT, the standard clause-lists and so on are sufficient, as the input is the same as for standard satisfiability.
    • Weighted MaxSAT:
      1. We could represent this as a pair [F,w] where F is the (formal) clause-set and w is the map from clauses to weights.
      2. However using just pairs [C,w] of clauses of weights is more natural, since only the given clauses of weights, and the notion of a map is less natural here.
      3. Actually this replacement of clauses by pairs (C,w) replaces the set (or variations) of clauses by a map (in the set-theoretical sense).
    • For partial MaxSAT:
      • We could represent the input as a pair [F_H, F_S] of the "hard" clause-set and "soft" clause-set.
      • For a "formal" partial MaxSAT instance, it seems best to have a triple [V,F_H,F_S], rather than a pair of formal clause-sets; we (likely) never consider the total assignments over just the variables of the "soft" clauses.
      • But see below for a better possibility.
    • For weighted partial MaxSAT, it then seems natural to have a triple [F_H,F_S] where F_H and F_S are the "hard" and "soft" clauses, F_S is a weighted MaxSAT problem as above (pairs of clauses and weights). But see below.
  • Considering minimising the falsified clauses (for CNF; for DNF we should consider minimising the satisfied clauses), we can unify partial and weighted MaxSAT by considering pairs [C,w], where the weight can be inf --- this indicates that the clause shall be satisfied (this is achievable iff the minimum weight is strictly less than inf).
  • We consider thus just "wcl", i.e., weighted clauses, in all the usual variations ("wcs", "wcl", "fwcs", "fwcl").
  • The differentiation between partial and non-partial forms is just whether inf occurs or not; and for ordinary MaxSAT just all w=1.
  • In principle we could allow arbitrary w.
  • We should also a basic (weighted) (partial) MaxSAT solver at the Maxima level.
Clause-lists instead of clause-sets
Better general naming conventions
  • See "Notions for clauses, clause-sets etc." in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/plans/general.hpp for special issues regarding clause-sets etc.
  • See "Naming" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/plans/Statistics.hpp for naming of statistics.
  • Systematise the use of suffices like "cs" and "cs_f".
    1. For variables: "v".
    2. For literals: "l".
    3. For clauses: "c".
    4. For clause-sets: "cs".
    5. For clause-lists: "cl".
    6. For ordered clause-sets: "ocs".
    7. The "formal" versions:
      • "fcs", "ofcs"
      • "lcs", "olcs".
  • For "standardised clause-sets we use prefix "std", e.g., "stdcs", or "stdnbfcs".
  • What about literals as sets of pairs [v,e], where e is a value (forbidden for CNF, allowed for DNF)?
    1. We could use the prefix "ms" for monosigned?
    2. So "msl", "msc", "mscs", "mscl", "msfcs", "msfocs", "msfmcs", "msfomcs", "msflcs", "msfolcs".
    3. However then we could not express that in a CNF (or DNF) we wanted to have both allowed and forbidden values?
    4. Then we needed triples [v,e,s], where [v,e] as before, while s in {-1,+1} ? (This would allow negation.)
    5. We could also have "signed literals" (see below) additionally with negation?
    6. We could call pairs [n,e] "non-boolean literals" ("nbl"), while triples [n,e,s] are "monosigned literals" ("msl") ?
    7. Clause-sets would then be "nbcs" resp. "mscs" etc.
  • And then we have signed literals as sets of pairs [v,E], where E is a set of values (or a list?)?
    1. We could use the prefix "s" for signed?
    2. So "sl", "sc", "scs", "scl", "sfcs", "sofcs", "smucs", "somucs", "slcs", "solcs".
    3. It seems sensible to allow also triple [v,E,s], where s in {-1,+1} (for efficient negation).
    4. Such triples would sensibly be called "signed literals" ("sl"); now how to call pairs [v,E]? "Power literals" ("pl")!
  • For the various forms of generalised clause-sets D we need also forms which are pairs [F,D], where D yields the domain of variables:
    1. Using the suffix "ud" for "uniform domain" (D is just a set resp. a list for the ordered cases).
    2. While the suffix "fd" for "function domain" mean a function which assigns to every variable a set resp. a list.
  • Then we have the different kind of partial assignments:
    1. Likely, partial assignments should be syntactically identical with clauses.
    2. Notions: "pa", "nbpa", "mspa", "ppa", "spa".
    3. And then, like for literals, clauses, clause-sets etc. one has the CNF- and the DNF-*interpretation*.
    4. For clauses we wanted to stay with sets; perhaps for partial assignments we could have them ordered?
      • So speaking of "opa", "omspa" and "ospa".
      • Perhaps one should actually also allow to have ordered clauses? Better not! Then we have too many combinations.
    5. But we also need the representation of partial assignments via total assignments! How to call them --- "total partial assignments"?
    6. Or perhaps, since we are already using suffixes like "_l" for stating representational differernces, "pa_mp" (for map). Seems reasonable.
    7. Then we could also have "pa_l" (as lists).
    8. And then there are partial assignments which are actually "total assignments" (w.r.t. a set of variables)?! Perhaps using "tpa" ?
  • It seems that in general we do not mention the output-type in the name:
    1. However, if we do, for example "clause-sets maps to hash-map", then we should use "...hm_cs(args)".
    2. The special syntax "cs2hm(F)" should be reserved for conversions.
  • There is the issue of using underscores ("min_var_deg_cs") or not ("varregcsp").
    1. Perhaps leaving it out only for those predicates.
  • See discussion of in-place modifications in "Singular DP-reduction" in Satisfiability/Lisp/Reductions/plans/DP-Reductions.hpp.
Develop combinations of look-ahead with conflict-driven solvers
  • See [OK, Present and future of practical SAT solving; CSR 8-2008] for first schemes.
  • This should go to Backtracking/CombinedSchemes.mac.
  • Perhaps first we do not consider autarkies (and we add them later).
Proof systems
Finding out "all properties" of an instance
  • We need some scheme which allows to let the system run all existing tests.
  • One application would be to located poly-time classes which include the instance.
  • Perhaps all relevant functions have an "exploration" version, these versions are put into a global list, and then one just runs through this list.
  • Then there will be however duplications in the output; but perhaps this is the lesser evil.
    1. Though for example once we know that the instance is satisfiable, then there is no point in running tests for minimal unsatisfiability.
    2. Perhaps for each module we write a basic exploration function, and this function then organises the exploration at module level, while if needed asks for input established by other modules.
    3. Such a hierarchical scheme looks alright; fits into our general, "tree-based" organisation.
  • Different from normal functions, this also needed text-output, to explain the findings:
    1. Perhaps this output all goes to a file.
Survey and belief propagation
  • We should create a new module on belief propagation and survey propagation.
Converting CNFs to DNFs

Definition in file general.hpp.