Previous  Up  Next

Module Dpll_core


module Dpll_core: sig .. end
State and actions of a MiniSat like DPLL solver.

A low level interface to a DPLL solver with an implementation following the algorithm presented in the following paper:



Solver Creation, Problem Setup and Solution


type solver
Type of DPLL-based SAT solver instances.
val new_solver : unit -> solver
New DPLL solver. 


val fresh_variable : solver -> Dpll_literal.Variable.t
Fresh variable in the given solver. 


val add_clause : solver -> Dpll_literal.Literal.t list -> unit
Adds the clause (disjunction of literals) to the solver.
val model : solver -> Dpll_literal.Literal.t list
A model satisfying the problem. 


val add_interface_variable : solver -> Dpll_literal.Variable.t -> unit
add_interface_variables s v treats the variable v and its negation as interface literals. 


val is_interface_variable : solver -> Dpll_literal.Variable.t -> bool
Is the variable an interface_variable?

Solver Status


val decision_level : solver -> int
The number of variables assigned arbitrarily by Dpll_core.decide in the current solver state. 


val inference_possible : solver -> bool
Might an inference be made?
val get_literal_possible : solver -> bool
Is there an interface literal in the current partial model that has not been dispatched by Dpll_core.get_literal since it was assigned?
val conflict_detected : solver -> bool
Has the solver deduced that the current (partial) model cannot be (extended to) a satisfying variable assignment?

If a conflict is detected, then either the problem is unsatisfiable, or it may be resolved by a backjump, or there is a literal assigned using set_literal that must be explained.

val decision_possible : solver -> bool
Might further arbitrary variable assignment decisions be attempted?
val backjump_possible : solver -> bool
Might a backjump be used to resolve a conflict? 


val satisfied : solver -> bool
Has the solver deduced that the current model is a satisfying assignment for every variable? 


val unsatisfiable : solver -> bool
Has the solver deduced that the problem is unsatisfiable?



Literal Status



Functions to access the status of a literal in the current solver state. A literal is either unassigned or assigned true or assigned false. If a literal is assigned a value (true or false), it is either a decision literal, or inferred by unit propagation or else externally set.
val is_true : solver -> Dpll_literal.Literal.t -> bool
Is the literal assigned true?
val is_decided : solver -> Dpll_literal.Literal.t -> bool
Has the literal been assigned by arbitrary decision?
val is_inferred : solver -> Dpll_literal.Literal.t -> bool
Has the literal been inferred by unit propagation?
val level : solver -> Dpll_literal.Literal.t -> int
The decision level at which a literal was assigned. Only meaningful if the literal is currently assigned.

Search and Inference


val decide : solver -> unit
Makes an arbitrary assignment to an unassigned variable. 


val infer : solver -> unit
Attempt to infer a unit propagation or a conflict. 


val set_literal : solver -> Dpll_literal.Literal.t -> unit
Attempt 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. 


val get_literal : solver -> Dpll_literal.Literal.t
Choose an interface literal assigned true in the current partial model that has not been chosen since it was assigned.



Conflict Resolution


val set_conflict_clause : solver -> Dpll_literal.Literal.t list -> unit
set_conflict_clause ls initializes the conflict clause with the disjoined literals. 


val literal_to_explain : solver -> Dpll_literal.Literal.t
Returns the next conflict literal to explain for conflict resolution. 


val set_literal_explanation : solver -> Dpll_literal.Literal.t list -> unit
set_literal_explanation s ls removes Dpll_core.literal_to_explain from the set of conflict literals using the provided explanation ls. 


val backjump : solver -> unit
Resolve a conflict by backjumping to undo conflicting assignments from the current partial model. A learned clause is added to the solver instance to prevent the same conflict later.



Search Optimization


val forget_some_learned_clauses : solver -> unit
Forget some clauses learned by the solver though conflict analysis. 


val restart : solver -> unit
Undo all arbitrary variable assignment decisions.



Usage Statistics


val num_vars : solver -> int
Number of variables created.
val num_clauses : solver -> int
Number of added clauses that are tracked in current state.
val num_learneds : solver -> int
Number of clauses learned through conflict analysis in current state.
val num_conflicts : solver -> int
Number of conflicts encountered.
val num_decisions : solver -> int
Number of arbitrary variable assignment ever tried.
val num_inferences : solver -> int
Number of variable assignment ever made by unit propagation.
val num_externally_set : solver -> int
Number of variable assignments ever made by Dpll_core.set_literal.
Hosted by the SourceForge.net Logo* web site.
*Other names and brands may be claimed as the property of others.