Plans for the concept of an active clauseset.
 Todo:
 The following needs to be updated.

See supermodule Satisfiability/ProblemInstances.

See supermodule ComputerAlgebra/Satisfiability.

This file shall be partially moved to Satisfiability/ProblemInstances/ActiveClauseSets/concepts/plans and partially to Satisfiability/ProblemInstances/ClauseSets/concepts/plans.
 Todo:
 Dictionary: (The following is outdated! "clause" > "active clause" and "clauseset" > "active clauseset")

"clause" generalised to "constraint" enhanced to "active clauseset" (semantically like a constraint, but can be viewed as a clauseset)

"clauseset" generalised to "constraint satisfaction problem" enhanced to "alliance of active clausesets".
Ordinary clausesets however should now be treated as active clausesets, and not as alliances of active clausesets, since alliances of active clausesets assume that there constituents are intelligent but not numerous.
 Todo:
 Update with Concepts/plans/ClauseSets.hpp (transferring ideas from there to here or the other way around (?!)).
 Todo:
 Partial assignment (see Concepts/plans/PartialAssignments.hpp)

An active clauseset (ACLS F in the sequel) has a connection to the main partial assignment:
 it can process the new assignments
 and it can undo them.

The concept of partial assignments needs to support this. Actually, speaking of "partial assignments" might be a bit misleading, since literals for us are kind of arbitrary constraints ?!

A problem here is, that we might have different types of literals (for example unary and binary literals), and because of static typing then we need actually a tuple of partial assignments, collected into the "superassignment" phi.
 Todo:
 Evaluation

The current partial assignment phi can be evaluated (written phi(F)), returning a 4valued object:
 0 if all total assignments extending phi falsify F
 1 if all total assignments extending phi satisify F
 0/1 if there are total assignments extending phi falsifing and satisfying F
 unknown (can not be returned if all variables of F got a unique value).

So we need to extend Boost::tribool by a "4valued logic"; we need literature on that (see verification of circuits).
 Todo:
 Implied literals

The literal type of F is the same as for the associated partial assignment.

Processing the new assignment creates a list of implied literals (or should this be a partial assignment?).

If there are for example literals for equality, then this included implied equivalences.
 Todo:
 Support for local search

Given a total assignment for the variables, an alteration is produced which satisfies F or comes as close as possible to that. (Total assignment means that all variables are fixed; perhaps here we should consider only unary literals?)

For autarky search, here it must also be possible to disable variables; this is easiest understand by referring to an underlying clausemodel.
 Todo:
 Causes of conflict

For partial assignments, let "phi' <= phi" be true if var(phi') <= var(phi) and for all in var(phi') the literals phi'(v) weakens phi(v) (the set of allowed values of phi'(v) contains the set of allowed values of phi(v)).

Now if phi(F) = 0, then phi' is computed with phi' <= phi and phi'(F) = 0.
 Todo:
 Autarkies: What is an appropriate notions of autarkies? Easiest is to refer to some underlying clausemodel ?!
 Todo:
 For a "strong ACLS" all above operations are polytime in the number of variables, and are always complete (no "unknow" for evaluation, all implied literals and equivalences, the changed total assignment is satisfying). XXX This should be now "active clauses".
 Todo:
 Should we have statistics for an underlying clausemodel? XXX This seems to be the point of speaking of "active clausesets".
 Todo:
 CNF versus DNF

Regarding QBF for example, we should allow to represent conditions as CNFs and as DNFs (that is, as sets of (partial) falsifying assignments resp. (partial) satisfying assignments), potentially also allowing mixed representations.

One could also regard partial representations, that is, the condition itself recognises the satisfying and the falsying total assignments, but it might have only some partial CNF or DNFclauses "in it" (those found until now).
Definition in file ActiveClauseSets.hpp.