OKlibrary  0.2.1.6
UnitClausePropagation.hpp File Reference

Plans for Maxima-components regarding UCP. More...

Go to the source code of this file.


Detailed Description

Plans for Maxima-components regarding UCP.

Todo:
Connections
Todo:
The most basic form of UCP
  • DONE ucp_0_cs is also needed in the form returning a partial assignment.
  • And we need the forms for formal clause-sets and clause-lists.
  • Currently we have two forms of ucp:
    1. If the input F is found unsatisfiable, then {{}} is returned.
    2. The other extreme is that as soon as the empty clause has been created, the reduction process stops.
    Likely we should indicate this in the names: "ucp_full, ucp_min" ?

Definition in file UnitClausePropagation.hpp.