fuqi-jia

benchmark-submission

Git repository for the submission of SMT-LIB benchmarks

BLAN

Bit-bLAsting solving Non-linear integer constraints.

cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

fuqi-jia.github.io

Homepage

GRL-SVO

This project proposes two Reinforcement Learning (RL) approaches combined with Graph Neural Networks (GNN) for Suggesting Variable Order (SVO).

math_puzzles_smtlib_generator

Some discrete math puzzles described via SMTLIB v2.6.

OMT_NRA_Benchmark

A collection of classical OMT(NRA) instances.

prob-smt

pytorch-tutorial

PyTorch示例代码；复现GNN模型

Splitwise-MILP

The Splitwise-like algorithm using MILP encoding.

fuqi-jia/BLAN

Bit-bLAsting solving Non-linear integer constraints.

fuqi-jia/GRL-SVO

This project proposes two Reinforcement Learning (RL) approaches combined with Graph Neural Networks (GNN) for Suggesting Variable Order (SVO).

fuqi-jia/Splitwise-MILP

The Splitwise-like algorithm using MILP encoding.

fuqi-jia/benchmark-submission

Git repository for the submission of SMT-LIB benchmarks

fuqi-jia/cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

fuqi-jia/fuqi-jia.github.io

Homepage

fuqi-jia/math_puzzles_smtlib_generator

Some discrete math puzzles described via SMTLIB v2.6.

fuqi-jia/OMT_NRA_Benchmark

A collection of classical OMT(NRA) instances.

fuqi-jia/prob-smt

fuqi-jia/pytorch-tutorial

PyTorch示例代码；复现GNN模型

fuqi-jia/Yices-ismt

fuqi-jia/Yices-ismt-description

fuqi-jia/AAAI25

Code, dataset and appendix for the AAAI25 paper

fuqi-jia/smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.