DM841 - PseudoBoolean Satisfiability and Optimization: Benchmarks

Best known results on the bechmark instances

The table below reports the best known results attained by complete solvers on the instances given for the assignment, namely those belonging to the categories: DEC-SMALLINT-LIN,OPT-SMALLINT-LIN. The field Answer concerns the satisfiability of the instances. Its labels have the following meaning:

• Decision problems:
  • SAT: proved satisfiable
    
  • UNKNOWN TO: unknown at timeout
• Optimization problems
  • OPT: proved optimal
    
  • SAT TO: proved satisfiable but not proven optimal at timeout.

Code

library(tibble)
library(dplyr)
library(stringr)

DATA <- read.table("./PB16competition.txt", fill = TRUE, sep = "|", dec = ".", head = TRUE, strip.white = TRUE)
DATA <- as_tibble(DATA) |> filter(Category %in% c("DEC-SMALLINT-LIN", "OPT-SMALLINT-LIN"))
DATA <- DATA |> mutate(across(Instance.name, basename))
DATA <- DATA |> mutate(Instance.name = str_remove(Instance.name, ".opb"))
DATA <- DATA |> mutate(across(c(Category, Instance.name, Checked.answer), factor))
DATA$Checked.answer <- factor(DATA$Checked.answer,
    levels = c("SAT", "UNSAT", "SAT TO", "SAT MO", "OPT", "UNKNOWN", "UNKNOWN TO", "UNKNOWN MO", "UNKNOWN EXCODE", "SIGNAL", "ERR NOCERT")
)
LONG <- DATA %>%
    group_by(Category, Instance.name) %>%
    summarize(
        Answer = first(Checked.answer),
        ObjFun = min(Objective.function[Checked.answer == Answer]),
        .groups = "keep"
    )

instances <- read.table("./instances.txt", fill = TRUE, head = FALSE)
# instances <- basename(list.files("../PseudoBoolean_v3.0/data/",recursive=TRUE))
instances$V1 <- sub(".opb.bz2", "", basename(instances$V1))

# DATA <- DATA |> filter(Instance.name %in% instances)
FINAL <- left_join(instances, LONG, by = c("V1" = "Instance.name"))
colnames(FINAL) <- c("Instance.name", "Vars", "Cls", "Category", "Answer", "ObjFun")
FINAL |> group_by(Category) |> summarize(across(Instance.name,n_distinct))

Code

# require(tidyr)
require(DT)
datatable(select(FINAL, Category, Instance.name, Vars, Cls, Answer, ObjFun),
    rownames = FALSE,
    # caption = "Benchmarks",
    options = list(
        order = list(list(0, "desc"), list(2, "asc"), list(3, "asc")),
        dom = "ft",
        paging = FALSE,
        pageLength = length(unique(FINAL$Instance.name))
    )
) %>%
    formatStyle(
        columns = 0:6,
        fontFamily = "monospace",
        fontSize = "0.7rem"
    )

Code

# https://search.r-project.org/CRAN/refmans/DT/html/formatCurrency.html