Module Dpll

module Dpll: sig .. end
A term-level DPLL solver.

A term level interface to a DPLL solver. The implementation uses a form of multi-input and-inverter graphs internally as a semi-canonical term representation. More information about and-inverter graph schemes can be found in the following papers:

class make : unit -> Solver_api.dpll

Hosted by the Logo* web site.
*Other names and brands may be claimed as the property of others.