BitContradiction filtering improvements.

This commit is contained in:
Marek Lemańczyk committed 2026-02-15 16:12:57 +01:00
1 parent 9ed467b4b0
commit 411310cf40
2 files changed
+46 -39

No files matched your search

@@ -144,8 +144,8 @@ internal sealed class PrivateWorkSet
internal static class BitContradictionSolverWithAMultiplier internal static class BitContradictionSolverWithAMultiplier
{ {
#if DETAILED_LOG || WITH_PRUNE_STATS #if DETAILED_LOG || WITH_PRUNE_STATS
private const ulong DebugTargetP = 138000953UL; private const ulong DebugTargetP = 138001793UL;
private static readonly BigInteger DebugTargetK = new(((337429718205079UL - 1UL) >> 1) / DebugTargetP); private static readonly BigInteger DebugTargetK = new(((1976939441553367UL - 1UL) >> 1) / DebugTargetP);
private static readonly BigInteger DebugTargetQ = ((DebugTargetK * DebugTargetP) << 1) + BigInteger.One; private static readonly BigInteger DebugTargetQ = ((DebugTargetK * DebugTargetP) << 1) + BigInteger.One;
// private const ulong DebugTargetQ = 1209708008767UL; // private const ulong DebugTargetQ = 1209708008767UL;
@@ -2613,7 +2613,7 @@ internal static class BitContradictionSolverWithAMultiplier
{ {
pruneReason = CarryDropPruneReason.ZeroDrop; pruneReason = CarryDropPruneReason.ZeroDrop;
#if WITH_PRUNE_STATS #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif #endif
return true; return true;
} }
@@ -2640,8 +2640,8 @@ internal static class BitContradictionSolverWithAMultiplier
) )
{ {
pruneReason = CarryDropPruneReason.DominanceReached10AndStayedAbove5; pruneReason = CarryDropPruneReason.DominanceReached10AndStayedAbove5;
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#if WITH_PRUNE_STATS #if WITH_PRUNE_STATS
// TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif #endif
return true; return true;
} }
@@ -2653,9 +2653,9 @@ internal static class BitContradictionSolverWithAMultiplier
) )
{ {
pruneReason = CarryDropPruneReason.Dominance1011121314; pruneReason = CarryDropPruneReason.Dominance1011121314;
#if WITH_PRUNE_STATS // #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif // #endif
return true; return true;
} }
@@ -2664,9 +2664,9 @@ internal static class BitContradictionSolverWithAMultiplier
(totalCarry67Count > totalCarry8Count && zeroCount < first10 && lowestCarryAfter10 >= 3 && (totalCarry7Count > totalCarry8Count || (totalCarry7Count & 1) == 1))) (totalCarry67Count > totalCarry8Count && zeroCount < first10 && lowestCarryAfter10 >= 3 && (totalCarry7Count > totalCarry8Count || (totalCarry7Count & 1) == 1)))
{ {
pruneReason = CarryDropPruneReason.Dominance67ThenZeroDrop; pruneReason = CarryDropPruneReason.Dominance67ThenZeroDrop;
#if WITH_PRUNE_STATS // #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif // #endif
return true; return true;
} }
@@ -2677,9 +2677,9 @@ internal static class BitContradictionSolverWithAMultiplier
) )
{ {
pruneReason = CarryDropPruneReason.Dominance15161718Drop; pruneReason = CarryDropPruneReason.Dominance15161718Drop;
#if WITH_PRUNE_STATS // #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif // #endif
return true; return true;
} }
@@ -2688,9 +2688,9 @@ internal static class BitContradictionSolverWithAMultiplier
(totalCarry10Count >= totalCarry9Count || totalCarry8Count >= totalCarry9Count || totalCarry10Count < 190)) (totalCarry10Count >= totalCarry9Count || totalCarry8Count >= totalCarry9Count || totalCarry10Count < 190))
{ {
pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop; pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop;
#if WITH_PRUNE_STATS // #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif // #endif
return true; return true;
} }
@@ -2714,9 +2714,9 @@ internal static class BitContradictionSolverWithAMultiplier
) )
{ {
pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop; pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop;
#if WITH_PRUNE_STATS // #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif // #endif
return true; return true;
} }
@@ -2756,18 +2756,18 @@ internal static class BitContradictionSolverWithAMultiplier
) )
{ {
pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop; pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop;
#if WITH_PRUNE_STATS // #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif // #endif
return true; return true;
} }
if (totalCarry7Count + totalCarry8Count > totalCarry9Count + totalCarry10Count && totalCarry11Count > 100) if (totalCarry7Count + totalCarry8Count > totalCarry9Count + totalCarry10Count && totalCarry11Count > 100)
{ {
pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop; pruneReason = CarryDropPruneReason.Dominance10AndMoreDrop;
#if WITH_PRUNE_STATS // #if WITH_PRUNE_STATS
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif // #endif
return true; return true;
} }
@@ -2790,7 +2790,7 @@ internal static class BitContradictionSolverWithAMultiplier
AnsiConsole.MarkupLine($"[MediumOrchid1_1]{nameof(CarryDropPruneReason.HighDensityWithShortLowStreaks)}[/] prune reason for [DodgerBlue1]p[/]=[Gray100 Bold]{pLong}[/], [DodgerBlue1]q[/]=[Gray100 Bold]{qExact}[/]: [DarkOrange]totalCarryAbove10[/]=[Yellow]{totalCarryAbove10}[/], [DarkOrange]shortestStreakBelow10[/]=[Yellow]{shortestStreakBelow10}[/], [DarkOrange]lastStreakBelow10[/]=[Yellow]{lastStreakBelow10}[/], [DarkOrange]first10[/]=[Yellow]{first10}[/], [DarkOrange]totalCarryBelow10[/]=[Yellow]{totalCarryBelow10}[/], [DarkOrange]longestStreakBelow10[/]=[Yellow]{longestStreakBelow10}[/], [DarkOrange]totalCarry11Count[/]=[Yellow]{totalCarry11Count}[/]"); AnsiConsole.MarkupLine($"[MediumOrchid1_1]{nameof(CarryDropPruneReason.HighDensityWithShortLowStreaks)}[/] prune reason for [DodgerBlue1]p[/]=[Gray100 Bold]{pLong}[/], [DodgerBlue1]q[/]=[Gray100 Bold]{qExact}[/]: [DarkOrange]totalCarryAbove10[/]=[Yellow]{totalCarryAbove10}[/], [DarkOrange]shortestStreakBelow10[/]=[Yellow]{shortestStreakBelow10}[/], [DarkOrange]lastStreakBelow10[/]=[Yellow]{lastStreakBelow10}[/], [DarkOrange]first10[/]=[Yellow]{first10}[/], [DarkOrange]totalCarryBelow10[/]=[Yellow]{totalCarryBelow10}[/], [DarkOrange]longestStreakBelow10[/]=[Yellow]{longestStreakBelow10}[/], [DarkOrange]totalCarry11Count[/]=[Yellow]{totalCarry11Count}[/]");
} }
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif #endif
return true; return true;
} }
@@ -2825,7 +2825,7 @@ internal static class BitContradictionSolverWithAMultiplier
( (
lastStreakBelow10 >= 5 || lastStreakBelow10 >= 5 ||
lastStreakBelow10 == 0 || lastStreakBelow10 == 0 ||
(lastStreakBelow10 < 5 && totalTransitionsOver10 > 100) || (lastStreakBelow10 < 5 && totalTransitionsOver10 > 90) ||
(lastStreakBelow10 < 5 && totalCarryBelow10 < 186) || (lastStreakBelow10 < 5 && totalCarryBelow10 < 186) ||
(totalTransitionsOver10 < 100) (totalTransitionsOver10 < 100)
) )
@@ -2842,20 +2842,23 @@ internal static class BitContradictionSolverWithAMultiplier
(lastStreakBelow10 <= 28 && lastStreakBelow10 > 0) || (lastStreakBelow10 <= 28 && lastStreakBelow10 > 0) ||
(longestStreakBelow10 < 49 && first10 < 32) || (longestStreakBelow10 < 49 && first10 < 32) ||
(totalTransitionsOver10 > 63 && longestStreakBelow10 > 40) || (totalTransitionsOver10 > 63 && longestStreakBelow10 > 40) ||
(totalCarryBelow10 < 300 && totalCarry2Count < 8 && lastStreakBelow10 > 0) || (totalCarryBelow10 < 300 && totalCarry2Count < 8 && (lastStreakBelow10 > 0 || totalCarryBelow10 > totalCarry11Count)) ||
(totalTransitionsOver10 > 63 && first10 < 32) || (totalTransitionsOver10 > 44 && first10 < 32) ||
(totalTransitionsOver10 > 80 && totalCarryBelow10 > totalCarry10Count) || (totalTransitionsOver10 > 44 && totalCarryBelow10 > totalCarry10Count) ||
(totalTransitionsOver10 > 100 && totalCarry10Count > totalCarryBelow10) || (totalTransitionsOver10 > 44 && totalCarry10Count >= totalCarryBelow10) ||
(totalCarry10Count > totalCarryBelow10 && totalCarry11Count > 200) (totalCarry10Count > totalCarryBelow10 && totalCarry11Count > 200)
) )
) || ) ||
( (
totalTransitionsOver10 <= 35 && totalTransitionsOver10 <= 35 &&
( (
longestStreakBelow10 < 31 || (longestStreakBelow10 < 31 && totalCarryBelow10 > 62) ||
longestStreakBelow10 > 40 ||
(longestStreakBelow10 > 0 && longestStreakBelow10 < 20) ||
(longestStreakBelow10 > 30 && first10 < 32) ||
zeroCount > 10 zeroCount > 10
) && ) &&
zeroCount > 4 (zeroCount > 4 || first10 < 32)
) )
) )
) || ) ||
@@ -2885,7 +2888,7 @@ internal static class BitContradictionSolverWithAMultiplier
AnsiConsole.MarkupLine($"[MediumOrchid1_1]{nameof(CarryDropPruneReason.DominanceReached10AndStayedAbove5)}[/] prune reason for [DodgerBlue1]p[/]=[Gray100 Bold]{pLong}[/], [DodgerBlue1]q[/]=[Gray100 Bold]{qExact}[/]: [DarkOrange]reached5[/]=[Yellow]{reached5}[/], [DarkOrange]totalTransitionsOver10[/]=[Yellow]{totalTransitionsOver10}[/], [DarkOrange]lastStreakBelow10[/]=[Yellow]{lastStreakBelow10}[/], [DarkOrange]longestStreakBelow10[/]=[Yellow]{longestStreakBelow10}[/], [DarkOrange]zeroCount[/]=[Yellow]{zeroCount}[/], [DarkOrange]first10[/]=[Yellow]{first10}[/], [DarkOrange]totalCarryBelow10[/]=[Yellow]{totalCarryBelow10}[/], [DarkOrange]totalCarry2[/]=[Yellow]{totalCarry2Count}[/], [DarkOrange]totalCarry10[/]=[Yellow]{totalCarry10Count}[/], [DarkOrange]totalCarry11[/]=[Yellow]{totalCarry11Count}[/]{Environment.NewLine}"); AnsiConsole.MarkupLine($"[MediumOrchid1_1]{nameof(CarryDropPruneReason.DominanceReached10AndStayedAbove5)}[/] prune reason for [DodgerBlue1]p[/]=[Gray100 Bold]{pLong}[/], [DodgerBlue1]q[/]=[Gray100 Bold]{qExact}[/]: [DarkOrange]reached5[/]=[Yellow]{reached5}[/], [DarkOrange]totalTransitionsOver10[/]=[Yellow]{totalTransitionsOver10}[/], [DarkOrange]lastStreakBelow10[/]=[Yellow]{lastStreakBelow10}[/], [DarkOrange]longestStreakBelow10[/]=[Yellow]{longestStreakBelow10}[/], [DarkOrange]zeroCount[/]=[Yellow]{zeroCount}[/], [DarkOrange]first10[/]=[Yellow]{first10}[/], [DarkOrange]totalCarryBelow10[/]=[Yellow]{totalCarryBelow10}[/], [DarkOrange]totalCarry2[/]=[Yellow]{totalCarry2Count}[/], [DarkOrange]totalCarry10[/]=[Yellow]{totalCarry10Count}[/], [DarkOrange]totalCarry11[/]=[Yellow]{totalCarry11Count}[/]{Environment.NewLine}");
} }
TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount); // TraceCarryDropHeuristicPrune(pLong, qExact, pruneReason, reached10, reachedBelow5, reached5, zeroCount);
#endif #endif
return true; return true;
} }
@@ -3128,13 +3131,15 @@ internal static class BitContradictionSolverWithAMultiplier
reason = ContradictionReason.ParityUnreachable; reason = ContradictionReason.ParityUnreachable;
#endif #endif
#if WITH_PRUNE_STATS #if WITH_PRUNE_STATS
if (pLong == 138000953 && qExact.Equals(_testCase)) // if (pLong == 138000953 && qExact.Equals(_testCase))
{ // {
AnsiConsole.MarkupLine($"Validating heuristic prune: p={pLong}, q={qExact}, reason={carryDropPruneReason}"); // AnsiConsole.MarkupLine($"Validating heuristic prune: p={pLong}, q={qExact}, reason={carryDropPruneReason}");
} // }
#endif #endif
#if WITH_PRUNE_VALIDATION
ValidateHeuristicPruneAgainstPowmod2OrThrow(qExact, pLong, $"CarryDropHeuristic:{carryDropPruneReason}"); ValidateHeuristicPruneAgainstPowmod2OrThrow(qExact, pLong, $"CarryDropHeuristic:{carryDropPruneReason}");
#endif
return true; return true;
} }
#if false #if false
@@ -3426,8 +3431,9 @@ internal static class BitContradictionSolverWithAMultiplier
#if WITH_PRUNE_STATS #if WITH_PRUNE_STATS
IncrementPruneCounter(ref _prunedWithTryPropagateCarry1); IncrementPruneCounter(ref _prunedWithTryPropagateCarry1);
#endif #endif
#if WITH_PRUNE_VALIDATION
ValidateHeuristicPruneAgainstPowmod2OrThrow(qExact, pLong, "TryPropagateCarry1"); ValidateHeuristicPruneAgainstPowmod2OrThrow(qExact, pLong, "TryPropagateCarry1");
#endif
return true; return true;
} }
} }
@@ -14,6 +14,7 @@
<!-- <DefineConstants>$(DefineConstants);SELF_TEST</DefineConstants> --> <!-- <DefineConstants>$(DefineConstants);SELF_TEST</DefineConstants> -->
<!-- <DefineConstants>$(DefineConstants);EXPORT_STAGE</DefineConstants> --> <!-- <DefineConstants>$(DefineConstants);EXPORT_STAGE</DefineConstants> -->
<DefineConstants>$(DefineConstants);WITH_PRUNE_STATS</DefineConstants> <DefineConstants>$(DefineConstants);WITH_PRUNE_STATS</DefineConstants>
<DefineConstants>$(DefineConstants);WITH_PRUNE_VALIDATION</DefineConstants>
</PropertyGroup> </PropertyGroup>
<ItemGroup> <ItemGroup>