Getting @CNF_RESERVED_XXX instead of literals for big model

[DarioRomano]

Hello, it's likely user error, but I'm unsure how to resolve the issue myself. I'm currently using logicNG to process models originating from the UVL and pure::variants domain. My code modifies constraints using your framework. For a rather big model, depending on the configuration of my code I suddenly find @CNF_RESERVED_XXX instead of Literals (features) in my constraints. The formula factory for the specific situation gives me the following printout:

Name:              
Positive Literals: 4810
Negative Literals: 4634
Negations:         18
Implications:      0
Equivalences:      0
Conjunctions (2):  5902
Conjunctions (3):  5977
Conjunctions (4):  5782
Conjunctions (>4): 14789
Disjunctions (2):  118824
Disjunctions (3):  10354
Disjunctions (4):  20549
Disjunctions (>4): 34096
Pseudo Booleans:   0
CCs:               0

Have I possibly misconfigured the FormulaFactory, or could I be misusing the library in some other way? I would be very thanksful for any insights you can provide.

Thanks in advance.

[DarioRomano]

If it is of any help, here's also the configuration of the formula factory:

{CNF=CNFConfig{
algorithm=ADVANCED
fallbackAlgorithmForAdvancedEncoding=TSEITIN
distributedBoundary=-1
createdClauseBoundary=1000
atomBoundary=12
}
, MINISAT=MiniSatConfig{
varDecay=0.95
varInc=1.0
clauseMin=DEEP
restartFirst=100
restartInc=2.0
clauseDecay=0.999
removeSatisfied=true
learntsizeFactor=0.3333333333333333
learntsizeInc=1.1
incremental=true
initialPhase=false
proofGeneration=false
cnfMethod=PG_ON_SOLVER
auxiliaryVariablesInModels=false
bbInitialUBCheckForRotatableLiterals=true
bbCheckForComplementModelLiterals=true
bbCheckForRotatableLiterals=true
}, GLUCOSE=GlucoseConfig{
lbLBDMinimizingClause=6
lbLBDFrozenClause=30
lbSizeMinimizingClause=30
firstReduceDB=2000
specialIncReduceDB=1000
incReduceDB=300
factorK=0.8
factorR=1.4
sizeLBDQueue=50
sizeTrailQueue=5000
reduceOnSize=false
reduceOnSizeSize=12
maxVarDecay=0.95
}, MAXSAT=MaxSATConfig{
incrementalStrategy=NONE
pbEncoding=LADDER
pbEncoding=SWC
cardinalityEncoding=TOTALIZER
weightStrategy=NONE
solverType=GLUCOSE
verbosity=NONE
symmetry=true
limit=2147483647
bmo=true
}, MUS=MUSConfig{
algorithm=DELETION
}
, CC_ENCODER=CCConfig{
amoEncoder=BEST
amkEncoder=BEST
alkEncoder=BEST
exkEncoder=BEST
bimanderGroupSize=SQRT
bimanderFixedGroupSize=3
nestingGroupSize=4
productRecursiveBound=20
commanderGroupSize=3
}
, PB_ENCODER=PBConfig{
pbEncoder=BEST
binaryMergeUseGAC=true
binaryMergeNoSupportForSingleBit=false
binaryMergeUseWatchDog=true
}
, FORMULA_RANDOMIZER=FormulaRandomizerConfig{
seed=0
variables=null
numVars=25
weightConstant=0.1
weightPositiveLiteral=1.0
weightNegativeLiteral=1.0
weightOr=30.0
weightAnd=30.0
weightNot=1.0
weightImpl=1.0
weightEquiv=1.0
maximumOperandsAnd=5
maximumOperandsOr=5
weightPbc=0.0
weightPbcCoeffPositive=1.0
weightPbcCoeffNegative=0.2
weightPbcTypeLe=0.2
weightPbcTypeLt=0.2
weightPbcTypeGe=0.2
weightPbcTypeGt=0.2
weightPbcTypeEq=0.2
maximumOperandsPbc=5
maximumCoefficientPbc=10
weightCc=0.0
weightAmo=0.0
weightExo=0.0
maximumOperandsCc=5
}, ADVANCED_SIMPLIFIER=AdvancedSimplifierConfig{restrictBackbone=true, factorOut=true, simplifyNegations=true, ratingFunction=org.logicng.transformations.simplification.DefaultRatingFunction@5a13d9ca, handler=null}}

[czengler]

Hi @DarioRomano

the @CNF_RESERVED_XXX are auxiliary variables generated by a CNF transformation algorithm (like Tseitin oder Plaisted-Greenbaum). So I guess, you generate a CNF somewhere? There are different algorithms to generate a CNF in LogicNG, some of them do not introduce auxiliary variables (like the factorization, or the BDD based CNF algorithm), others introduce new auxiliary variables (Tseitin, or PG).

The default algorithm advanved is a combination of both - it tries to generate a CNF without the introduction of auxiliary variables and if it gets too large, switches to an algorithm which introduces auxiliary variables. If you say, you have quite a large model, it is very well possible, that a CNF without the introduction of auxiliary variables is not feasible.

All the different algorithms and pitfalls are documented here: https://logicng.org/documentation/formulas/operations/transformations/normal-form-transformations/#cnf-transformations

But usually, these auxiliary variables do no harm. I do not know, if you really need the CNF in your application. If you just need it, to add a formula to our SAT Solver, you don't ;) You can add regular formulas to our SAT Solver without the need to convert them to CNF first - the solver performs the transformations internally.

So, if the auxiliary variables are really a problem for you, we would need to understand a little bit more about the use case and the problem.

[DarioRomano]

Thank you for the answer! I'm currently using your framework to perform constraint transformation on variability models. I'm using CNF transformations on some (parts of) constraints, to modify and potentially merge them. Sometimes they are also used to split constraints into more simple constraints. For example I have a constraint:

A => B or (C and ~D)

I then apply the CNF to only the subtree to the right of the implication to get:

A =>(B or C) and (B or ~D)

at this point I can split the constraint up into two smaller constraints within the same model:

A => B or C
A => B or ~D

I'm performing these splits because I'm trying to bring more complex constraints into the domain of "Relations" used by the pure::variants software. These Relations can only be formed from constraints with limited complexity, so I'm trying to split complex constraints into lower complexity ones that I can then transform into Relations. More info on that in this paper.

In any case, for this use case I need to be able to access the created CNF-formulas again when performing additional operations on them and re-assembling them to new constraints.

Again, thanks for the answer, and I will look into your provided link to see if there's an algorithm that is better suited for my use case.

(I also hope this doesn't come across like a complete misuse of the framework) 😂

[DarioRomano]

I've now tried out the BDD and factorization algorithms, and it seems that for this specific model I'm trying to operate on, the space and time complexity is a bit higher than I hoped for. Running for half an hour, neither of the algorithms was able to finish conversion for the model in question. As it is not critical for me to use this model though, I can accept this limitation.