Skip to main content
MiniSat provides mechanisms to limit resource consumption during solving. This is essential for real-world applications where unlimited solving time is impractical.

​
Command-line resource limits

Resource limits can be set via command-line options when running the standalone solver.

​
CPU time limit

​
cpu-lim
integer
default:"0"
CPU time limit in secondsRange: [0, INT32_MAX]
  • 0: No limit (default)
  • > 0: Terminate after specified seconds
minisat -cpu-lim=300 problem.cnf output.txt
The solver will stop after 300 seconds (5 minutes) and return INDETERMINATE.
CPU time limits use operating system signals. On timeout, the solver terminates gracefully but may not complete all cleanup operations.

​
Memory limit

​
mem-lim
integer
default:"0"
Memory limit in megabytesRange: [0, INT32_MAX]
  • 0: No limit (default)
  • > 0: Limit memory usage to specified MB
minisat -mem-lim=2048 problem.cnf output.txt
The solver will stop if memory usage exceeds 2048 MB (2 GB).
Memory limits are enforced at the system level using rlimit. If the limit is exceeded, MiniSat catches the allocation failure and returns INDETERMINATE.

​
Programmatic resource limits

When using MiniSat as a library, you have finer control over resource limits through the API.

​
Conflict budget

Limit the number of conflicts before returning: 
#include "minisat/core/Solver.h"

Minisat::Solver solver;

// Add clauses...

// Set conflict budget
solver.setConfBudget(10000);

// Solve with budget
vec<Lit> assumptions;
lbool result = solver.solveLimited(assumptions);

if (result == l_Undef) {
    // Budget exhausted
    printf("Conflict budget reached\n");
} else if (result == l_True) {
    printf("SATISFIABLE\n");
} else {
    printf("UNSATISFIABLE\n");
}
​
setConfBudget
method
Set conflict budget
void setConfBudget(int64_t x)
  • x: Maximum number of conflicts
  • Budget is relative to current conflict count
  • Use budgetOff() to disable

​
Propagation budget

Limit the number of propagations: 
Minisat::Solver solver;

// Set propagation budget
solver.setPropBudget(1000000);

vec<Lit> assumptions;
lbool result = solver.solveLimited(assumptions);

if (result == l_Undef) {
    printf("Propagation budget reached\n");
}
​
setPropBudget
method
Set propagation budget
void setPropBudget(int64_t x)
  • x: Maximum number of propagations
  • Budget is relative to current propagation count
  • Finer-grained control than conflict budget

​
Disabling budgets

// Remove all budgets
solver.budgetOff();

// Now solve() calls have no resource limits
bool result = solver.solve();
The solve() methods (without “Limited” suffix) automatically call budgetOff() before solving. Use solveLimited() to respect budgets.

​
Asynchronous interruption

For long-running solves, you can interrupt from another thread: 
#include <thread>
#include "minisat/core/Solver.h"

Minisat::Solver solver;

// Start solving in background
std::thread solver_thread([&]() {
    vec<Lit> assumptions;
    lbool result = solver.solveLimited(assumptions);
    // Handle result...
});

// Wait for some condition...
std::this_thread::sleep_for(std::chrono::seconds(5));

// Interrupt solving
solver.interrupt();

// Wait for solver to stop
solver_thread.join();

// Clear interrupt flag for future use
solver.clearInterrupt();
​
interrupt
method
Trigger asynchronous interruption
void interrupt()
  • Sets internal flag checked during search
  • Solver stops and returns l_Undef
  • Thread-safe: can be called from signal handlers
​
clearInterrupt
method
Clear interrupt flag
void clearInterrupt()
  • Resets interrupt flag
  • Call before next solve() invocation

​
Combining limits

You can combine multiple limit types: 
Minisat::Solver solver;

// Set multiple limits
solver.setConfBudget(50000);   // Max 50k conflicts
solver.setPropBudget(10000000); // Max 10M propagations

// Setup interrupt handler
std::signal(SIGINT, [](int) {
    solver.interrupt();
});

vec<Lit> assumptions;
lbool result = solver.solveLimited(assumptions);

if (result == l_Undef) {
    // One of the limits was reached
    printf("Resource limit reached\n");
    printf("Conflicts: %lld\n", solver.conflicts);
    printf("Propagations: %lld\n", solver.propagations);
}
The solver stops as soon as any limit is reached. Check the statistics to determine which limit triggered termination.

​
Return values and budgets

Understanding return values when using budgets:
Satisfiable
  • A satisfying assignment was found
  • Result is definitive
  • Budget was not reached
  • Model available in solver.model

​
Practical examples

​
Portfolio solving with timeouts

#include "minisat/core/Solver.h"

void try_configuration(Minisat::Solver& solver, 
                       const char* name,
                       int conflicts) {
    solver.setConfBudget(conflicts);
    
    vec<Lit> assumptions;
    lbool result = solver.solveLimited(assumptions);
    
    if (result != l_Undef) {
        printf("Config %s solved it!\n", name);
    }
}

Minisat::Solver s1, s2, s3;

// Load problem into all solvers...

// Try different configurations with budgets
try_configuration(s1, "aggressive", 10000);
try_configuration(s2, "conservative", 10000);
try_configuration(s3, "random", 10000);

​
Incremental solving with time slices

Minisat::Solver solver;

// Add initial clauses...

// Solve in time slices
for (int round = 0; round < 10; round++) {
    solver.setConfBudget(5000); // 5k conflicts per round
    
    vec<Lit> assumptions;
    lbool result = solver.solveLimited(assumptions);
    
    if (result != l_Undef) {
        printf("Solved in round %d\n", round);
        break;
    }
    
    printf("Round %d: %lld conflicts\n", round, solver.conflicts);
}

​
Statistics for monitoring

Track resource usage through statistics: 
Minisat::Solver solver;

vec<Lit> assumptions;
lbool result = solver.solveLimited(assumptions);

// Check statistics
printf("Conflicts: %lld\n", solver.conflicts);
printf("Propagations: %lld\n", solver.propagations);
printf("Decisions: %lld\n", solver.decisions);
printf("Random decisions: %lld\n", solver.rnd_decisions);
printf("Restarts: %lld\n", solver.starts);
All statistics are cumulative across multiple solve() calls. They are never reset unless you create a new solver instance.

​
Best practices

  1. Start with conflict budgets: Easier to estimate than propagations or time
  2. Use solveLimited(): Regular solve() ignores budgets
  3. Clear interrupts: Always call clearInterrupt() after handling an interrupt
  4. Monitor statistics: Use statistics to calibrate budgets
  5. Handle l_Undef gracefully: Always check for indeterminate results

Configuration

Tune solver parameters for better performance

Performance

Optimize solving speed

Build docs developers (and LLMs) love

Get started for freeTalk to us