English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We present Graph-$Q$-SAT, a branching heuristic for a Boolean SAT solvertrained with value-based reinforcement learning (RL) using Graph NeuralNetworks for function approximation. Solvers using Graph-$Q$-SAT are completeSAT solvers that either provide a satisfying assignment or proof ofunsatisfiability, which is required for many SAT applications. The branchingheuristics commonly used in SAT solvers make poor decisions during theirwarm-up period, whereas Graph-$Q$-SAT is trained to examine the structure ofthe particular problem instance to make better decisions early in the search.Training Graph-$Q$-SAT is data efficient and does not require elaborate datasetpreparation or feature engineering. We train Graph-$Q$-SAT using RL interfacingwith MiniSat solver and show that Graph-$Q$-SAT can reduce the number ofiterations required to solve SAT problems by 2-3X. Furthermore, it generalizesto unsatisfiable SAT instances, as well as to problems with 5X more variablesthan it was trained on. We show that for larger problems, reductions in thenumber of iterations lead to wall clock time reductions, the ultimate goal whendesigning heuristics. We also show positive zero-shot transfer behavior whentesting Graph-$Q$-SAT on a task family different from that used for training.While more work is needed to apply Graph-$Q$-SAT to reduce wall clock time inmodern SAT solving settings, it is a compelling proof-of-concept showing thatRL equipped with Graph Neural Networks can learn a generalizable branchingheuristic for SAT search.

Can $Q$-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?