Significant Performance Difference Between Static Library and Dynamic Library with IPAMIR interface

[gaspard-quenard]

Hello,

First of all, thank you for your amazing solver :)

Description

I have followed the instructions in the README to compile both the static and dynamic libraries of uwrmaxsat. While both libraries compile and function correctly, there is a significant performance discrepancy when using the dynamic library with the ipamir interface. For the problem satellite02ac.wcsp.wcnf, the static library find an optimal solution in approximately 1.2 seconds while using the dynamic library with the ipamir interface took around 340 seconds to find an optimal solution. This time difference only occur when there are soft literals: if I remove all the weighted literals in the file satellite02ac.wcsp.wcnf, the dynamic library is as quick as the static library. So it seem the problem only occurs when I use the function ipamir_add_soft_lit.

Here is an example code to reproduce my results using the ipamir interface:

#include <iostream>
#include "ipamir.h" 
#include <ctime>    
#include <string.h>


/**
 * Read a WCNF file and solve it using IPAMIR library.
*/
void run_wcnf_file_with_ipamir(const char* filename) {
    // Initialize the solver
    void* solver = ipamir_init();
    if (!solver) {
        std::cerr << "Failed to initialize IPAMIR solver." << std::endl;
        return;
    }

    // Open the WCNF file
    FILE* file = fopen(filename, "r");
    if (!file) {
        std::cerr << "Failed to open file: " << filename << std::endl;
        ipamir_release(solver);
        return;
    }

    char line[256];

    printf("Reading file %s\n", filename);

    // Read the file line by line
    while (fgets(line, sizeof(line), file)) {
        // Skip comments and problem line
        if (line[0] == 'c' || line[0] == 'p') {
            continue;
        }

        // Read the weight of the clause
        int weight;
        if (sscanf(line, "%d", &weight) != 1) {
            std::cerr << "Failed to read weight." << std::endl;
            fclose(file);
            ipamir_release(solver);
            return;
        }

        // Tokenize the rest of the line to read literals
        char* token = strtok(line, " ");
        token = strtok(NULL, " "); // Skip the weight
        if (weight == 156116) {
            // Process hard clause
            while (token != NULL) {
                int literal;
                if (sscanf(token, "%d", &literal) != 1) {
                    std::cerr << "Failed to read literal." << std::endl;
                    fclose(file);
                    ipamir_release(solver);
                    return;
                }
                ipamir_add_hard(solver, literal);
                
                token = strtok(NULL, " ");
            }
        } else {
            // Process soft clause
            int num_literals = 0;
            while (token != NULL) {
                int literal;
                if (sscanf(token, "%d", &literal) != 1) {
                    std::cerr << "Failed to read literal." << std::endl;
                    fclose(file);
                    ipamir_release(solver);
                    return;
                }

                if (literal != 0) {
                    ipamir_add_soft_lit(solver, -literal, weight);
                    num_literals++;
                }
                token = strtok(NULL, " ");
            }
            if (num_literals != 1) {
                std::cerr << "Soft clause should have only one literal." << std::endl;
                fclose(file);
                ipamir_release(solver);
                return;
            }
        }
    }

    fclose(file);

    // Solve the formula and measure the time taken
    clock_t start = clock();
    std::cout << "Launching the solver..." << std::endl;
    int result = ipamir_solve(solver);
    clock_t end = clock();
    double elapsed_time = static_cast<double>(end - start) / CLOCKS_PER_SEC;
    std::cout << "Time elapsed: " << elapsed_time << " seconds" << std::endl;

    // Output the result
    if (result == 30) {
        std::cout << "The formula is satisfiable!" << std::endl;
        std::cout << "Objective value: " << ipamir_val_obj(solver) << std::endl;
    } else if (result == 20) {
        std::cout << "The formula is not satisfiable." << std::endl;
    } else {
        std::cout << "Solver returned with code: " << result << std::endl;
    }

    ipamir_release(solver);
}


int main() {

    char* filename = "satellite02ac.wcsp.wcnf";
    run_wcnf_file_with_ipamir(filename);
    return 0;
}

And here is the makefile associated:

# Compiler
CXX = g++

# Compiler flags
CXXFLAGS = -I./lib -std=c++11 -Wall -Wextra

# Linker flags
LDFLAGS = -L./lib -luwrmaxsat 

# Target executable
TARGET = solve_sat

# Source files
SRCS = solve_sat.cpp

# Object files
OBJS = $(SRCS:.cpp=.o)

all: $(TARGET)

$(TARGET): $(OBJS)
	$(CXX) $(OBJS) $(LDFLAGS) -o $(TARGET)

%.o: %.cpp
	$(CXX) $(CXXFLAGS) -c $< -o $@

clean:
	rm -f $(OBJS) $(TARGET)

.PHONY: all clean

Here is another easier WCNF file which is solved in 0.15 seconds with the static library on my machine, while this code takes 1.7 seconds to solve it.
wcnf_file.txt

Additional information

• The same objective value is found for both the static and dynamic library.
• No errors or warnings are reported during compilation or execution.
• The static and dynamic library are compiled with maxpre and scip.

Do you have any clues as to why it is so much slower with the dynamic library ?

[marekpiotrow]

Hi Gaspard,

the difference between the library and the standalone uwrmaxsat solver is that the solver runs the SCIP solver in a separate thread (in its default configuration) while the library is single-threaded. You can force uwrmaxsat to run in a single thread by the -no-par option. If you compare times of these (single-threaded) versions, they should be almost the same. In case of satellite02ac.wcsp.wcnf, 340s is the solving time of SCIP solver, which is started first with the default time limit of 600s. For this instance, uwrmaxsat alone is much quicker and solves the problem in <2s, if it is run in parallel or without starting SCIP. You can try running your solve_sat application in one of the following ways:
UWRFLAFS="-no-scip" ./solve_sat
UWRFLAGS="-scip-delay=300" ./solve_sat
to observe the time difference when solving this instance without starting SCIP solver or with the start of SCIP delayed by 300s.

If there are no soft literals, the SCIP solver is not started by default.

You can also add the options -v1 (or -v2) to the UWRFLAGS to see more output of the solving process. The time assigned to SCIP can be controled by the options -scip-cpu and -scip-cpu-add (see their short descripions in the output of ./uwrmaxsat -h).

Best regards,
Marek

[marekpiotrow]

I should also add that there should be no difference between ipamir static and dynamic libraries.

You can build a statically linked version of your application by adding -static to CXXFLAGS in the Makefile and changing LDFLAGS to:
LDFLAGS = -static -L./lib -luwrmaxsat -lgmp -L./cominisatps/build/release/lib -lcominisatps -L./scipoptsuite-8.1.0/build/lib -lscip -lsoplex-pic -L./maxpre/src/lib -lmaxpre
to have libuwrmaxsat.a, libcominisatps.a, libscip.a and libsoplex-pic.a statically linked.

The paths above should be set accordingly to your environment.

[gaspard-quenard]

Hi Marek,

Thank you for the explanation, it works perfectly using the UWRFLAGS flags provided.

[marekpiotrow]

Hi Gaspard,

partially inspired by your post, I changed the default behavior of the IPAMIR library in such a way that now it runs the SCIP solver in a separate thread (in the same way as the standalone application). To have it run in a single thread, one must set UWRFLAGS="-no-par".

Best regards,
Marek