Package: picosat
Version: 913-1
Severity: normal
Dear maintainer,
The package description says:
>Description: SAT solver with proof and core support
and the help message shows:
>% picosat -h
>usage: picosat [ <option> ... ] [ <input> ]
(snip)
> -t <trace> generate compact proof trace file
> -T <trace> generate extended proof trace file
> -r <trace> generate reverse unit propagation proof file
> -c <core> generate clausal core file in DIMACS format
> -V <core> generate file listing core variables
> -U <core> generate file listing used variables
but I cannot get the proof or core.
>% echo p cnf 1 2 1 0 -1 0 | picosat -c core.txt
(snip)
>c writing clausal core to 'core.txt'
>*** picosat: compiled without trace support
>Abort
How to fix:
(a) Modify the configure file s/satcompetition=yes/satcompetition=no/
(this may be an upstream release bug that can not be disabled the
"satcompetition" mode by any configure option).
And
(b) Remove CFLAGS in debian/rules file not to pass this variable to the
configure script.
Additional comment:
Enabling trace support will cause some performance drop (so disabled
for SAT competition). It is a trade-off.
Could you please include two executable binary of both trace on and off
in the picosat package (or in the separated two packages) ?
Regards,
Nobuhiro
--
To UNSUBSCRIBE, email to [email protected]
with a subject of "unsubscribe". Trouble? Contact [email protected]
