diff --git a/R/mkCactus.R b/R/mkCactus.R index 1666054..a90a299 100755 --- a/R/mkCactus.R +++ b/R/mkCactus.R @@ -1,11 +1,13 @@ #!/usr/bin/env Rscript # generate a cactus plot (png and pdf) from CVS files -# USAGE: mkCactus runs [subtitle] [nproblems] -# where runs is a filename that contains a list of CSV filenames which are generated by sat-benchmark +# USAGE: mkCactus runs [nproblems] [subtitle] +# where runs is a filename that contains a list of CSV filenames which are generated by satbenchmark2csv library("ggplot2") -version = "0.11.0" +version = "0.11.1 for SC2018" -getData = function (t, p, c) { +solved = 0 + +getData = function (t, p, cut) { df1 <- read.csv(as.character(t[[1]]), header=T, sep=",", comment="#") if (nrow(df1) == 0) { return(NULL) } df2 <- data.frame(solver=df1[["solver"]], @@ -17,33 +19,35 @@ getData = function (t, p, c) { } else { df2[["valid"]] <- numeric(nrow(df2)) } - if (0 < c) { - df2 <- df2[1:c,] + if (0 < cut) { + df2 <- df2[1:min(nrow(df2),cut),] } df2 <- df2[order(df2[["time"]]),] # sort by time if (p && t[[2]] != "") { df2[["solver"]] = sub("^ +", "", as.character(t[[2]])) } df2[["num"]] <- 1:nrow(df2) # reassign rownumbers + thr <- max(df2[["time"]]) + solved <<- max(solved, nrow(subset(df2, time < 0.8 * thr))) df2 } -graph = function (d, subt) { +graph = function (d, subt, cut) { g <- ggplot(d, aes(num, time, color=solver, size=solver, alpha=solver)) g <- g + geom_point(size=0.5) g <- g + geom_line(data=d) + g <- g + geom_point(data=subset(d, valid==3),size=2,shape=4) g <- g + scale_size_manual(values=rep(0.6, times=nrow(d))) g <- g + scale_alpha_manual(values=rep(1.0, times=nrow(d))) - g <- g + geom_point(data=subset(d, valid==3),size=2,shape=4) # g <- g + scale_size_manual(values=c(0.7,0.7,0.7,0.7,0.3,0.3,0.3)) -- by aes(size=solver) # g <- g + scale_alpha_manual(values=c(1.0,1.0,1.0,1.0,0.5,0.5,0.5)) -- by aes(alpha=solver) - g <- g + theme(legend.position = c(0.85,0.2), legend.justification = c(1,0)) - g <- g + scale_x_continuous(limits=c(0,350), breaks=seq(0,350,10), expand=c(0,4)) - g <- g + scale_y_continuous(limits=c(0, max(d$time)), breaks=seq(0,max(d$time),100), expand=c(0,4)) - # g <- g + scale_y_continuous(limits=c(0,410) ,breaks=seq(0,410,100)) - g <- g + labs(title="Cactus plot on SAT-Race 2017 Main track (with a short timeout)", subtitle=subt, - x="#solved", y="execution time [sec]") - g <- g + annotate("text", x=0.75*max(d$num), y=10, - label=paste(format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S"), " ", "drawn with mkCactus.R (ver. ", version, ")", sep=""), - color="darkgray", size=2.6) + maxx = 400 + g <- g + theme(legend.position = c(0.95,0.05), legend.justification = c(1,0)) + g <- g + scale_y_continuous(limits=c(0,max(d$time)), breaks=seq(0,max(d$time),100), expand=c(0.01,4)) + g <- g + scale_x_continuous(limits=c(0,maxx), breaks=seq(00,maxx,10), expand=c(0,2)) + #g <- g + annotate("text", x=100, y=50, + # label=paste(format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S"), " ", "drawn with mkCactusL.R (ver. ", version, ")", sep=""), + # color="darkgray", size=2.6) + g <- g + labs(title="Cactus plot on SAT Competition 2018 Benchmark Main track", subtitle=subt, + x=if (0 < cut) paste("#solved out of ", cut, sep="") else "#solved", y="CPU time [sec]") print(g) } @@ -51,29 +55,28 @@ graph = function (d, subt) { merged <- list() args <- commandArgs(trailingOnly=TRUE) ts <-format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S") - subt <- paste(" - ", ts, " drawn with mkCactus.R (ver. ", version, ")", sep="") - if (0 < length(args)){ + + if (1 <= length(args)){ exps <- args[1] name <- gsub("\\.[^.]+$", "", exps) - targetPDF <- paste("cactus-", name, ".pdf", sep="") - targetPNG <- paste("cactus-", name, ".png", sep="") - if (1 < length(args) && args[2] != "") { subt <- args[2] } + targetPDF <- paste("Cactus-", name, ".pdf", sep="") + targetPNG <- paste("Cactus-", name, ".png", sep="") } else { exps <- "runs" name <- "runs" - targetPDF <- "cactus-SC17main.pdf" - targetPNG <- "cactus-SC17main.png" + targetPDF <- "Cactus-SC18main.pdf" + targetPNG <- "Cactus-SC18main.png" } cut <- -1 - if (2 < length(args)) { - cut <- as.integer(args[3]) - } - runs <- read.csv(exps, comment="#", sep=",", header=F) - withTag <- 1 < ncol(runs) - for (i in seq(nrow(runs))) { merged = rbind(merged, getData(runs[i,], withTag, cut)); } - + if (2 <= length(args)) { cut <- as.integer(args[2] ) } + subt <- paste(exps, " -- ", ts, " drawn with mkCactus.R (ver. ", version, ")", sep="") + spec <- " - CPU: Intel Core i5-8500B@3.0GHz, Mem: 32GB, SSD, NixOS on Darwin" + #runs <- read.csv(exps, comment="#", sep=",", header=F) + #withTag <- 1 < ncol(runs) + #for (i in seq(nrow(runs))) { merged = rbind(merged, getData(runs[i,], withTag, cut)); } + merged = rbind(merged, getData(exps, FALSE, 5000)); cairo_pdf(filename=targetPDF, width=10, height=6, antialias="subpixel", onefile=TRUE) - graph(merged, subt) + graph(merged, paste(subt, spec, sep="\n"), cut) ggsave(filename=targetPDF, width=10, height=6, scale=1.0, dpi=400) - ggsave(filename=targetPNG, width=10, height=6, scale=1.0, dpi=200) + # ggsave(filename=targetPNG, width=10, height=6, scale=1.0, dpi=400) })() diff --git a/R/mkCactusL2019.R b/R/mkCactusL2019.R new file mode 100755 index 0000000..4b9b2e0 --- /dev/null +++ b/R/mkCactusL2019.R @@ -0,0 +1,84 @@ +#!/usr/bin/env Rscript +# generate a cactus plot (png and pdf) from CVS files +# USAGE: mkCactusL runs [nproblems] [subtitle] +# where runs is a filename that contains a list of CSV filenames which are generated by satbenchmark2csv +library("ggplot2") +version = "0.13 for SR2019" + +solved = 0 + +getData = function (t, p, cut) { + df1 <- read.csv(as.character(t[[1]]), header=T, sep=",", comment="#") + if (nrow(df1) == 0) { return(NULL) } + df2 <- data.frame(solver=df1[["solver"]], + num=df1[["num"]], + target=df1[["target"]], + time=df1[["time"]]) + if (ncol(df1) == 5) { + df2[["valid"]] <- df1[["valid"]] + } else { + df2[["valid"]] <- numeric(nrow(df2)) + } + if (0 < cut) { + df2 <- df2[1:min(nrow(df2),cut),] + } + df2 <- df2[order(df2[["time"]]),] # sort by time + if (p && t[[2]] != "") { df2[["solver"]] = sub("^ +", "", as.character(t[[2]])) } + df2[["num"]] <- 1:nrow(df2) # reassign rownumbers + thr <- max(df2[["time"]]) + solved <<- max(solved, nrow(subset(df2, time < 0.8 * thr))) + df2 +} + +graph = function (d, subt, cut) { + g <- ggplot(d, aes(num, time, color=solver, size=solver, alpha=solver)) + g <- g + geom_point(size=0.5) + g <- g + geom_line(data=d) + g <- g + geom_point(data=subset(d, valid==3),size=2,shape=4) + g <- g + scale_size_manual(values=rep(0.6, times=nrow(d))) + g <- g + scale_alpha_manual(values=rep(1.0, times=nrow(d))) + # g <- g + scale_size_manual(values=c(0.7,0.7,0.7,0.7,0.3,0.3,0.3)) -- by aes(size=solver) + # g <- g + scale_alpha_manual(values=c(1.0,1.0,1.0,1.0,0.5,0.5,0.5)) -- by aes(alpha=solver) + maxx = 400 + g <- g + theme(legend.position = c(0.95,0.05), legend.justification = c(1,0)) + g <- g + scale_y_continuous(limits=c(0,max(d$time)), breaks=seq(0,max(d$time),100), expand=c(0.01,4)) + g <- g + scale_x_continuous(limits=c(0,maxx), breaks=seq(00,maxx,10), expand=c(0,2)) + #g <- g + annotate("text", x=100, y=50, + # label=paste(format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S"), " ", "drawn with mkCactusL.R (ver. ", version, ")", sep=""), + # color="darkgray", size=2.6) + g <- g + labs(title="Cactus plot on SAT RACE 2019 Benchmark Main track", subtitle=subt, + x=if (0 < cut) paste("#solved out of ", cut, sep="") else "#solved", y="CPU time [sec]") + print(g) +} + +(function() { + merged <- list() + args <- commandArgs(trailingOnly=TRUE) + ts <-format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S") + + if (1 <= length(args)){ + exps <- args[1] + name <- gsub("\\.[^.]+$", "", exps) + targetPDF <- paste("CactusL-", name, ".pdf", sep="") + targetPNG <- paste("CactusL-", name, ".png", sep="") + } else { + exps <- "runs" + name <- "runs" + targetPDF <- "CactusL-SC18main.pdf" + targetPNG <- "CactusL-SC18main.png" + } + cut <- -1 + if (2 <= length(args)) { cut <- as.integer(args[2] ) } + subt <- paste(exps, " -- ", ts, " drawn with mkCactusL.R (ver. ", version, ")", sep="") + spec <- " - CPU: Intel Core i5-8500B@3.0GHz, Mem: 32GB, SDD, NixOS on Darwin" + # if (3 <= length(args) && args[3] != "") { subt <- args[3] } + runs <- read.csv(exps, comment="#", sep=",", header=F) + withTag <- 1 < ncol(runs) + for (i in seq(nrow(runs))) { merged = rbind(merged, getData(runs[i,], withTag, cut)); } + + # png(filename=targetPNG, width=1600, height=1000) + # cairo_pdf(filename=targetPDF, width=10, height=6, antialias="subpixel", onefile=TRUE) + graph(merged, paste(subt, spec, sep="\n"), cut) + ggsave(filename=targetPDF, width=10, height=6, scale=1.0, dpi=400) + # ggsave(filename=targetPNG, width=10, height=6, scale=1.0, dpi=400) +})()