OptimalBranchingCore

apply_branch(problem::AbstractProblem, clause::Clause, vertices::Vector)::Tuple

Create a branch from the given clause applied to the specified vertices.

Arguments

• problem: The problem instance.
• clause: The clause that containing the information about how to fix the values of the variables.
• vertices: A vector of vertices to be considered for the branch.

Returns

• AbstractProblem: A new instance of AbstractProblem with reduced size.

branch_and_reduce(problem::AbstractProblem, config::BranchingStrategy; reducer::AbstractReducer=NoReducer(), result_type=Int, show_progress=false)

Branch the given problem using the specified solver configuration.

Arguments

• problem: The problem instance to solve.
• config: The configuration for the solver, which is a BranchingStrategy instance.

Keyword Arguments

• reducer::AbstractReducer=NoReducer(): The reducer to reduce the problem size.
• result_type::Type{TR}: The type of the result that the solver will produce.

Returns

The resulting value, which may have different type depending on the result_type.

branching_table(problem::AbstractProblem, table_solver::AbstractTableSolver, variables::Vector{Int})

Obtains the branching table for a given problem using a specified table solver.

Arguments

• problem: The problem instance.
• table_solver: The table solver, which is a subtype of AbstractTableSolver.
• variables: A vector of indices of the variables to be considered for the branching table.

Returns

A branching table, which is a BranchingTable object.

candidate_clauses(tbl::BranchingTable{INT}) where {INT}

Generates candidate clauses from a branching table.

Arguments

• tbl::BranchingTable{INT}: The branching table containing bit strings.

Returns

• Vector{Clause{INT}}: A vector of Clause objects generated from the branching table.

complexity_bv(branching_vector::Vector)::Float64

Calculates the complexity that associated with the provided branching vector by solving the equation:

\[γ^0 = \sum_{δρ \in \text{branching_vector}} γ^{-δρ}\]

Arguments

• branching_vector: a vector of problem size reductions in the branches.

Returns

• Float64: The computed γ value.

covered_by(t::BranchingTable, dnf::DNF)

Check if the branching table t is covered by the logic expression dnf. Returns true if there exists at least one bitstring in each group of t that satisfies dnf, false otherwise.

covered_by(a::Integer, clause_or_dnf)

Check if a is covered by the logic expression clause_or_dnf.

Arguments

• a: A bit string.
• clause_or_dnf: Logic expression, which can be a Clause object or a DNF object.

Returns

true if a satisfies clause_or_dnf, false otherwise.

is_false_literal(c::Clause)

Check if the clause is a false literal.

is_true_literal(c::Clause)

Check if the clause is a true literal.

literals(c::Clause)

Return all literals in the clause.

measure(problem::AbstractProblem, measure::AbstractMeasure)::Number

Calculate the size of the problem, reducing which serves as the guiding principle for the branching strategy.

Arguments

• problem: The problem instance.
• measure: The measure of the problem size.

Returns

A real number representing the problem size.

minimize_γ(table::BranchingTable, candidates::Vector{Clause}, Δρ::Vector, solver)

Finds the optimal cover based on the provided vector of problem size reduction. This function implements a cover selection algorithm using an iterative process. It utilizes an integer programming solver to optimize the selection of sub-covers based on their complexity.

Arguments

• table::BranchingTable: A branching table containing clauses that need to be covered, a table entry is covered by a clause if one of its bit strings satisfies the clause. Please refer to covered_by for more details.
• candidates::Vector{Clause}: A vector of candidate clauses to form the branching rule (in the form of DNF).
• Δρ::Vector: A vector of problem size reduction for each candidate clause.
• solver: The solver to be used. It can be an instance of LPSolver or IPSolver.

Returns

A tuple of two elements: (indices of selected subsets, γ)

optimal_branching_rule(table::BranchingTable, variables::Vector, problem::AbstractProblem, measure::AbstractMeasure, solver::AbstractSetCoverSolver)::OptimalBranchingResult

Generate an optimal branching rule from a given branching table.

Arguments

• table: A BranchingTable instance containing candidate clauses.
• variables: A vector of variables to perform the branching.
• problem: The problem instance being solved.
• measure: The measure used for evaluating the problem size reduction in the branches.
• solver: The solver used for the weighted minimum set cover problem, which can be either LPSolver or IPSolver.

Returns

A OptimalBranchingResult object representing the optimal branching rule.

reduce_problem(::Type{R}, problem::AbstractProblem, reducer::AbstractReducer) where R

Reduces the problem size directly, e.g. by graph rewriting. It is a crucial step in the reduce and branch strategy.

Arguments

• R: The element type used for computing the size of solution. The should have an additive commutative monoid structure.
• problem: The problem instance.
• reducer: The reducer.

Returns

A tuple of two values:

• AbstractProblem: A new instance of AbstractProblem with reduced size.
• Number: The local gain of the reduction, which will be added to the global gain.

select_variables(problem::AbstractProblem, measure::AbstractMeasure, selector::AbstractSelector)::Vector{Int}

Selects a branching strategy for a AbstractProblem instance.

Arguments

• problem: The problem instance.
• measure: The measure of the problem size.
• selector: The variables selection strategy, which is a subtype of AbstractSelector.

Returns

A vector of indices of the selected variables.

test_rule(table::BranchingTable, predicted::DNF, problem::AbstractProblem, m::AbstractMeasure, variables::Vector)

Test the validity and complexity of a rule.

Arguments

• table::BranchingTable: The branching table.
• predicted::DNF: The logic expression in DNF.
• problem::AbstractProblem: The problem.
• m::AbstractMeasure: The measure.
• variables::Vector: The variables.

Returns

• is_valid::Bool: Whether the rule is valid.
• gamma::Float64: The complexity of the rule.

weighted_minimum_set_cover(solver, weights::AbstractVector, subsets::Vector{Vector{Int}}, num_items::Int)

Solves the weighted minimum set cover problem.

Arguments

• solver: The solver to be used. It can be an instance of LPSolver or IPSolver.
• weights::AbstractVector: The weights of the subsets.
• subsets::Vector{Vector{Int}}: A vector of subsets.
• num_items::Int: The number of elements to cover.

Returns

A vector of indices of selected subsets.

AbstractMeasure

The base type for the measure of the problem size in terms of computational hardness. Some widely used measures include the number of variables, the vertices with connectivity of at least 3, etc.

AbstractProblem

The problem type that can be used in the optimal branching framework.

AbstractReducer

An abstract type representing a reducer in the context of branching problems. This serves as a base type for all specific reducer implementations.

AbstractSelector

An abstract type for the strategy of selecting a subset of variables to be branched.

AbstractSetCoverSolver

An abstract type for the strategy of solving the set covering problem.

AbstractTableSolver

An abstract type for the strategy of obtaining the branching table.

BranchingStrategy
BranchingStrategy(; kwargs...)

A struct representing the configuration for a solver, including the reducer and branching strategy.

Fields

• table_solver::AbstractTableSolver: The solver to resolve the relevant bit strings and generate a branching table.
• set_cover_solver::AbstractSetCoverSolver = IPSolver(): The solver to solve the set covering problem.
• selector::AbstractSelector: The selector to select the next branching variable or decision.
• m::AbstractMeasure: The measure to evaluate the performance of the branching strategy.

BranchingTable{INT <: Integer}

A list of groupped bitstrings, which is used for designing the branching rule. A valid branching rule, which is represented by a logic expression in Disjunctive Normal Form (DNF), should cover at least one bitstring from each group, where by cover, we mean there exists at least one bitstring in the group that satisfies the logic expression. Please check covered_by for more details.

Fields

• bit_length::Int: The length of the bit string.
• table::Vector{Vector{INT}}: The list of groupped bitstrings used for branching, where each group is a vector of bitstrings. The bitstrings uses INT type to store the bitstring.

CandidateClause{INT <: Integer}

A candidate clause is a clause containing the formation related to how it can cover the items in the branching table.

Fields

• covered_items::Set{Int}: The items in the branching table that are covered by the clause.
• clause::Clause{INT}: The clause itself.

Clause{INT <: Integer}

A Clause is conjunction of literals, which is specified by a pair of bit strings. The type parameter INT is the integer type for storing the bit strings.

Fields

• mask: A bit string that indicates the variables involved in the clause.
• val: A bit string that indicates the positive literals in the clause.

Examples

To check if a bit string satisfies a clause, use OptimalBranchingCore.covered_by.

julia> using OptimalBranchingCore

julia> clause = Clause(0b1110, 0b1010)
Clause{UInt8}: #2 ∧ ¬#3 ∧ #4

julia> OptimalBranchingCore.covered_by(0b1110, clause)
false

julia> OptimalBranchingCore.covered_by(0b1010, clause)
true

DNF{INT}

A data structure representing a logic expression in Disjunctive Normal Form (DNF), which is a disjunction of one or more conjunctions of literals. In OptimalBranchingCore, a DNF is used to represent the branching rule.

Fields

• clauses::Vector{Clause{INT}}: A vector of Clause objects.

IPSolver <: AbstractSetCoverSolver
IPSolver(; optimizer = HiGHS.Optimizer, max_itr::Int = 20, γ0::Float64 = 2.0, verbose::Bool = false)

An integer programming solver for set covering problems.

Fields

• optimizer: The optimizer to be used.
• max_itr::Int: The maximum number of iterations to be performed.
• γ0::Float64: The initial γ value.
• verbose::Bool: Whether to print the solver's output.

LPSolver <: AbstractSetCoverSolver
LPSolver(; optimizer = HiGHS.Optimizer, max_itr::Int = 20, γ0::Float64 = 2.0, verbose::Bool = false)

A linear programming solver for set covering problems.

Fields

• optimizer: The optimizer to be used.
• max_itr::Int: The maximum number of iterations to be performed.
• γ0::Float64: The initial γ value.
• verbose::Bool: Whether to print the solver's output.

MaxSize

A struct representing the maximum size of a result. (actually a tropical int)

Fields

• size: The maximum size value.

Constructors

• MaxSize(size): Creates a MaxSize instance with the specified size.

struct MaxSizeBranchCount

Reture both the max size of the results and number of branches.

Fields

• size: The max size of the results.
• count::Int: The number of branches of that size.

Constructors

• MaxSizeBranchCount(size): Creates a MaxSizeBranchCount with the given size and initializes the count to 1.
• MaxSizeBranchCount(size, count::Int): Creates a MaxSizeBranchCount with the specified size and count.

struct MockTableSolver <: AbstractTableSolver

The MockTableSolver randomly generates a branching table with a given number of rows. Each row must have at least one variable to be covered by the branching rule.

Fields

• n::Int: The number of rows in the branching table.
• p::Float64 = 0.0: The probability of generating more than one variables in a row, following the Poisson distribution.

NumOfVariables

A struct representing a measure that counts the number of variables in a problem. Each variable is counted as 1.

OptimalBranchingResult{INT <: Integer}

The result type for the optimal branching rule.

Fields

• optimal_rule::DNF{INT}: The optimal branching rule.
• branching_vector::Vector{T<:Real}: The branching vector that records the size reduction in each subproblem.
• γ::Float64: The optimal γ value (the complexity of the branching rule).

struct RandomSelector <: AbstractSelector

The RandomSelector struct represents a strategy for selecting a subset of variables randomly.

Fields

• n::Int: The number of variables to select.