Question about unlabeled OR nodes

[symphorien]

I'm intrigued as to why only some OR nodes are labeled with an opposing variable.
The corresponding code is here

dsharp/src/src_sharpSAT/MainSolver/DecisionTree.cpp

Lines 726 to 731 in b8b2526

	//Dimitar Sht. Shterionov: ignoring negative values on OR nodes
	if (choiceVar > 0)
	out << "O " << choiceVar << " " << children.size();
	else
	out << "O 0 " << children.size();

and does not explain why only positive literals are valid opposing variables.
I tried to patch this away,

diff --git a/src/src_sharpSAT/MainSolver/DecisionTree.cpp b/src/src_sharpSAT/MainSolver/DecisionTree.cpp
index a9a3f11..6311652 100644
--- a/src/src_sharpSAT/MainSolver/DecisionTree.cpp
+++ b/src/src_sharpSAT/MainSolver/DecisionTree.cpp
@@ -724,8 +724,8 @@ void DTNode::genNNF(ostream & out)
 	else if (DT_OR == type)
 	{
 		//Dimitar Sht. Shterionov: ignoring negative values on OR nodes
-		if (choiceVar > 0)
-			out << "O " << choiceVar << " " << children.size();
+		if (true)
+			out << "O " << std::abs(choiceVar) << " " << children.size();
 		else
 			out << "O 0 " << children.size();
 
diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h
index 1eb440c..1ef75cd 100644
--- a/src/src_sharpSAT/MainSolver/MainSolver.h
+++ b/src/src_sharpSAT/MainSolver/MainSolver.h
@@ -333,7 +333,7 @@ public:
 					out << "AND";
 					break;
 				case DT_OR:
-					out << "OR";
+					out << "OR " << node->choiceVar;
 					break;
 				case DT_BOTTOM:
 					out << "F";

but of course this leads to incorrect results:
with

p cnf 4 16
-2 1 4 0
3 1 -4 0
-2 3 -4 0
1 4 3 0
3 -1 -2 0
1 -4 3 0
4 2 3 0
-1 -2 4 0
2 -1 3 0
3 -4 1 0
2 -1 4 0
-4 1 -2 0
3 -4 -2 0
2 3 -4 0
3 2 -4 0
2 -1 -4 0

and priority to variables 2,4 I get

nnf 13 16 4
L -2
L -1
L -4
L 3
A 4 0 1 2 3
L 4
A 2 0 1
L 2
L 1
A 2 7 8
O 0 2 6 9
A 3 5 3 10
O 0 2 4 11

with vanilla dsharp (see the two unlabeled OR nodes)
and with the patched dsharp I get

nnf 13 16 4
L -2
L -1
L -4
L 3
A 4 0 1 2 3
L 4
A 2 0 1
L 2
L 1
A 2 7 8
O 1 2 6 9
A 3 5 3 10
O 3 2 4 11

but the label 3 on the last OR node is incorrect: both branches lead to node 3 (L 3).

[haz]

Hrmz...well my first hunch was that the check was there for a non-negative variable number. choiceVar seems to hint at that, and since that was my first reaction, that may in fact be what the intention was. Searching through, this is only assigned once in the main solver (here), and this appears to use a literal value and not just the positive variable value.

So my suggestion then would be to use != 0 as the comparison, and make sure choiceVar is set to 0 by default in the constructor. Doesn't quite explain what's going on with the choice of 3 instead of 4 for that decision node. If I had to guess, I'd say there was a decision of 3 at the root, -3 proved unsolvable, the root Or was simplified to a single child, and the simplification merged a decision on 3 with a decision on 4 into a single Or node.

Won't have a chance to poke around the code for this until late April (very busy wrapping up courses), but happy to keep guiding you if you want to plug away. You seem to already have a handle on what's going on in the code ;)

[symphorien]

I think I found the issue: the choiceVar of OR nodes is not translated. I will make a PR fixing this in the comming day, if everything goes well.

[haz]

Ah! That'd do it. Nothing has caused me more grief than the finicky details of the translation procedures. I should have suspected it to begin with. Nice catch!