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.
 Todo:
 Relations to other modules
 Todo:
 Update plans:
 Todo:
 Redesign

See "Clauselists instead of clausesets" below.

See "Better general naming conventions" below.
 Todo:
 MaxSAT, weighted MaxSAT, and partial MaxSAT

We have the following definitions:

A MaxSAT problem, given a clauseset, is the problem of finding an assignment that maximises the number of satisfied clauses.

A weighted MaxSAT problem, given a clauseset and a mapping from the clauses to positiveinteger 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 clauseset and a partitioning of the clauseset 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 clauseset, a partitioning of the clauseset into "hard" and "soft" clauses, and map from "soft" clauses to positiveinteger 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 MaxSAT Evaluations; Josep Argerlich, ChuMin 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 datastructures at the Lisplevel to handle these concepts:

For MaxSAT, the standard clauselists and so on are sufficient, as the input is the same as for standard satisfiability.

Weighted MaxSAT:

We could represent this as a pair [F,w] where F is the (formal) clauseset and w is the map from clauses to weights.

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.

Actually this replacement of clauses by pairs (C,w) replaces the set (or variations) of clauses by a map (in the settheoretical sense).

For partial MaxSAT:

We could represent the input as a pair [F_H, F_S] of the "hard" clauseset and "soft" clauseset.

For a "formal" partial MaxSAT instance, it seems best to have a triple [V,F_H,F_S], rather than a pair of formal clausesets; 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 nonpartial 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.
 Todo:
 Clauselists instead of clausesets
 Todo:
 Better general naming conventions

See "Notions for clauses, clausesets etc." in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/plans/general.hpp for special issues regarding clausesets 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".

For variables: "v".

For literals: "l".

For clauses: "c".

For clausesets: "cs".

For clauselists: "cl".

For ordered clausesets: "ocs".

The "formal" versions:

"fcs", "ofcs"

"lcs", "olcs".

For "standardised clausesets 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)?

We could use the prefix "ms" for monosigned?

So "msl", "msc", "mscs", "mscl", "msfcs", "msfocs", "msfmcs", "msfomcs", "msflcs", "msfolcs".

However then we could not express that in a CNF (or DNF) we wanted to have both allowed and forbidden values?

Then we needed triples [v,e,s], where [v,e] as before, while s in {1,+1} ? (This would allow negation.)

We could also have "signed literals" (see below) additionally with negation?

We could call pairs [n,e] "nonboolean literals" ("nbl"), while triples [n,e,s] are "monosigned literals" ("msl") ?

Clausesets 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?)?

We could use the prefix "s" for signed?

So "sl", "sc", "scs", "scl", "sfcs", "sofcs", "smucs", "somucs", "slcs", "solcs".

It seems sensible to allow also triple [v,E,s], where s in {1,+1} (for efficient negation).

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 clausesets D we need also forms which are pairs [F,D], where D yields the domain of variables:

Using the suffix "ud" for "uniform domain" (D is just a set resp. a list for the ordered cases).

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:

Likely, partial assignments should be syntactically identical with clauses.

Notions: "pa", "nbpa", "mspa", "ppa", "spa".

And then, like for literals, clauses, clausesets etc. one has the CNF and the DNF*interpretation*.

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.

But we also need the representation of partial assignments via total assignments! How to call them  "total partial assignments"?

Or perhaps, since we are already using suffixes like "_l" for stating representational differernces, "pa_mp" (for map). Seems reasonable.

Then we could also have "pa_l" (as lists).

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 outputtype in the name:

However, if we do, for example "clausesets maps to hashmap", then we should use "...hm_cs(args)".

The special syntax "cs2hm(F)" should be reserved for conversions.

There is the issue of using underscores ("min_var_deg_cs") or not ("varregcsp").

Perhaps leaving it out only for those predicates.

See discussion of inplace modifications in "Singular DPreduction" in Satisfiability/Lisp/Reductions/plans/DPReductions.hpp.
 Todo:
 Develop combinations of lookahead with conflictdriven solvers

See [OK, Present and future of practical SAT solving; CSR 82008] for first schemes.

This should go to Backtracking/CombinedSchemes.mac.

Perhaps first we do not consider autarkies (and we add them later).
 Todo:
 Proof systems
 Todo:
 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 polytime 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.

Though for example once we know that the instance is satisfiable, then there is no point in running tests for minimal unsatisfiability.

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.

Such a hierarchical scheme looks alright; fits into our general, "treebased" organisation.

Different from normal functions, this also needed textoutput, to explain the findings:

Perhaps this output all goes to a file.
 Todo:
 Survey and belief propagation

We should create a new module on belief propagation and survey propagation.
 Todo:
 Converting CNFs to DNFs

This should be the special domain of lookahead solvers.

See ComputerAlgebra/Satisfiability/Lisp/Backtracking/plans/SplittingTrees.hpp.

See Satisfiability/Algorithms/AllSolutions/plans/general.hpp for plans at the C++level.

An important application is discussed in ComputerAlgebra/Satisfiability/Lisp/Preprocessing/plans/general.hpp.

In a certain sense the task is a special case of the problems discussed in ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/plans/general.hpp, however it seems to have a different focus.

The task of computing the transversal hypergraph is related, but different, namely this is computing (for a CNF) the set of *all* prime implicantes (minimal satisfying assignments), while here we typically want to minimise the number of clauses. Of course, knowing all prime implicants can help, but this restricts the problem to only small cases (i.e., "finite functions").

MG put at some time some heuristics into ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac, but this is clearly not an appropriate place.

The whole taumethodology should be applicable here (especially since we are computing the whole tree; however now we are looking at satisfiable cases).

ComputerAlgebra/Satisfiability/Lisp/Counting/plans/general.hpp is related, but likely we should have an independent module.

There are plans in Solvers/OKsolver/SAT2002/plans/general.hpp (see "Enable finding all solutions" there), but due to the use of autarkies it is not clear whether the OKsolver is the right tool here.

What is the appropriate name for the new module? "Cnf2Dnf"? Or perhaps better "Dualisation"?
Definition in file general.hpp.