DM841 - PseudoBoolean Satisfiability and Optimization: Benchmarks
Author
Marco Chiarandini
Published
November 28, 2023
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))