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.
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?
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.
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
.