Clauses.hpp File Reference

Plans for clause-constructions. More...

Go to the source code of this file.

Detailed Description

Plans for clause-constructions.

Boolean clauses, and more general clauses
  • We have a notion of boolean clauses in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac.
    1. The meaning of literals is the same for boolean CNF-clauses and boolean DNF-clauses. (This is different from signed clauses.)
  • Also clauses of more general literals are all just plain sets.
  • With more general literals we get the problem of "standardising" clauses; see ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp.
    1. For monosigned clauses "possibly degenerated clauses" contain pairs [v,e],[v,e'] with e <> e', while this is not the case for clauses.
    2. A degenerated CNF-monosigned clause is constant true, a degenerated DNF-monosigned clause is constant false.
  • We also need to provide promotions (just promoting the literals).
Signed clauses as conditions
Sets of conditions? (Clause-sets as special cases?) Big And resp. big Or ?!

Definition in file Clauses.hpp.