GitHub

Metric Heap

The necessary components for the search strategies allowing for a ``smarter'' way of expanding the tableau tree structure, aiming at finding a fully expanded open branch (resp. closing all branches) in the fastest way possible.

A MetricHeap is basically a heap parametrized over a metric, i.e., a function which extracts some information about a tableau branch, therefore containing in each node a tableau branch and the relative value for the metric, and which is ordered as a min heap over this metric value.

Note that all MetricHeaps are ordered from the smaller value to the greatest, and can contain negative values (all Ints)

Helpers to clear the heaps (e.g., to deallocate memory removing already expanded non-leaf nodes and closed nodes) are also provided.

SoleReasoners.MetricHeapNode — Type
struct MetricHeapNode{T<:AbstractTableau}
    metricvalue::Int
    tableau::T
end

The atomic element of a MetricHeap, it contains a tableau branch and a value for the metric associated with the MetricHeap it is contained in.

source
Base.show — Method
Base.show(io::IO, metricheapnode::MetricHeapNode)

A MetricHeapNode is represented as a tuple (metricvalue, tableau).

source
SoleReasoners.MetricHeapOrdering — Type
struct MetricHeapOrdering <: Base.Order.Ordering end

Definition of a new ordering for the heaps treating them as min heaps ordered on the metric value.

source
Base.Order.lt — Method
lt(_::MetricHeapOrdering, a::MetricHeapNode, b::MetricHeapNode)

Definition of the lt function for the new ordering.

source
SoleReasoners.MetricHeap — Type
struct MetricHeap
    heap::BinaryHeap{MetricHeapNode}
    metric::Function
end

A MetricHeap is basically a heap parametrized over a metric, i.e., a function which extracts some information about a tableau branch, therefore containing in each node a tableau branch and the relative value for the metric, and which is ordered as a min heap over this metric value.

Note that all MetricHeaps are ordered from the smaller value to the greatest, and can contain negative values (all Ints).

source
Base.push! — Method
push!(metricheap::MetricHeap, metricheapnode::MetricHeapNode)

Push new metricheapnode to a MetricHeap.

source
Base.push! — Method
push!(metricheap::MetricHeap, tableau::T) where {T<:AbstractTableau}

Push new tableau to a MetricHeap.

source
Base.push! — Method
push!(
    metricheaps::Vector{MetricHeap},
    tableau::T
) where {
    T<:AbstractTableau
}

Push new tableau to each metric heap.

source
Base.pop! — Method
pop!(metricheap::MetricHeap)

Pop head of a MetricHeap and return the tableau associated with it.

source
Base.isempty — Method
isempty(metricheap::MetricHeap)

Returns true if the MetricHeap is empty, false otherwise.

source
SoleReasoners.cleanheap! — Method
cleanheaps!(metricheaps::Vector{MetricHeap})

Function to clean the MetricHeap removing all the nodes that have already been expanded that are not leaves (as the latters correspond to an open fully expanded branch, i.e., a satisfiable branch) or closed.

source
SoleReasoners.cleanheaps! — Method
cleanheaps!(metricheaps::Vector{MetricHeap})

Function to clean the MetricHeaps removing from all heaps all the nodes that have already been expanded that are not leaves (as the latters correspond to an open fully expanded branch, i.e., a satisfiable branch) or closed.

source
Base.show — Method
Base.show(io::IO, metricheap::MetricHeap)

A MetricHeap is represented by its metric and its heap.

source

Metrics

Various metrics that can be used to create MetricHeaps to ease the search of the expansion node on any tableau, such as randombranch assigning a random weight to each node when pushing it into the heaps, distancefromroot assignign to each node its distance from the root giving priority to smaller distances (i.e., breadth-first search), or inversedistancefromroot, giving priority to larger distances (i.e., a sort of depth-first search).

metrics using specific fields of tableaux structures (e.g., formula for formulalength for PropositionalTableau) can be found in the metric.jl file of each subdirectory.

SoleReasoners.randombranch — Method
randombranch(_::T) where {T<:AbstractTableau}

metric assigning a random weight to each node when pushing it into the heaps. It leverages Xoshiro as pseudo-random generator with random seed.

For deterministic execution (i.e., experimental environments), it is advised to reimplement a similar custom function specifying a seed for the generator, such as: rng = Xoshiro(42) customrandombranch(_::T) where {T<:AbstractTableau} = rand(rng, Int) Note that the rng is defined outside of the function body; otherwise, it produces always the same value.

source
SoleReasoners.distancefromroot — Method
distancefromroot(t::T) where {T<:AbstractTableau}

metric assignign to each node its distance from the root giving priority to smaller distances (somewhat similar to breadth-first search).

source
SoleReasoners.inversedistancefromroot — Method
inversedistancefromroot(t::T) where {T<:AbstractTableau}

metric assignign to each node its distance from the root giving priority to larger distances (somewhat similar to deep-first search).

source
SoleReasoners.formulaheight — Method
formulaheight(t::T) where {T<:ManyValuedMultiModalTableau}

metric assignign to each node the height of its formula in the assertion, or 0 in case the assertion is of the type {<:Truth,<:Truth}.

source

Choosenode

Various policies to choose which node to actually expand given the heads of the heaps (i.e., using a roundrobin! policy, choosing each time the head of a different heap in a sequential way, or mostvoted!, choosing the node that is the head of most heaps).

Note that all policies are are signed as !, as they change the structures (``popping'' elements from the heaps).

SoleReasoners.roundrobin! — Method
roundrobin!(metricheaps::Vector{MetricHeap}, cycle::Int)

Choose a node using the provided MetricHeaps, alternating between them at each cycle.

The result can either be nothing, in case all heaps are empty and therefore the tableau closed, or a node; an expanded node can only be returned if it is a leaf and in that case it represents a satisfiable branch for the tableau (i.e., a fully expanded open branch without contraddictions).

This is the default and suggested policy, as it prevents starvation.

source
SoleReasoners.mostvoted! — Method
mostvoted!(metricheaps::Vector{MetricHeap}, args...)

Choose a leaf using the provided MetricHeaps, returning the leaf which is the head of most of the heaps. In case

To prevent starvation, use roundrobin! instead.

source