Plans for Maximagenerators for satisfiable instances with given solutions.
More...
Go to the source code of this file.
Detailed Description
Plans for Maximagenerators for satisfiable instances with given solutions.
 Todo:
 Uniquely satisfiable problems

Input is a formal clauseset FF and a partial assignment phi.

We want to find a minimal subassignment phi' of phi such that the assignments of phi  phi' are all enforced.

If phi * FF is uniquely satisfiable, then phi' * FF, or, equivalent, FF together with the unitclauses representing the assignments from phi', is still uniquely satisfiable.

DONE (see minUNISAT) The easiest approach is to choose for each step a random ordering of the variables in phi, go through them in this order, check whether after removal of this variable FF + {comp_sl(phi)} still is unsatisfiable, and remove the first such variable, repeating the whole procedure until no variable can be removed anymore.

A generalisation finds all variables which can be removed, and gives them to some heuristics to decide which to choose.

We always just call a Maxima SAT solver, but this can be a wrapper to some external SAT solver.

So that we need a generic wrapper for calling an external SAT solver (assuming extended DIMACS input and output).
Definition in file PlantedSolutions.hpp.