v1.24.10

D-Painless Release Notes

Major Changes

Sharing Architecture

• New SharingEntity: Implements thread-safe subscription-based sharing using weak references to prevent circular dependencies.
• Enhanced GlobalSharingStrategy Implementations: MallobSharing now follows the sharing strategy described in MallobSat.

Clause Management

• Optimized ClauseExchange:

  • When back to use flexible array member pattern for efficient memory layout
  • Implements reference counting via boost::intrusive_ptr
  • Provides safe creation and pointer conversion methods

• Lock-free ClauseBuffer:

  • Wraps boost::lockfree::queue for concurrent operations
  • Supports multiple producers/consumers
  • Maintains proper reference counting during pops and pushes

• New ClauseDatabase Interface:

  • Abstract interface for clause storage systems
  • Used by SharingStrategy and SolverCdclInterface

Requirements

• C++20 or later
• Boost headers
• MPI for distributed operations

International SAT Competition 2024

Version submitted to the ISC24

• 🥇Ranked first in Parallel SAT and UNSAT Tracks.

• Updated descriptions and a detailed article on the parallel solver PL-PRS-BVA-KISSAT-1Gr are provided in the pdf files.

• The different submissions can be launched as follow

  • PL-PRS-BVA-KISSAT-1Gr:

  ./painless -v=1 -c=$nb_solvers -t=5000 -shr-strat=1 -shr-sleep=100000 -sbva-count=12 -ls-after-sbva=2 -sbva-timeout=1000 $path_to_cnf

  • PL-PRS-BVA-KISSAT-2Gr:

  ./painless -v=1 -c=$nb_solvers -t=5000 -shr-strat=3 -shr-sleep=100000 -sbva-count=12 -ls-after-sbva=2 -sbva-timeout=1000 $path_to_cnf

  • PL-PRS-BVA-MPI:

  mpirun --mca btl_tcp_if_include eth0 --mca orte_abort_on_non_zero_status false --allow-run-as-root --hostfile $path_to_hostfile --bind-to none ./painless -v=1 -c=$nb_solvers -t=1000 -sbva-timeout=120 -shr-strat=1 -shr-sleep=100000 -gshr-strat=2 -dist $path_to_cnf