Plans on quantified satisfiability problems.
More...
Go to the source code of this file.
Detailed Description
Plans on quantified satisfiability problems.
 Todo:
 Create milestones
 Todo:
 Connections to other modules
 Todo:
 Basic concepts

"Quantifiers" are perhaps best represented by pairs [q,x], where q is a string "fa" ("for all") or "ex" ("there exists"), while x is a variable.

A "quantifier prefix" is a list of quantifiers.

Quantified problems are then (in the simplest form) just pairs [P,I], where P is a quantifier prefix, while I for example is a formal clauseset. Such problems are in "prenex normal form".

We also need to represent "dependent quantifiers", which perhaps are based on an underlying set of "universal variables", and are then just represented by a set of such universal variables  so dependent quantifiers just speak about existential variables.

The matrix of such a "dependent problem" is a condition depending on all universal and existential variables, and a solution is a (partial) assignment of boolean functions to the existential variables, formally depending on exactly the universal variables the existential variable depends on, such that substituting these functions into the matrix yields a tautology (in the universal variables).

Since we want to treat CNF and DNF equally, we need also the corresponding formulations seeking for counterexamples for the universal variables.
 Todo:
 Basic backtracking algorithms

Given problems in prenex normal form, perform the basic andor search, either just returning the result ("true" or "false"), or the whole tree.

This can be done for arbitrary conditions which allow the application of partial assignments.

Such a condition additionally should allow to evaluate satisfiability and the existence of autarkies in the existential variables only, crossing out the universal variables.

Analogously, the conditions additionally should allow to evaluate contradictions and the existence of "antiautarkies" in the universal variables only, crossing out the existential variables.
 Todo:
 Representing solutions by finite functions

For delivering solutions, a rich tool set for representing boolean functions, and finite functions in general, is needed (simplest with (truth) tables). See "New module FiniteFunctions" in ComputerAlgebra/Satisfiability/Lisp/plans/general.hpp.

The trivial algorithm finding some solution runs through all total assignments to the universal variables, for each case determines all total assignments to the existential variables which fulfil the condition, and then for each existential variable v determines a realiser for v which only depends on its universal variables.

For the last step the intersection over all other universal variables of assignments to v are needed (roughly).
 Todo:
 Generators
 Todo:
 Perhaps only considering the simplest case

Motivated by the coveringcode problem (see ComputerAlgebra/Satisfiability/Lisp/Generators/Codes.mac). perhaps our first algorithmic approach in the QBFarea just concerns problems of the type Q = (forall x_1, ..., x_p thereexist y_1, ..., y_q such that F(x,y) holds), where F(x,y) is a CNF allowing cardinality constraints and ordinary clauses.

Instantiation:

One basic approach is to instantiate all x_i, and then to solve the SAT problem.

Vis MUS:

Another basic approach is to consider F'(y), where all x have been crossed out, and to find a (minimally) unsatisfiable subclauseset F'', such that the original universal variables occurring in clauses of F'' don't have a clash  exactly in this case Q is false.

So here one would enumerate of minimally unsatisfiable subclausesets of F'(y), and check whether these clauses are clashfree regarding the original xvariables.

This looks attractive, since the problem of enumerating MUS's is interesting in its own right, and quite some algorithms exist for it.

Perhaps one could also include the clashfreeness condition in the search for the MUS's ?!

In any case a largest autarky for F'(y) is to be computed and applied. So practically we can assume F'(y) to be lean.

The booleanfunction approach:

To consider the booleanfunction version, that is we consider Q as a satisfiability problem in the xvariables, where now not just constant boolean functions are to be used, but boolean functions depending on the x_1, ..., x_q, and where the substitution must yield a tautology, seems already for this Pi_2level quite daunting, but nevertheless very interesting.
Definition in file general.hpp.