class type dpll = object .. end
Term level interface to a DPLL solver. A newly created DPLL solver
has the following initial properties:
Problem Setup and Solution
method owns_constant : Term.term -> bool
owns_constant c holds when
c is a boolean constant or
connective.
method add_clause : Term.term list -> unit
Adds the clause (disjunction of pure Boolean terms) to the
solver.
method proxy : Term.term -> Term.term
A proxy for a pure boolean term.
method add_interface_variable : Term.term -> unit
add_interface_variables v treats the variable
v and its
negation as an interface literal.
Solver Status
method variables : Term.Term_set.t
Set of all variables known to this solver.
method decision_level : int
Decision level of the solver.
- Ensure
0 <= decision_level
method inference_possible : bool
Might an inference be made?
method get_literal_possible : bool
Is there an interface literal in the current partial model
that has not been dispatched by
Solver_api.dpll.get_literal since it was
assigned?
method conflict_detected : bool
Has the solver deduced that the current (partial) model cannot
be (extended to) a satisfying variable assignment?
method decision_possible : bool
Might further arbitrary variable assignment decisions be
attempted?
method backjump_possible : bool
Might a backjump be used to resolve a conflict?
method satisfied : bool
Has the solver deduced that the current model is a satisfying
assignment for every variable?
method unsatisfiable : bool
Has the solver deduced that the problem is unsatisfiable?
Literal Status
method is_interface_literal : Term.term -> bool
Is the literal
l an interface literal for the solver.
method is_true : Term.term -> bool
Is the literal
l assigned true in the solver state?
method level : Term.term -> int
The decision level at which literal
l was assigned true.
Search and Inference
method decide : unit
Makes an arbitrary assignment to an unassigned variable.
method infer : unit
Attempt to infer a unit propagation or a conflict.
method set_literal : Term.term -> unit
set_literal l attempts to make a variable assignment
inferred by an external agent. The interface literal is
ignored if the corresponding variable is already assigned in
the current partial model.
method get_literal : Term.term
Choose an interface literal assigned true in the current
partial model that has not been dispatched since it was
assigned.
Conflict Resolution
method set_conflict_clause : Term.term list -> unit
set_conflict_clause ls initializes the conflict clause with
the disjoined literals.
method literal_to_explain : Term.term
Returns the next conflict literal to explain for conflict
resolution.
method set_literal_explanation : Term.term list -> unit
method backjump : unit
Resolve a conflict by backjumping to undo conflicting
assignments from the current partial model. A learned clause is
added to the solver to prevent the same conflict later.
Search Optimization
method forget_some_learned_clauses : unit
Forget some clauses learned by the solver though conflict
analysis.
method restart : unit
Undo all arbitrary variable assignment decisions.
Usage Statistics
method num_vars : int
Number of variables created.
method num_clauses : int
Number of added clauses that are tracked in current state.
method num_learneds : int
Number of clauses learned through conflict analysis in current
state.
method num_conflicts : int
Number of conflicts encountered.
method num_decisions : int
Number of arbitrary variable assignment ever tried.
method num_inferences : int
Number of variable assignment ever made by unit propagation.
method num_externally_set : int
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.