Minicard (bigraph.Minicard)

Types

type t

The type of MiniCARD solvers.

type var

The type of solver variables.

val pp_var : 
  Ppx_deriving_runtime.Format.formatter ->
  var ->
  Ppx_deriving_runtime.unit

val show_var : var -> Ppx_deriving_runtime.string

type lit

The type of literals.

val pp_lit : 
  Ppx_deriving_runtime.Format.formatter ->
  lit ->
  Ppx_deriving_runtime.unit

val show_lit : lit -> Ppx_deriving_runtime.string

type value =

| False
| True
| Unknown

The value of a variable in a model.

val pp_value : 
  Ppx_deriving_runtime.Format.formatter ->
  value ->
  Ppx_deriving_runtime.unit

val show_value : value -> Ppx_deriving_runtime.string

Solver interface

Overview

The typical workflow when using the solver is:

Create a solver instance with create
Create variables with new_var
Build literals using pos_lit and neg_lit
Add clauses and cardinality constraints
Invoke solve or get_models
Inspect assignments with value_of

Solver instances are mutable and constraints accumulate incrementally until solving or model enumeration.

val create : unit -> t

Create a new solver.

Raises Out_of_memory if memory allocation fails.

Solver options

val set_verbosity : t -> int -> unit

Set the verbosity level.

0: silent
1: some logging
2: verbose logging

The default level is 0.

val set_phase_saving : t -> int -> unit

Control the level of phase saving.

0: disabled
1: limited
2: full

The default level is 2.

val set_detect_clause : t -> bool -> unit

Enable detection of cardinality constraints that are equivalent to clauses.

The default value is false.

Variables and literals

val new_var : t -> var

new_var s creates and returns a fresh variable in solver s. Variables are numbered consecutively starting from 0.

val pos_lit : var -> lit

pos_lit v returns the positive literal associated with v.

val neg_lit : var -> lit

neg_lit v returns the negative literal associated with v.

val negate : lit -> lit

negate l returns the negation of literal l. The following identity holds:

  negate (negate l) = l

Clauses

val add_clause : t -> lit list -> unit

add_clause s lits adds the clause represented by the disjunction of literals in lits to solver s.

For example:

  add_clause s [ a; b; c ]

encodes:

$a \vee b \vee c$ .

An empty clause makes the instance unsatisfiable. Specialised helpers exist for clauses of arity 0 to 4.

val add_clause_empty : t -> unit

val add_clause_unit : t -> lit -> unit

val add_clause_binary : t -> lit -> lit -> unit

val add_clause_ternary : t -> lit -> lit -> lit -> unit

val add_clause_quaternary : t -> lit -> lit -> lit -> lit -> unit

Cardinality constraints

val add_at_most : t -> lit list -> int -> unit

add_at_most s lits k adds an at-most cardinality constraint. The constraint states that at most k literals in lits may be assigned True.

val add_at_least : t -> lit list -> int -> unit

add_at_least s lits k adds an at-least cardinality constraint. The constraint states that at least k literals in lits may be assigned True.

Solving and models

val solve : t -> bool

solve s attempts to solve the current constraint set. Returns true if the constraints are satisfiable and false otherwise.

Note. The particular satisfying assignment returned by the solver is not deterministic and may depend on internal heuristics and optimisation settings.

val simplify : t -> unit

simplify s simplifies the current constraint set. This performs unit propagation and removes satisfied constraints.

Note. Calling this function is optional and preserves satisfiability.

val okay : t -> bool

okay s is false if the solver has already derived a contradiction from the currently added constraints.

Note. A return value of true does not guarantee satisfiability.

val value_of : t -> var -> value

value_of s v returns the value of variable v in the model produced by the most recent successful call to solve.

Raises Failure if v is not a valid variable index.

val get_models : ?vars:var list -> t -> var list list

get_models ?vars s enumerates all models of solver s. Each model is represented as the list of variables assigned True in that model. If vars is provided, blocking clauses are constructed using only the variables in vars. Otherwise all variables are used.

Models are distinguished only with respect to the variables used to construct blocking clauses. Returned models are still complete assignments over all variables.

Warning. This function modifies the solver state internally by adding blocking clauses and therefore does not support incremental solving.

Note. Model enumeration order and representative models are not deterministic and may depend on internal solver heuristics.

Model enumeration may require exponential time and memory.

Statistics

type stat = {

v : int;
(*
Number of variables.
*)
c : int;
(*
Number of clauses.
*)
mem : float;
(*
Memory used in MB.
*)
cpu : float;
(*
CPU time in seconds.
*)

}

val pp_stat : 
  Ppx_deriving_runtime.Format.formatter ->
  stat ->
  Ppx_deriving_runtime.unit

val show_stat : stat -> Ppx_deriving_runtime.string

val get_stats : t -> stat

Return statistics for the solver.

Note. Memory usage and CPU time are inherently non-deterministic and may vary between executions.

This function may only be called after solve.

val cpu_time : unit -> float

Cumulative user CPU time (seconds) for the process, as measured by the solver's C layer. Monotonic; not reset per solve.

Example usage

We begin by creating a solver and three propositional variables:

  # #require "ppx_deriving.runtime"
  # open Minicard;;
  # #install_printer pp_var;;

  # let s = create ();;
  val s : t = <abstr>
  # let x0 = new_var s
    and x1 = new_var s
    and x2 = new_var s;;
  val x0 : var = 0
  val x1 : var = 1
  val x2 : var = 2

Literals are constructed from variables using pos_lit and neg_lit. We can encode the conjunction of clauses:

$(x_0 \vee x_1) \wedge (\neg x_0 \vee x_2) \wedge \neg x_1$

as follows:

  # add_clause_binary s (pos_lit x0) (pos_lit x1);;
  - : unit = ()
  # add_clause_binary s (neg_lit x0) (pos_lit x2);;
  - : unit = ()
  # add_clause_unit s (neg_lit x1);;
  - : unit = ()

We can now check satisfiability:

  # solve s;;
  - : bool = true

Solver statistics can be queried after solving:

  # get_stats s;;
  - : stat = {v = 3; c = 3; mem = 0.; cpu = 0.080029}

The returned statistics include the number of variables and clauses, together with approximate memory usage and accumulated CPU time.

Since the instance is satisfiable, we can inspect the model returned by the solver:

  # value_of s x0;;
  - : value = True
  # value_of s x1;;
  - : value = False
  # value_of s x2;;
  - : value = True

The assignment satisfies all three clauses:

$x_0 \vee x_1$ is satisfied because $x_0 = \top$
$\neg x_0 \vee x_2$ is satisfied because $x_2 = \top$
$\neg x_1$ is satisfied because $x_1 = \bot$

Cardinality constraints restrict the number of literals that may be assigned $\top$ . For example:

  # add_at_most s
      [pos_lit x0; pos_lit x1; pos_lit x2]
      1;;
  - : unit = ()

states that at most one variable among $\{x_0, x_1, x_2\}$ may be assigned $\top$ .

The constraint set is now unsatisfiable:

  # solve s;;
  - : bool = false

Indeed, the original clauses force at least two variables to be assigned $\top$ in the model.

As another example, contradictory unit clauses immediately make the instance unsatisfiable:

  # let s = create ();;
  val s : t = <abstr>
  # let x = new_var s;;
  val x : var = 0
  # add_clause_unit s (pos_lit x);;
  - : unit = ()
  # add_clause_unit s (neg_lit x);;
  - : unit = ()
  # okay s;;
  - : bool = false
  # solve s;;
  - : bool = false

We now construct a fresh solver to demonstrate model enumeration:

  # let s = create ();;
  val s : t = <abstr>
  # let x0 = new_var s
    and x1 = new_var s
    and x2 = new_var s;;
  val x0 : var = 0
  val x1 : var = 1
  val x2 : var = 2

The following constraints require exactly one variable among $\{x_0, x_1, x_2\}$ to be assigned $\top$ :

  # add_at_least s
      [pos_lit x0; pos_lit x1; pos_lit x2]
      1;;
  - : unit = ()
  # add_at_most s
      [pos_lit x0; pos_lit x1; pos_lit x2]
      1;;
  - : unit = ()
  # solve s;;
  - : bool = true

We can enumerate all satisfying assignments:

  # get_models s;;
  - : var list list = [[0]; [2]; [1]]

The solver therefore finds exactly three models:

$x_0 = \top$ , $x_1 = \bot$ , $x_2 = \bot$
$x_0 = \bot$ , $x_1 = \top$ , $x_2 = \bot$
$x_0 = \bot$ , $x_1 = \bot$ , $x_2 = \top$

get_models also supports projected model enumeration. In the following example, blocking clauses are constructed using only the variable $x_0$ :

  # let s = create ();;
  val s : t = <abstr>
  # let x0 = new_var s
    and x1 = new_var s;;
  val x0 : var = 0
  val x1 : var = 1
  # add_clause_binary s (pos_lit x0) (pos_lit x1);;
  - : unit = ()
  # solve s;;
  - : bool = true

We enumerate the models with:

  # get_models ~vars:[x0] s;;
  - : var list list = [[1; 0]; [1]]

The clause $x_0 \vee x_1$ has three satisfying assignments:

$x_0 = \top$ , $x_1 = \bot$
$x_0 = \bot$ , $x_1 = \top$
$x_0 = \top$ , $x_1 = \top$

Since blocking clauses are constructed using only $x_0$ , models are distinguished only by the value assigned to $x_0$ . The solver therefore returns one representative model for each possible value of $x_0$ .

The returned models are still complete assignments over all variables.