Plans for satisfaction problems (in general)
More...
Go to the source code of this file.
Detailed Description
Plans for satisfaction problems (in general)
 Todo:
 Variables

The set of all variables in some context is Var.

However, it seems to be to use this concept only "implicitely".
 Todo:
 Value set

The set of all possible values for the variable in Var (in some context) is Val.

Again, likely this is best only used implicitely.
 Todo:
 Total assignments

One total assignment: f: Var > Val, just treated as a function which can be evaluated on all elements of Var (while otherwise behaviour is undefined) and yields and element of Val.

The set of all total assignments is TASS (again, likely only to be used implicitely).
 Todo:
 Domain association and allowed total assignments

A domain association is a special kind of condition, given by a set of signed literals, which either specify the set of allowed or forbidden values for some variables.

So a "domain association" is nothing than a partial assignment, and perhaps we should drop this notion at all  there is a set of variables and its associated value set (the set of possible values for any variable), and if one wishes to introduce restricted variable domains, then a partial multiassigment is to be considered ?!

So a "problem" typically is given as a pair (P, phi), where P is a problem instance and phi is a partial multiassignment. One can speak of phi as the "domain association".
 Todo:
 The notion of "condition"

See ComputerAlgebra/Satisfiability/Lisp/ConstraintProblems/plans/Conditions.hpp for the realisation of these concepts.

A condition is a map from TASS to {false,true}.

A solution is a total assignment evaluating to true; perhaps better, a "satisfying assignment", since as interesting (in general) are the "falsifying assignments".

So for a most general condition, all what can be done (at first) is to run through all total assignment; this is the "oracle model".

The fundamental task (for the theory of generalised satisfiability(!)) for a condition P (like "problem"): Represent P^{1}(false) and P^{1}(true). "Representation" of sets of total assignments can mean different things:

Measure the set, either with its natural probability in the product probability space TASS, or just classifying it as empty or nonempty.

Give a powerclauseset representation, i.e., a signed CNFrepresentation of P^{1}(false) resp. a signed DNFrepresentation of P^{1}(true), where we have several refinements:

A prime powerclauseset, that is, a prime signed CNF resp. a prime signed DNF: no clause can be replaced by a smaller one (where for CNFclauses C,D it is C smaller than D iff C semantically implies D).

A hitting powerclauseset, that is, a hitting signed CNF resp. a hitting signed DNF: each pair of clauses clash, i.e., the sets of represented total assignments are disjoint.

A special case of a hitting clauseset is a full clauseset, where each pair of clauses contains (exactly) the same variables. A full DNF representation is just how "constraint satisfaction problems" are commonly understood.
The powerclauseset can be given either explicitly listed, or "online", one clause after another.

Give a BDD representation; this represents directly P^{1}(false) and P^{1}(true) together.
In each case, also partial information is important:

Regarding measurement, we can have

upper bounds

lower bounds

approximations

For powerclauseset representations, we can have subclausesets.

BDD representations are harder to make partial, since it represents satisfying and falsifying assignments at the same time.

Given a partial multiassignment phi, the most fundamental operation is the application phi*P, which is the condition which is false for total assignments f not covered by phi, and P(f) otherwise.

So phi*P in general is just the pair (P,phi) explained above as "problem". The fact, that a variable v has been eliminated, since phi assigned a specific value to v (in general phi might only restrict v to a subset of its domain), can be recorded explicitely; forgetting this explicit recording, we arrive at the usual notion of the application of a partial assignment to a generalised clauseset.

For clausesets we can forget the variables which already have been assigned, since we can define a composition of partial assignments where the first assignments always renders a later assignment void; however in the present of multiassignments this is not possible.

This notion of phi*P is satisfiability centered, we also need phi*'P, which renders every total assignment not covered by phi true.

Now the above fundamental task is to be considered for phi * P (and phi *' P).

Compare with ComputerAlgebra/Satisfiability/Lisp/plans/PartialAssignments.hpp.

The "point of view of satisfiability" is the emphasise on partial assignments and clausesets relative to a notion of "literal":

A "literal" is a special condition such that "x implies y" can always be decided "very quickly" for literals x, y, and such that all fundamental tasks can be performed "very quickly".

A "clause" is a finite set of literals, either interpreted as CNFclause ("or") or as DNFclause ("and"). There are three normalising conditions on clauses:

No literal implies another literal.

Stronger: Two literals cannot be combined into an equivalent literal.

The clause does not represent a constant condition.
It must hold for normalised clauses, that a CNFclause C implies a CNFclause D iff for all x in C there is a literal y in D such that x implies y. This restricts the notion of literals.

"Parallel" to clauses one has partial assignments, which semantically correspond to DNFclauses for satisfiability testing, and to CNFclauses for falsifiability testing, but which have a different meaning: Partial assignments steer the backtracking process.

Clausesets are set of clauses (with finitely many variables).

The fundamental tasks are solved by returning clausesets, where typically only the cumulative ksection (all clauses up to length k) is of interest: k = 0 is just the satproblem, k = 1 yields all implied unitclauses (or some of them), and so on.

One problem is, how to call these generalised "literals", "clauses", "clausesets":

"abstract" literals, ... ?

"active" literals, ... ?
As examples for such "abstract literals" we have already

boolean literals

(generalised) literals

signed (or power) literals.
See ComputerAlgebra/Satisfiability/Lisp/plans/Literals.hpp.

For an "effective condition" we have one associated literal type, and "most" basic tasks can be solved "efficiently" (generalised clauses).

These would be the "active clauses".

While the fundamental tasks can be performed in constant time for active literals, now we can do then in polynomial time.

Having a OBDD representation should mean that we have an active clause.

And perhaps also representations as hitting clausesets imply "active clause".
This kind of discussion needs cleanup (should be moved to Satisfiability/ProblemInstances/concepts/plans).

A "condition set" is a set of effective conditions, either a conjunction or a disjunction (generalising clausesets).

Finally we have "alliances of condition sets", which are combinations of condition sets, allowing for different literal types to be used.
 Todo:
 Constructing conditions

We have the propositional connectives.

And the quantifiers "for all" and "exists".
 Todo:
 Functions for conditions

var(P) yields a set of variables, such that P does not depend on variables not in var(P).
 Todo:
 Backdoors

A set of variables V is a "backdoor" for condition P regarding one of the above fundamental tasks, if for every assignment of values to the variables in V the task can be "efficiently" solved. The knowledge about some such backdoors is important structural information, either given with the problem instance itself (a priori), or computed later (a posteriori). Given some set of variables, an interesting task is to find a smallest backdoor (from the ones we know) which includes this set.

Consider as an example the condition given by AES (see Cryptanalysis/plans/Rijndael.hpp): This is a condition on n+n+k boolean variables, where n is block length and k the key length. Given n+?+k or ?+n+k variables, the remaining variables are uniquely determined and can be efficiently computed by the encryption resp. decryption algorithm.

So we have two backdoors for computing a full DNF representation.
Definition in file SatisfactionProblems.hpp.