» Experiments :: AIGER Synthesis Parallel - Legacy :: SOTA Solvers and VBS analysis

State-of-the-Art Solvers


Hold Ctrl to select multiple instances.
Filter instances
JS expression filter. Valid variables are name, FractionOfBinaryClauses, FractionOfNegativeLiteralsPerClauseEntropy, FractionOfNegativeLiteralsPerClauseMax, FractionOfNegativeLiteralsPerClauseMean, FractionOfNegativeLiteralsPerClauseMin, FractionOfNegativeLiteralsPerClauseVariationCoefficient, FractionOfNegativeVariablesEntropy, FractionOfNegativeVariablesMax, FractionOfNegativeVariablesMean, FractionOfNegativeVariablesMin, FractionOfNegativeVariablesVariationCoefficient, FractionOfPositiveLiteralsPerClauseEntropy, FractionOfPositiveLiteralsPerClauseMax, FractionOfPositiveLiteralsPerClauseMean, FractionOfPositiveLiteralsPerClauseMin, FractionOfPositiveLiteralsPerClauseVariationCoefficient, FractionOfPositiveVariablesEntropy, FractionOfPositiveVariablesMax, FractionOfPositiveVariablesMean, FractionOfPositiveVariablesMin, FractionOfPositiveVariablesVariationCoefficient, FractionOfTernaryClauses, FractionOfUnaryClauses, ClausesToVariablesRatio, ClausesToVariablesRatioCubic, ClausesToVariablesRatioQuadratic, LinearizedClausesToVariablesRatio, LinearizedClausesToVariablesRatioQuadratic, LinearizedClaustesToVariablesRatioCubic, NumberOfClauses, NumberOfVariables, VariablesToClausesRatio, VariablesToClausesRatioCubic, VariablesToClausesRatioQuadratic, ClauseNodeDegreesEntropy, ClauseNodeDegreesMax, ClauseNodeDegreesMean, ClauseNodeDegreesMin, ClauseNodeDegreesVariationCoefficient, VariableNodeDegreesEntropy, VariableNodeDegreesMax, VariableNodeDegreesMean, VariableNodeDegreesMin, VariableNodeDegreesVariationCoefficient, DegreeEntropy, DegreeMax, DegreeMean, DegreeMin, DegreeVariationCoefficient,
Example: (numAtoms >= 6000 && numAtoms <= 8000 && name.match(/k3/))
A solver is considered state-of-the-art if no other solver solves a strict superset of the instances it solves.
Unique solver contribution is the number of instances only solved by this solver.