OKlibrary  0.2.1.6
PlantedSolutions.hpp File Reference

Plans for Maxima-generators for satisfiable instances with given solutions. More...

Go to the source code of this file.


Detailed Description

Plans for Maxima-generators for satisfiable instances with given solutions.

Todo:
Uniquely satisfiable problems
  • Input is a formal clause-set FF and a partial assignment phi.
  • We want to find a minimal sub-assignment 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 unit-clauses 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.