Search code examples
satsat-solverssat4j

Is there any SAT Solver that provides a built-in library as Sat4j?

As far as I know, Sat4j is a library that integrates SAT solver miniSAT on Java environment. I've searched on SAT competition (http://www.satcompetition.org/) and found that Kissat considered as the best SAT Solver so far. Thus I wanna find a library that integrates Kissat (or Glucose is also ok) to test the performance.

  1. Is there any SAT Solver that provides a build-in library as Sat4j?
  2. If not, how to test Kissat and Glucose SAT Solver? Thanks a ton!

I've read source code of Kissat and Glucose SAT Solver but I dont understand how to test them by CNF file. Anyone used to work with it can help me?

Solution

  • Kissat usage overview:

    The commandline syntax of Kissat:

    usage: kissat [ <option> ... ] [ <dimacs> [ <proof> ] ]

    To get extensive help

    kissat --help

    The DIMACS CNF file format is described here.

    You are supposed to download and build the Kissat executable. There are no precompiled binaries available in the official Kissat repository. The build process is working for Unix systems.

    A volunteer provides Kissat Windows binaries and libraries on GitHub.

    Example:

    kissat xxx.cnf.txt

    Input file xxx.cnf.txt:

    c CNF/DIMACS file for "<expression>"
c created: 27-Mar-2023 21:00:35
c by akBoole 06-Mar-2023
c command: akBoole "a and b" -d -o xxx.cnf.txt
c a 1
c b 2
c
p cnf 3 4
1 -3 0
2 -3 0
-1 -2 3 0
3 0

    Resulting output:

    c ---- [ banner ] ------------------------------------------------------------
c
c Kissat SAT Solver
c 
c Copyright (c) 2021-2022 Armin Biere University of Freiburg
c Copyright (c) 2019-2021 Armin Biere Johannes Kepler University Linz
c Ported to Windows, 2020 - 2022 Axel Kemper, Springe
c 
c Version sc2021-sweep unknown
c gcc.exe (Rev1, Built by MSYS2 project) 12.1.0 -W -Wall -Wformat=0 -O3 -DNEMBEDDED -DNDEBUG -DNMETRICS -DNSTATISTICS -D__USE_MINGW_ANSI_STDIO=1 -mno-ms-bitfields -I../src/pal-win -include global.h
c Sat, Jul 2, 2022 10:54:48 PM MINGW64_NT-10.0-19044 akLand 3.3.5-341.x86_64 x86_64
c
c ---- [ parsing ] -----------------------------------------------------------
c
c opened and reading DIMACS file:
c
c   xxx.cnf.txt
c
c parsed 'p cnf 3 4' header
c closing input after reading 193 bytes
c finished parsing after 0.00 seconds
c
c ---- [ solving ] -----------------------------------------------------------
c
c  seconds switched rate      trail variables
c         MB reductions conflicts glue remaining
c          level restarts redundant irredundant
c
c *  0.02  0 0 0 0  0 0   0   0 0% 0  3  0 0%
c {  0.02  0 0 0 0  0 0   0   0 0% 0  3  0 0%
c }  0.02  0 0 0 0  0 0   0   0 0% 0  3  0 0%
c 1  0.02  0 0 0 0  0 0   0   0 0% 0  3  0 0%
c
c ---- [ result ] ------------------------------------------------------------
c
s SATISFIABLE
v 1 2 3 0
c
c ---- [ profiling ] ---------------------------------------------------------
c
c           0.00    0.00 %  search
c           0.00    0.00 %  simplify
c =============================================
c           0.02  100.00 %  total
c
c ---- [ statistics ] --------------------------------------------------------
c
c conflicts:                                0                0.00 per second
c decisions:                                0                0.00 per conflict
c propagations:                             3              192    per second
c
c ---- [ resources ] ---------------------------------------------------------
c
c maximum-resident-set-size:          3166208 bytes          3 MB
c process-time:                                              0.02 seconds
c
c ---- [ shutting down ] -----------------------------------------------------
c
c exit 10

    Note two special and significant output lines:

    s SATISFIABLE
v 1 2 3 0

    The example has a solution, i.e. is satisfiable. The three input variables all have the value 1/true.