search

NTU-ALComLab / ssatABC

Stochastic SAT solver within ABC
Other
5 stars 2 forks source link

segfaults on empty random quantifier #22

Closed symphorien closed 2 years ago

symphorien commented 2 years ago

When run on an unsat formula like

p cnf 1 2
e 1 0
r 0.7  0
1 0
-1 0

I get a segmentation fault:

$  abc -c ssat unsat.sdimacs
ABC command line: "ssat".

[INFO] Input sdimacs file: unsat.sdimacs
zsh: segmentation fault (core dumped)  abc -c ssat unsat.sdimacs
nianzelee commented 2 years ago

The SSAT file is missing a variable ID for the randomly quantified variable. The syntax is r <probability> <variable ID> 0.

If you modify the file (see below), the solver should return the correct answer, i.e., probability 0.

p cnf 2 2
e 1 0
r 0.7 2 0
1 0
-1 0

(Note that the header is changed because we have two variables and two clauses.)

symphorien commented 2 years ago

Ok so the bug is rather caused by having an empty random quantifier? Unfortunately, removing the random quantifier is not accepted:

[ERROR] Currently only support "{RE,ER}-2SSAT"!
nianzelee commented 2 years ago

Ok so the bug is rather caused by having an empty random quantifier?

This is not a bug. A randomized quantifier has to quantify a variable, which was missing in the formula.

Unfortunately, removing the random quantifier is not accepted:

[ERROR] Currently only support "{RE,ER}-2SSAT"!

The solver can solve SSAT formulas under random-exist or exist-random quantification. If you only have one layer of existential quantification, you can use a SAT solver instead.

symphorien commented 2 years ago

It would have been nice to handle this corner case uniformly, but I get your point. thanks.