G4satbench Eval

g4satbench-eval

G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks — Li et al. (2023) (arXiv:2309.16941, 2023)

What this evaluates

This benchmark evaluates the capability of Graph Neural Networks to solve Boolean satisfiability (SAT) problems. It probes whether GNNs can accurately predict formula satisfiability, generate satisfying variable assignments, and identify unsatisfiable cores, while assessing their ability to learn search heuristics from graph-structured logical representations.

Datasets

• G4SATBench — total ?; splits: train (-1), val (-1), test (-1); repo https://github.com/zhaoyu-li/G4SATBench

Metrics

• classification accuracy (primary) — range: [0, 1]
  • Fraction of correctly classified instances for satisfiability prediction (binary graph classification) and unsat-core variable prediction (binary node classification).
• solving accuracy — range: [0, 1]
  • Fraction of satisfiable instances where at least one of the model's predicted assignments satisfies the formula. Multiple predictions per instance are allowed and evaluated collectively.

Input / output format

Input: CNF formulas encoded as heterogeneous graphs (LCG* or VCG*), where nodes represent literals and clauses, and edges encode variable-clause membership and literal polarity.

Output: Binary label (1/0) for satisfiability prediction; binary label per variable for satisfying assignment and unsat-core variable prediction.

Scoring recipe

# Classification accuracy (SAT/unsat & core)
correct = sum(1 for p, g in zip(predictions, gold) if p == g)
accuracy = correct / len(gold)

# Solving accuracy (assignment)
solved = 0
for inst, preds_inst in zip(instances, all_predictions):
    if any(satisfies_formula(inst, a) for a in preds_inst):
        solved += 1
solving_accuracy = solved / len(instances)

Common pitfalls

• Solving accuracy counts an instance as solved if any of the model's predicted assignments satisfies the formula, not just the first or highest-confidence one.
• GNNs are evaluated on static graph classification/node prediction tasks rather than dynamic search steps, meaning they cannot directly model backtracking (CDCL) search dynamics despite being used in neural-guided solvers.
• Graph encodings must use the refined LCG* or VCG* variants (with polarity edges) rather than standard LIG/VIG/LCG/VCG to avoid losing critical logical information required for optimal GNN construction.

Evidence (verbatim from paper)

For satisfiability prediction and unsat-core variable prediction, we report the classification accuracy of each GNN model in G4SATBench. For satisfying assignment prediction, we report the solving accuracy of the predicted assignments. If multiple assignments are predicted for a SAT instance, the instance is considered solved if any of the predictions satisfy the formula.

Citation

@misc{li2023g4satbench,
  title={G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks},
  author={Li et al. (2023)},
  year={2023},
  note={arXiv:2309.16941}
}

• arXiv: 2309.16941