PartialAssignments.hpp File Reference

Plans regarding partial assignments. More...

Go to the source code of this file.

Detailed Description

Plans regarding partial assignments.

Boolean partial assignments
  • We have a notion of a "partial assignment" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac.
  • Syntactically a partial assignment is just a set of literals.
  • Semantically a partial assignment (as a set of total assignments) is the same as a DNF-clause.
  • We have the relation "phi <= psi", meaning that the set of total assignments for phi is a superset for that of psi. This is the same as the implication-relation for DNF-clauses.
  • However there are further operations associated with partial assignments:
    1. composition
    2. application phi * F
    3. evaluation phi(v), phi(x), phi(F)
  • Shall we make a notational difference between "partial assignments" and "partial multiassignments", or is it just depending on the underlying literal-type?

Definition in file PartialAssignments.hpp.