Calculemus

DP Module

Namespace: Calculemus
Assembly: Calculemus.dll

The Davis-Putnam and the Davis-Putnam-Loveland-Logemann procedures.

Table of contents

Types

Type Description

trailmix

Flags to mark literals in the case split trail used in the DPLL iterative implementation. DP.dpli

Parsing clauses

Functions and values

Function or value Description

!>>xs

Full Usage: !>>xs

Parameters:
    xs : string list list - The input list of string lists.

Returns: formula<prop> list list The list of clauses.

Parses a list of string lists into a list of clauses. A clause is list of literals.

xs : string list list

The input list of string lists.

Returns: formula<prop> list list

The list of clauses.

Note

This operator is not part of the original code and it was added here for convenience.

Example 

 !>> [["p"];["p";"~q"]]
Evaluates to [[`p`]; [`p`; `~q`]].

Unit propagation rule

Functions and values

Function or value Description

hasUnitClause clauses

Full Usage: hasUnitClause clauses

Parameters:
    clauses : formula<'a> list list - The input clauses to be checked.

Returns: bool true, if clauses contain unit clauses; otherwise, false.

clauses has unit clauses.

clauses : formula<'a> list list

The input clauses to be checked.

Returns: bool

true, if clauses contain unit clauses; otherwise, false.

Note

This function is not part of the original code: it has been added to remove the use of exceptions as control flow (which causes performance degradation in F#) in the implementations of the DP and DPLL procedures.

Example 

 !>> [["p"];["p";"~q"]] 
 |> hasUnitClause
Evaluates to true.

Example 

 !>> [["p";"~q"]] 
 |> hasUnitClause
Evaluates to false.

one_literal_rule clauses

Full Usage: one_literal_rule clauses

Parameters:
    clauses : formula<'a> list list - The input clauses.

Returns: formula<'a> list list The result of 1-literal rule application, if there are unit clauses.

Applies the 1-literal rule to the input clauses.

For the first unit clause p in clauses:

  • removes any instance of ~p from the other clauses.
  • removes p and any clauses containing it.

clauses : formula<'a> list list

The input clauses.

Returns: formula<'a> list list

The result of 1-literal rule application, if there are unit clauses.

KeyNotFoundException Thrown when there aren't unit clauses.
Example

Removes the first unit clause present. 

 !>> [["p"];["s";"t"];["q"]] 
 |> one_literal_rule
Evaluates to [[`q`; `p /\ q`]].

Example

Removes also complements of the literal from other clauses. 

 !>> [["p"];["s";"~p"];["~p";"t"]]
 |> one_literal_rule
Evaluates to [[`s`]; [`t`]].

Example

Removes all clauses containing the literal of the unit clause. 

 !>> [["p"];["s";"p"];["q";"t"]] 
 |> one_literal_rule
Evaluates to [[`q`; `t`]].

Example

Fails if there aren't unit clauses. 

 !>> [["s";"p"];["q";"t"]] 
 |> one_literal_rule
Throws System.Collections.Generic.KeyNotFoundException: An index satisfying the predicate was not found in the collection..

Pure literal rule

Functions and values

Function or value Description

affirmative_negative_rule clauses

Full Usage: affirmative_negative_rule clauses

Parameters:
    clauses : formula<'a> list list - The input clauses.

Returns: formula<'a> list list The clauses cleaned of those containing pure literals, if the latter were present in the input.

Removes all clauses that contain pure literals.

clauses : formula<'a> list list

The input clauses.

Returns: formula<'a> list list

The clauses cleaned of those containing pure literals, if the latter were present in the input.

Exception Thrown with message affirmative_negative_rule when there aren't pure literals.
Example 

 !>> [["p";"q";"~t"];["~p";"q"];["p";"t"]]
 |> affirmative_negative_rule
Evaluates to [[`p`; `t`]].

Example 

 !>> [["p";"~q";"~t"];["~p";"q"];["p";"t"]]
 |> affirmative_negative_rule
Throws System.Exception: affirmative_negative_rule.

hasPureLiteral clauses

Full Usage: hasPureLiteral clauses

Parameters:
    clauses : formula<'a> list list - The input clauses to be checked.

Returns: bool true, if clauses contain pure literals; otherwise, false.

clauses has pure literals.

A literal is said to be 'pure' if it occurs only positively or only negatively in the list of clauses.

clauses : formula<'a> list list

The input clauses to be checked.

Returns: bool

true, if clauses contain pure literals; otherwise, false.

Note

This function is not part of the original code: it has been added to remove the use of exceptions as control flow (which causes performance degradation in F#) in the implementations of the DP and DPLL procedures.

Example 

 !>> [["p";"q"];["~p";"~q"]]
 |> hasPureLiteral
Evaluates to false.

Example 

 !>> [["p";"q"];["~p";"q"]]
 |> hasPureLiteral
Evaluates to true.

pureLiterals clauses

Full Usage: pureLiterals clauses

Parameters:
    clauses : formula<'a> list list - The input clauses.

Returns: formula<'a> list The list of literals that occur pure in clauses.

Pure literals in clauses.

A literal is said to be 'pure' if it occurs only positively or only negatively in the list of clauses.

clauses : formula<'a> list list

The input clauses.

Returns: formula<'a> list

The list of literals that occur pure in clauses.

Note

This function is not part of the original code: it has been added to remove the use of exceptions as control flow (which causes performance degradation in F#) in the implementations of the DP and DPLL procedures.

Example 

 !>> [["p";"q";"~t"];["~p";"q"];["p";"t"]]
 |> pureLiterals
Evaluates to [`q`].

Example 

 !>> [["p";"~q";"~t"];["~p";"q"];["p";"t"]]
 |> pureLiterals
Evaluates to [].

Resolution rule

Functions and values

Function or value Description

resolution_blowup cls l

Full Usage: resolution_blowup cls l

Parameters:
Returns: int m * n - m - n where m and m are the number of clauses in which l occurs respectively positively and negatively in cls.

A simplistic heuristic to predict the best literal to resolve on.

cls : formula<'a> list list

The input clauses.

l : formula<'a>
Returns: int

m * n - m - n where m and m are the number of clauses in which l occurs respectively positively and negatively in cls.

Example 

 let cls = !>> [
      ["p";"c"];["~p";"d"]
      ["q";"~c"];["q";"~d"];["q";"~e"];["~q";"~d"];["~q";"e"]
 ]
 
 resolution_blowup cls !>"c" // evaluates to -1
 resolution_blowup cls !>"d" // evaluates to -1
 resolution_blowup cls !>"e" // evaluates to -1
 resolution_blowup cls !>"p" // evaluates to -1
 resolution_blowup cls !>"q" // evaluates to 1

resolution_rule clauses

Full Usage: resolution_rule clauses

Parameters:
    clauses : formula<'a> list list - The input clauses.

Returns: formula<'a> list list The result of resolving the input clauses on the literal which minimizes DP.resolution_blowup.

Resolves the input clauses on the literal which minimizes DP.resolution_blowup.

clauses : formula<'a> list list

The input clauses.

Returns: formula<'a> list list

The result of resolving the input clauses on the literal which minimizes DP.resolution_blowup.

Example 

 !>> [
      ["p";"c"];["~p";"d"]
      ["q";"~c"];["q";"~d"];["q";"~e"];["~q";"~d"];["~q";"e"]
 ]
 |>  resolution_rule
Evaluates to [[`c`; `d`]; [`q`; `~c`]; [`q`; `~d`]; [`q`; `~e`];[`~q`; `e`]; [`~q`; `~d`]].

resolve_on p clauses

Full Usage: resolve_on p clauses

Parameters:
    p : formula<'a> - The literal on which to resolve.
    clauses : formula<'a> list list - The input clauses.

Returns: formula<'a> list list The result of resolving the input clauses on p, if the rule is applicable; otherwise the input unchanged.

Resolves clauses on the literal p.

  • separates clauses in those containing p only positively \(C_i\) and those only negative \(D_j\) ,
  • creates new clauses from all the combinations \(C_i \lor D_j\),
  • removes all clauses containing p or its negation.

p : formula<'a>

The literal on which to resolve.

clauses : formula<'a> list list

The input clauses.

Returns: formula<'a> list list

The result of resolving the input clauses on p, if the rule is applicable; otherwise the input unchanged.

Note

This rule can increase the clauses' size.

Example 

 !>> [["p";"c1";"c2"];
      ["~p";"d1";"d2";"d3";"d4"];
      ["q";"t"];
      ["p";"e1";"e2"]]
 |> resolve_on !>"p"
Evaluates to [[`c1`; `c2`; `d1`; `d2`; `d3`; `d4`]; [`d1`; `d2`;`d3`; `d4`; `e1`; `e2`];[`q`; `t`]].

Example 

 !>> [["a"];["b"]]
 |> resolve_on !>"p"
Evaluates to [[`a`]; [`b`]].

Davis-Putnam Procedure

Functions and values

Function or value Description

dp clauses

Full Usage: dp clauses

Parameters:
    clauses : formula<'a> list list - The input clauses.

Returns: bool true, if the recursive application of the rules leads to an empty set of clauses (meaning that the input is satisfiable); otherwise, when the rules lead to a set that contains an empty clause, false (meaning that the input is unsatisfiable).

Tests clauses (propositional) satisfiability with the Davis-Putnam procedure.

Tests the (propositional) satisfiability of a list of clauses (to be understood as an iterated conjunction of disjunctions), using the Davis-Putnam procedure which consists in applying recursively the rules DP.one_literal_rule, DP.affirmative_negative_rule and DP.resolution_rule

clauses : formula<'a> list list

The input clauses.

Returns: bool

true, if the recursive application of the rules leads to an empty set of clauses (meaning that the input is satisfiable); otherwise, when the rules lead to a set that contains an empty clause, false (meaning that the input is unsatisfiable).

Example 

 dp !>> [["p"]]
Evaluates to true.

Example 

 dp !>> [["p"];["~p"]]
Evaluates to false.

dpsat fm

Full Usage: dpsat fm

Parameters:
Returns: bool true, if the input formula is satisfiable: otherwise false.

Tests fm (propositional) satisfiability with the Davis-Putnam procedure.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is satisfiable: otherwise false.

Example 

 dpsat !> "p"
Evaluates to true.

Example 

 dpsat !> "p /\ ~p"
Evaluates to false.

dptaut fm

Full Usage: dptaut fm

Parameters:
Returns: bool true, if the input formula is a tautology: otherwise false.

Tests fm (propositional) validity with the Davis-Putnam procedure.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is a tautology: otherwise false.

Example 

 dptaut !> "p"
Evaluates to false.

Example 

 dptaut (prime 11)
Evaluates to true.

Davis-Putnam-Loveland-Logemann Procedure

Functions and values

Function or value Description

dpll clauses

Full Usage: dpll clauses

Parameters:
    clauses : formula<'a> list list - The input clauses.

Returns: bool true, if the recursive application of the rules leads to an empty set of clauses (meaning that the input is satisfiable); otherwise, when the rules lead to a set that contains an empty clause, false (meaning that the input is unsatisfiable).

Tests clauses (propositional) satisfiability with the Davis-Putnam-Loveland-Logemann procedure.

Tests the (propositional) satisfiability of a list of clauses (to be understood as an iterated conjunction of disjunctions), using the Davis-Putnam-Loveland-Logemann procedure which consists in applying recursively the rules DP.one_literal_rule, DP.affirmative_negative_rule and, if neither of these is applicable (instead of DP.resolution_rule) the splitting rule.

The splitting rule consists in choosing some literal and testing, separately, the satisfiability of the union of the input with this literal and its negation, respectively: if one of these is satisfiable so the original input is.

The literal that maximizes DP.posneg_count is chosen for the splitting rule.

clauses : formula<'a> list list

The input clauses.

Returns: bool

true, if the recursive application of the rules leads to an empty set of clauses (meaning that the input is satisfiable); otherwise, when the rules lead to a set that contains an empty clause, false (meaning that the input is unsatisfiable).

Example 

 dpll !>> [["p"]]
Evaluates to true.

Example 

 dpll !>> [["p"];["~p"]]
Evaluates to false.

dpllsat fm

Full Usage: dpllsat fm

Parameters:
Returns: bool true, if the input formula is satisfiable: otherwise false.

Tests fm (propositional) satisfiability with the Davis-Putnam-Loveland-Logemann procedure.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is satisfiable: otherwise false.

Example 

 dpllsat !> "p"
Evaluates to true.

Example 

 dpllsat !> "p /\ ~p"
Evaluates to false.

dplltaut fm

Full Usage: dplltaut fm

Parameters:
Returns: bool true, if the input formula is a tautology: otherwise false.

Tests fm (propositional) validity with the Davis-Putnam-Loveland-Logemann procedure.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is a tautology: otherwise false.

Example 

 dplltaut !> "p"
Evaluates to false.

Example 

 dplltaut (prime 11)
Evaluates to true.

posneg_count cls l

Full Usage: posneg_count cls l

Parameters:
    cls : formula<'a> list list - The input clauses.
    l : formula<'a> - The input literal.

Returns: int The number of l's occurrences (both positively or negatively) in cls.

Counts the number of occurrences (both positively or negatively) of the literal l in cls.

It is used as an heuristic to chose the literal for the splitting rule in the Davis-Putnam-Loveland-Logemann procedure.

cls : formula<'a> list list

The input clauses.

l : formula<'a>

The input literal.

Returns: int

The number of l's occurrences (both positively or negatively) in cls.

Example 

 posneg_count !>> [
      ["p";"c"];["~p";"d"]
      ["q";"~c"];["q";"~d"];["q";"~e"];["~q";"~d"];["~q";"e"]
 ] !>"q"
Evaluates to 5.

DPLL iterative implementation

Functions and values

Function or value Description

backtrack trail

Full Usage: backtrack trail

Parameters:
    trail : ('a * trailmix) list - The input trail of assigned literals.

Returns: ('a * trailmix) list The literals in the trail starting from the first guessed one.

Removes items from the trail until the most recent decision literal is reached or there are no one left in the trail.

trail : ('a * trailmix) list

The input trail of assigned literals.

Returns: ('a * trailmix) list

The literals in the trail starting from the first guessed one.

Example 

 [
      !>"c", Deduced; 
      !>"b", Deduced; 
      !>"a", Guessed
 
      !>"e", Deduced; 
      !>"d", Guessed
 ]
 |> backtrack
Evaluates to [(`a`, Guessed); (`e`, Deduced); (`d`, Guessed)].

Example 

 [
      !>"c", Deduced; 
      !>"b", Deduced; 
      !>"e", Deduced; 
 ]
 |> backtrack
Evaluates to [].

dpli cls trail

Full Usage: dpli cls trail

Parameters:
    cls : formula<'a> list list - The input clauses.
    trail : (formula<'a> * trailmix) list - The input trail of assigned literals.

Returns: bool true, if the input (based on trail) is satisfiable; otherwise, false.

Tests clauses (propositional) satisfiability with the Davis-Putnam-Loveland-Logemann procedure with an iterative implementation.

cls : formula<'a> list list

The input clauses.

trail : (formula<'a> * trailmix) list

The input trail of assigned literals.

Returns: bool

true, if the input (based on trail) is satisfiable; otherwise, false.

Example 

 dpli !>>[["~p";"q"];["~q"]] [!>"p", Deduced; !>"~q", Deduced]
Evaluates to false.

Example 

 dpli !>>[["~p";"q"];["~q"]] []
Evaluates to true.

dplisat fm

Full Usage: dplisat fm

Parameters:
Returns: bool true, if the input formula is satisfiable: otherwise false.

Tests fm (propositional) satisfiability with the Davis-Putnam-Loveland-Logemann procedure with the iterative implementation.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is satisfiable: otherwise false.

Example 

 dplisat !> "p"
Evaluates to true.

Example 

 dplisat !> "p /\ ~p"
Evaluates to false.

dplitaut fm

Full Usage: dplitaut fm

Parameters:
Returns: bool true, if the input formula is a tautology: otherwise false.

Tests fm (propositional) validity with the Davis-Putnam-Loveland-Logemann procedure with iterative implementation.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is a tautology: otherwise false.

Example 

 dplitaut !> "p"
Evaluates to false.

Example 

 dplitaut (prime 11)
Evaluates to true.

unassigned clauses trail

Full Usage: unassigned clauses trail

Parameters:
    clauses : formula<'a> list list - The input clauses.
    trail : (formula<'a> * 'b) list - The input trail of assigned literals.

Returns: formula<'a> list The list of literals in clauses that are not in trail.

Returns clauses' literals that are not yet assigned in trail.

clauses : formula<'a> list list

The input clauses.

trail : (formula<'a> * 'b) list

The input trail of assigned literals.

Returns: formula<'a> list

The list of literals in clauses that are not in trail.

Example 

 let trail = [!>"p", Deduced;!>"q", Guessed]
 
 unassigned !>> [
      ["p";"c"];["~p";"d"]
      ["q";"~c"];["q";"~d"];["q";"~e"];["~q";"~d"];["~q";"e"]
 ] trail
val trail: (obj * obj) list
Evaluates to [`c`; `d`; `e`].

unit_propagate (cls, trail)

Full Usage: unit_propagate (cls, trail)

Parameters:
    cls : formula<'a> list list - The input clauses.
    trail : (formula<'a> * trailmix) list - The input trail of assigned literals.

Returns: formula<'a> list list * (formula<'a> * trailmix) list The tuple of the clauses and trail updated with the result of unit propagation.

Performs unit propagation modifying internally the clauses cls.

The clauses are updated only from the point of view of the removing of unit clauses' complementary literals, if there are.

cls : formula<'a> list list

The input clauses.

trail : (formula<'a> * trailmix) list

The input trail of assigned literals.

Returns: formula<'a> list list * (formula<'a> * trailmix) list

The tuple of the clauses and trail updated with the result of unit propagation.

Example 

 ((!>> [["p"];["p";"q"]]), [])
 |> unit_propagate
Evaluates to ([[`p`]; [`p`; `q`]], [(`p`, Deduced)]).

Example 

 ((!>> [["p"];["~p";"q"]]), [])
 |> unit_propagate
Evaluates to ([[`p`]; [`q`]], [(`q`, Deduced); (`p`, Deduced)]).

unit_subpropagate (cls, fn, trail)

Full Usage: unit_subpropagate (cls, fn, trail)

Parameters:
    cls : formula<'a> list list - The input clauses.
    fn : func<formula<'a>, unit> - The fpf to process the trail.
    trail : (formula<'a> * trailmix) list - The input trail of assigned literals.

Returns: formula<'a> list list * func<formula<'a>, unit> * (formula<'a> * trailmix) list The triple of the clauses, fpf and trail updated with the result of unit propagation.

Performs unit propagation exhaustively modifying internally the clauses cls and processing the trail into a finite partial function fn for more efficient lookup.

The clauses are updated only from the point of view of the removing of unit clauses' complementary literals, if there are.

cls : formula<'a> list list

The input clauses.

fn : func<formula<'a>, unit>

The fpf to process the trail.

trail : (formula<'a> * trailmix) list

The input trail of assigned literals.

Returns: formula<'a> list list * func<formula<'a>, unit> * (formula<'a> * trailmix) list

The triple of the clauses, fpf and trail updated with the result of unit propagation.

Example 

 ((!>> [["p"];["p";"q"]]), undefined,[])
 |> unit_subpropagate 
 |> fun (cls,fpf,trail) -> (cls,fpf |> graph,trail)
val cls: obj
val fpf: obj
val trail: obj
Evaluates to ([[`p`]; [`p`; `q`]], [(`p`, ())], [(`p`, Deduced)]).

Example 

 ((!>> [["p"];["~p";"q"]]), undefined,[])
 |> unit_subpropagate 
 |> fun (cls,fpf,trail) -> (cls,fpf |> graph,trail)
val cls: obj
val fpf: obj
val trail: obj
Evaluates to ([[`p`]; [`q`]], [(`p`, ()); (`q`, ())], [(`q`, Deduced); (`p`, Deduced)]).

DPLL with backjumping and learning

Functions and values

Function or value Description

backjump cls p trail

Full Usage: backjump cls p trail

Parameters:
    cls : formula<'a> list list - The input clauses.
    p : formula<'a> - The literal to check.
    trail : (formula<'a> * trailmix) list - The input trail of assigned literals.

Returns: (formula<'a> * trailmix) list true, if the input formula is a tautology: otherwise false.

Goes back through the trail as far as possible while p still leads to a conflict.

cls : formula<'a> list list

The input clauses.

p : formula<'a>

The literal to check.

trail : (formula<'a> * trailmix) list

The input trail of assigned literals.

Returns: (formula<'a> * trailmix) list

true, if the input formula is a tautology: otherwise false.

Example 

 backjump !>>[["~p";"q"];["~q"]] !>"a"
 [
     !>"c", Deduced; 
     !>"b", Deduced; 
     !>"~a", Deduced
     !>"e", Guessed; 
     !>"p", Deduced; 
     !>"d", Guessed
 ]
Evaluates to [(`p`, Deduced); (`d`, Guessed)].

dplb cls trail

Full Usage: dplb cls trail

Parameters:
    cls : formula<'a> list list - The input clauses.
    trail : (formula<'a> * trailmix) list - The input trail of assigned literals.

Returns: bool true, if the input (based on trail) is satisfiable; otherwise, false.

Tests clauses (propositional) satisfiability with the Davis-Putnam-Loveland-Logemann procedure with an iterative implementation and backjumping and learning optimizations.

cls : formula<'a> list list

The input clauses.

trail : (formula<'a> * trailmix) list

The input trail of assigned literals.

Returns: bool

true, if the input (based on trail) is satisfiable; otherwise, false.

Example 

 dplb !>>[["~p";"q"];["~q"]] [!>"p", Deduced; !>"~q", Deduced]
Evaluates to false.

Example 

 dplb !>>[["~p";"q"];["~q"]] []
Evaluates to true.

dplbsat fm

Full Usage: dplbsat fm

Parameters:
Returns: bool true, if the input formula is satisfiable: otherwise false.

Tests fm (propositional) satisfiability with the Davis-Putnam-Loveland-Logemann procedure with the iterative implementation and backjumping and learning optimizations.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is satisfiable: otherwise false.

Example 

 dplbsat !> "p"
Evaluates to true.

Example 

 dplbsat !> "p /\ ~p"
Evaluates to false.

dplbtaut fm

Full Usage: dplbtaut fm

Parameters:
Returns: bool true, if the input formula is a tautology: otherwise false.

Tests fm (propositional) validity with the Davis-Putnam-Loveland-Logemann procedure with iterative implementation and backjumping and learning optimizations.

fm : formula<prop>

The input formula.

Returns: bool

true, if the input formula is a tautology: otherwise false.

Example 

 dplbtaut !> "p"
Evaluates to false.

Example 

 dplbtaut (prime 11)
Evaluates to true.

Example

dplbtaut is 4X more faster than dplitaut: 

 time dplbtaut (prime 101)
 // Evaluates to:
 // CPU time (user): 36.981689
 // val it: bool = true
 
 time dplitaut (prime 101)
 // Evaluates to:
 // CPU time (user): 130.045742
 // val it: bool = true