Older solvers did not differentiate when reporting failed
literals via the ipasir interface - they reported on a variable
granularity. More recent solvers like CaDiCaL and MergeSat report
on a per-literal basis. Hence, the code needed to be adapted to
fit the two reporting styles.
$:~/git/mergesat/ipasir$ git show -s
commit fef144cdaae178fb3985e2b770ba6a1509ca2b6e (HEAD -> ipasir-check-fixes, conps/ipasir-check-fixes)
Author: Norbert Manthey <nmanthey@conp-solutions.com>
Date: Fri Dec 31 14:32:04 2021 +0100
SATSolver: fix handling conflict clause
Older solvers did not differentiate when reporting failed
literals via the ipasir interface - they reported on a variable
granularity. More recent solvers like CaDiCaL and MergeSat report
on a per-literal basis. Hence, the code needed to be adapted to
fit the two reporting styles.
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
$:~/git/mergesat/ipasir$ bin/ipasir-check-satunsat-cadicalsc2020 10 2 8
Norbert Manthey -- IPASIR iterative satunsat checker
add formula that has sub formulas of blocks
use almost full stack of assumptions, except last variable for each block
and modify last polarities per call
initialized IPASIR solver: cadical-sc2020
created formula with 24 clauses, and maxvar 16
initial call returned with 10
performed 243902 calls per second, 2 SAT, 7 UNSAT
$:~/git/mergesat/ipasir$ bin/ipasir-check-satunsat-minisat220 10 2 8
Norbert Manthey -- IPASIR iterative satunsat checker
add formula that has sub formulas of blocks
use almost full stack of assumptions, except last variable for each block
and modify last polarities per call
initialized IPASIR solver: minisat220
created formula with 24 clauses, and maxvar 16
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
initial call returned with 10
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
performed 65789.5 calls per second, 2 SAT, 7 UNSAT
c [minisat220]
c [minisat220] calls 10 5773.7 per second
c [minisat220] restarts 10 5773.7 per second
c [minisat220] conflicts 2 1154.7 per second
c [minisat220] decisions 3 1732.1 per second
c [minisat220] propagations 166 95843.0 per second
c [minisat220]
Before the fix, MiniSat works, and CaDiCaL fails
$:~/git/mergesat/ipasir$ git checkout origin/master
$:~/git/mergesat/ipasir$ git show -s
commit a09fe113b64c61fb8ed95b19b007d7043540243e (HEAD, origin/master, origin/HEAD, conps/master, master)
Merge: ce05488 ac4cacc
Author: Tomas Balyo <biotomas@gmail.com>
Date: Wed May 13 10:46:42 2020 +0200
Merge pull request #17 from conp-solutions/ipasir-check
Ipasir check
$:~/git/mergesat/ipasir$ ./scripts/mkcln.sh
$:~/git/mergesat/ipasir$ ./scripts/mkone.sh ipasir-check-satunsat cadicalsc2020 &> /dev/null; echo $?
0
$:~/git/mergesat/ipasir$ ./scripts/mkone.sh ipasir-check-satunsat minisat220 &> /dev/null; echo $?
0
$:~/git/mergesat/ipasir$ bin/ipasir-check-satunsat-cadicalsc2020 10 2 8
Norbert Manthey -- IPASIR iterative satunsat checker
add formula that has sub formulas of blocks
use almost full stack of assumptions, except last variable for each block
and modify last polarities per call
initialized IPASIR solver: cadical-sc2020
created formula with 24 clauses, and maxvar 16
initial call returned with 10
error: in call 9, did not detect model (but 20) on satisfiable input, abort
used assumptions: -1 -2 -3 -5 -6 -7 -9 -10 -11 -13 -14 -15
$:~/git/mergesat/ipasir$ bin/ipasir-check-satunsat-minisat220 10 2 8
Norbert Manthey -- IPASIR iterative satunsat checker
add formula that has sub formulas of blocks
use almost full stack of assumptions, except last variable for each block
and modify last polarities per call
initialized IPASIR solver: minisat220
created formula with 24 clauses, and maxvar 16
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
initial call returned with 10
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
c [minisat220] ============================[ Search Statistics ]==============================
c [minisat220] | Conflicts | ORIGINAL | LEARNT | Progress |
c [minisat220] | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c [minisat220] ===============================================================================
c [minisat220] ===============================================================================
performed 48543.7 calls per second, 2 SAT, 7 UNSAT
c [minisat220]
c [minisat220] calls 10 4621.1 per second
c [minisat220] restarts 10 4621.1 per second
c [minisat220] conflicts 2 924.2 per second
c [minisat220] decisions 3 1386.3 per second
c [minisat220] propagations 166 76709.8 per second
c [minisat220]
Older solvers did not differentiate when reporting failed literals via the ipasir interface - they reported on a variable granularity. More recent solvers like CaDiCaL and MergeSat report on a per-literal basis. Hence, the code needed to be adapted to fit the two reporting styles.
Signed-off-by: Norbert Manthey nmanthey@conp-solutions.com
Testing Done
After the fix, check runs successfully
Before the fix, MiniSat works, and CaDiCaL fails