search

marcthurley / sharpSAT

The #SAT solver sharpSAT
MIT License
55 stars 24 forks source link

Fixing bug with log(0) called #15

Open msoos opened 2 years ago

msoos commented 2 years ago

This fixes a log(0) issue with CNF:

p cnf 4 4
-2 4 0
3 4 0
-3 -4 0
3 -4 0

That otherwise gives:

soos@tiresias:count_fuzzer$ ../sharpSAT/build/sharpSAT a.cnf 
Solving a.cnf
variables (all/used/free):      4/4/0
clauses (all/long/binary/unit): 4/0/4/0

Preprocessing .. DONE
variables (all/used/free):      1/0/1
clauses (all/long/binary/unit): 0/0/0/0
56 16
sharpSAT: /home/soos/development/sat_solvers/sharpSAT/src/component_types/difference_packed_component.h:119: DifferencePackedComponent::DifferencePackedComponent(Component&): Assertion `(data_size >> bits_of_data_size()) == 0' failed.
Aborted (core dumped)

@latower for visibility

ZaydH commented 2 years ago

@msoos Since sharpSAT's pull requests have sat for years, it might make sense for your team to fork the repository so it can stay up to date with fixes/features as needed.