Sometimes a component is generated, which contains no variables.
An assertion which detects these cases is given in 3c02806:
|
assert(rComp.varsBegin()->get<VariableIndex>() != varsSENTINEL |
|
&& "There are no variables in the component. That may be an issue."); |
An examples test instance is given in 039a029:
|
p cnf 6 13 |
|
c position 0 has variables 1..2 |
|
c position 1 has variables 3..4 |
|
c position 2 has variables 5..6 |
|
2 1 0 |
|
-2 -1 0 |
|
4 3 0 |
|
-4 -3 0 |
|
6 5 0 |
|
-6 -5 0 |
|
-1 -6 0 |
|
-4 -6 0 |
|
3 0 |
|
-5 -3 -1 0 |
|
5 3 0 |
|
5 1 0 |
|
3 1 0 |
Sometimes a component is generated, which contains no variables.
An assertion which detects these cases is given in 3c02806:
sharpSAT/include/sharpSAT/component_types/difference_packed_component.h
Lines 77 to 78 in 3c02806
An examples test instance is given in 039a029:
sharpSAT/test/benchmark/mks/wiki_geometry.cnf
Lines 1 to 17 in 039a029