-t doesn't appear to be working?

[drautb]

On a CNF with a large number of solutions, the -t flag does not appear to be respected?

For example:

➜  ~ sharpSAT -t 5 test.cnf 
Solving test.cnf
variables (all/used/free): 	24157/24157/0
clauses (all/long/binary/unit): 117992/107702/4802/5488

Preprocessing .. DONE
variables (all/used/free): 	9114/9114/0
clauses (all/long/binary/unit): 30429/20776/9653/0

time elapsed: 60.8239s
conflict clauses (all / bin / unit) 	20760/4434/0
failed literals found by implicit BCP 	 142729
implicit BCP miss rate 	 99.5291%
cache size 171MB
components (stored / hits) 		155330/202902
avg. variable count (stored / hits) 	290.042/108.931
cache miss rate 15.7594%
^C
➜  ~ 

It runs for over 60s before I kill it, even though I had passed -t 5 as an argument.

[ZaydH]

If you would be willing to share your test.cnf file, I can take a look at the issue for you. I have made extensive modifications to my own build of sharpSAT (called SPUR). I am pretty sure the timer works in my mods if you try it.

[drautb]

Sure, here's the CNF.

test.cnf.zip

[ZaydH]

@drautb I submitted a pull request. However, I am not optimistic of it getting roped in as it seems the project is no longer active. You can get the fix at my fork of the repo.

If you run into an issue, let me know.