Author name cluster

Feifei Ma

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

14 papers

2 author rows

AAAI Conference 2026 Conference Paper

LLM-Guided Quantified SMT Solving over Uninterpreted Functions

Kunhang Lv
Yuhang Dong
Rui Han
Fuqi Jia
Feifei Ma
Jian Zhang

Quantified formulas with Uninterpreted Functions (UFs) over non-linear real arithmetic pose fundamental challenges for Satisfiability Modulo Theories (SMT) solving. Traditional quantifier instantiation methods struggle because they lack semantic understanding of UF constraints, forcing them to search through unbounded solution spaces with limited guidance. We present AquaForte, a framework that leverages Large Language Models to provide semantic guidance for UF instantiation by generating instantiated candidates for function definitions that satisfy the constraints, thereby significantly reducing the search space and complexity for solvers. Our approach preprocesses formulas through constraint separation, uses structured prompts to extract mathematical reasoning from LLMs, and integrates the results with traditional SMT algorithms through adaptive instantiation. AquaForte maintains soundness through systematic validation: LLM-guided instantiations yielding SAT solve the original problem, while UNSAT results generate exclusion clauses for iterative refinement. Completeness is preserved by fallback to traditional solvers augmented with learned constraints. Experimental evaluation on SMT-COMP benchmarks demonstrates that AquaForte solves numerous instances where state-of-the-art solvers like Z3 and CVC5 timeout, with particular effectiveness on satisfiable formulas. Our work shows that LLMs can provide valuable mathematical intuition for symbolic reasoning, establishing a new paradigm for SMT constraint solving.

PDF Details DOI

AAAI Conference 2025 Conference Paper

A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic

Fuqi Jia
Yuhang Dong
Rui Han
Pei Huang
Minghao Liu
Feifei Ma
Jian Zhang

Optimization Modulo Nonlinear Real Arithmetic, abbreviated as OMT(NRA), generally focuses on optimizing a given objective subject to quantifier-free Boolean combinations of primitive constraints, including Boolean variables, polynomial equations, and inequalities. It is widely applicable in areas like program verification, analysis, planning, and so on. The existing solver, OptiMathSAT, officially supporting OMT(NRA), employs an incomplete algorithm. We present a sound and complete algorithm, Optimization Cylindrical Algebraic Covering (OCAC), integrated within the Conflict-Driven Clause Learning (CDCL) framework, specifically tailored for OMT(NRA) problems. We establish the correctness and termination of CDCL(OCAC) and explore alternative approaches using cylindrical algebraic decomposition (CAD) and first-order formulations. Our work includes the development of the first complete OMT solver for NRA, demonstrating significant performance improvements. In benchmarks generated from SMT-LIB instances, our algorithm finds the optimum value in about 150% more instances compared to the current leading solver, OptiMathSAT.

PDF Details DOI

AAAI Conference 2023 Short Paper

Can Graph Neural Networks Learn to Solve the MaxSAT Problem? (Student Abstract)

Minghao Liu
Pei Huang
Fuqi Jia
Fan Zhang
Yuchen Sun
Shaowei Cai
Feifei Ma
Jian Zhang

The paper presents an attempt to bridge the gap between machine learning and symbolic reasoning. We build graph neural networks (GNNs) to predict the solution of the Maximum Satisfiability (MaxSAT) problem, an optimization variant of SAT. Two closely related graph representations are adopted, and we prove their theoretical equivalence. We also show that GNNs can achieve attractive performance to solve hard MaxSAT problems in certain distributions even compared with state-of-the-art solvers through experimental evaluation.

PDF Details DOI

NeurIPS Conference 2023 Conference Paper

Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning

Fuqi Jia
Yuhang Dong
Minghao Liu
Pei Huang
Feifei Ma
Jian Zhang

Cylindrical Algebraic Decomposition (CAD) is one of the pillar algorithms of symbolic computation, and its worst-case complexity is double exponential to the number of variables. Researchers found that variable order dramatically affects efficiency and proposed various heuristics. The existing learning-based methods are all supervised learning methods that cannot cope with diverse polynomial sets. This paper proposes two Reinforcement Learning (RL) approaches combined with Graph Neural Networks (GNN) for Suggesting Variable Order (SVO). One is GRL-SVO(UP), a branching heuristic integrated with CAD. The other is GRL-SVO(NUP), a fast heuristic providing a total order directly. We generate a random dataset and collect a real-world dataset from SMT-LIB. The experiments show that our approaches outperform state-of-the-art learning-based heuristics and are competitive with the best expert-based heuristics. Interestingly, our models show a strong generalization ability, working well on various datasets even if they are only trained on a 3-var random dataset. The source code and data are available at https: //github. com/dongyuhang22/GRL-SVO.

PDF Details

IJCAI Conference 2022 Conference Paper

AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis

Jiaxin Liang
Feifei Ma
Junping Zhou
Minghao Yin

All Solution SAT (AllSAT) is a variant of Propositional Satisfiability, which aims to find all satisfying assignments for a given formula. AllSAT has significant applications in different domains, such as software testing, data mining, and network verification. In this paper, observing that the lack of component analysis may result in more work for algorithms with non-chronological backtracking, we propose a DPLL-based algorithm for solving AllSAT problem, named AllSATCC, which takes advantage of component analysis to reduce work repetition caused by non-chronological backtracking. The experimental results show that our algorithm outperforms the state-of-the-art algorithms on most instances.

PDF Details DOI

JAIR Journal 2022 Journal Article

Improving Simulated Annealing for Clique Partitioning Problems

Jian Gao
Yiqi Lv
Minghao Liu
Shaowei Cai
Feifei Ma

The Clique Partitioning Problem (CPP) is essential in graph theory with a number of important applications. Due to its NP-hardness, efficient algorithms for solving this problem are very crucial for practical purposes, and simulated annealing is proved to be effective in state-of-the-art CPP algorithms. However, to make simulated annealing more efficient to solve large-scale CPPs, in this paper, we propose a new iterated simulated annealing algorithm. Several methods are proposed in our algorithm to improve simulated annealing. First, a new configuration checking strategy based on timestamp is presented and incorporated into simulated annealing to avoid search cycles. Afterwards, to enhance the local search ability of simulated annealing and speed up convergence, we combine our simulated annealing with a descent search method to solve the CPP. This method further improves solutions found by simulated annealing, and thus compensates for the local search effect. To further accelerate the convergence speed, we introduce a shrinking factor to decline initial temperature and then propose an iterated local search algorithm based on simulated annealing. Additionally, a restart strategy is adopted when the search procedure converges. Extensive experiments on benchmark instances of the CPP were carried out, and the results suggest that the proposed simulated annealing algorithm outperforms all the existing heuristic algorithms, including five state-of-the-art algorithms. Thus the best-known solutions for 34 instances out of 94 are updated. We also conduct comparative analyses of the proposed strategies and show their effectiveness.

PDF Details DOI

AAAI Conference 2022 Conference Paper

Word Level Robustness Enhancement: Fight Perturbation with Perturbation

Pei Huang
Yuting Yang
Fuqi Jia
Minghao Liu
Feifei Ma
Jian Zhang

State-of-the-art deep NLP models have achieved impressive improvements on many tasks. However, they are found to be vulnerable to some perturbations. In this paper, we design a robustness enhancement method to defend against word substitution perturbation, whose basic idea is to fight perturbation with perturbation. We find that: although many welltrained deep models are not robust in the setting of the presence of adversarial samples, they satisfy weak robustness. That means they can handle most non-crafted perturbations well. Taking advantage of the weak robustness property of deep models, we utilize non-crafted perturbations to resist the adversarial perturbations crafted by attackers. Our method contains two main stages. The first stage is using randomized perturbation to conform the input to the data distribution. The second stage is using randomized perturbation to eliminate the instability of prediction results and enhance the robustness guarantee. Experimental results show that our method can significantly improve the ability of deep models to resist the state-of-the-art adversarial attacks while maintaining the prediction performance on the original clean data.

PDF Details

SAT Conference 2021 Conference Paper

Efficient SAT-Based Minimal Model Generation Methods for Modal Logic S5

Pei Huang 0002
Rundong Li
Minghao Liu 0001
Feifei Ma
Jian Zhang 0001

Abstract Modal logic S5 is useful in various applications of artificial intelligence. In recent years, the advance in solving the satisfiability problem of S5 has allowed many large S5 formulas to be solved within a few minutes. In this context, a new challenge arises: how to generate a minimal S5 Kripke model efficiently? The minimal model generation can be useful for tasks such as model checking and debugging of logical specifications. This paper presents several efficient SAT-based methods and provides a symmetry-breaking technique for the minimal model generation problem of S5. Extensive experiments demonstrate that our methods are good at tackling many large instances and achieve state-of-the-art performances. We find that a minimal model of a large S5 formula is usually very small, and we analyze this phenomenon via a graph model. Due to this characteristic, our incremental method performs best in most cases, and we believe that it is more suitable for minimal S5 Kripke model generation.

Details

SAT Conference 2021 Conference Paper

Investigating the Existence of Costas Latin Squares via Satisfiability Testing

Jiwei Jin
Yiqi Lv
Cunjing Ge
Feifei Ma
Jian Zhang 0001

Abstract Costas Latin squares are important combinatorial structures in combinatorial design theory. Some Costas Latin squares are found in recent years, but there are still some open problems about the existence of Costas Latin squares with specified properties including idempotency, orthogonality, and certain quasigroup properties. In this paper, we describe an efficient method for solving these problems using state-of-the-art SAT solvers. We present new results of Costas Latin squares with specified properties of even order \(n \le 10\). It is found that within this order range, most Costas Latin squares with such properties don’t exist except for a few cases. The non-existence can be certified since SAT solvers can produce a formal proof. Experimental results demonstrate the effectiveness of our method.

Details

IJCAI Conference 2019 Conference Paper

Approximating Integer Solution Counting via Space Quantification for Linear Constraints

Cunjing Ge
Feifei Ma
Xutong Ma
Fan Zhang
Pei Huang
Jian Zhang

Solution counting or solution space quantification (means volume computation and volume estimation) for linear constraints (LCs) has found interesting applications in various fields. Experimental data shows that integer solution counting is usually more expensive than quantifying volume of solution space while their output values are close. So it is helpful to approximate the number of integer solutions by the volume if the error is acceptable. In this paper, we present and prove a bound of such error for LCs. It is the first bound that can be used to approximate the integer solution counts. Based on this result, an approximate integer solution counting method for LCs is proposed. Experiments show that our approach is over 20x faster than the state-of-the-art integer solution counters. Moreover, such advantage increases with the problem scale.

PDF Details

TCS Journal 2019 Journal Article

On some matching problems under the color-spanning model

Sergey Bereg
Feifei Ma
Wencheng Wang
Jian Zhang
Binhai Zhu

Given a set of n points Q in the plane, each colored with one of the k given colors, a color-spanning set S ⊂ Q is a subset of k points with distinct colors. The minimum diameter color-spanning set (MDCS) is a color-spanning set whose diameter is minimum. Somehow symmetrically, the largest closest pair color-spanning set (LCPCS) is a color-spanning set whose closest pair is the largest. Both MDCS and LCPCS have been shown to be NP-complete, but whether they are fixed-parameter tractable (FPT) when k is a parameter is open. Motivated by this question, we consider the FPT tractability of some matching problems under this color-spanning model, where 2k is the parameter. We show that the following three problems are polynomially solvable (hence FPT): (1) MinSum Matching Color-Spanning Set, (2) MaxMin Matching Color-Spanning Set, and (3) MinMax Matching Color-Spanning Set. For the k-Multicolored Independent Matching problem, namely, computing a matching of 2k vertices in a graph such that the vertices of the edges in the matching do not share edges, we show that it is W[1]-hard. Finally, motivated by this problem, which is related to the parameterized independent set problem, we are able to prove that LCPCS is W[1]-hard.

Details DOI

IJCAI Conference 2019 Conference Paper

Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring

Pei Huang
Minghao Liu
Ping Wang
Wenhui Zhang
Feifei Ma
Jian Zhang

Modal logic S5 has found various applications in artificial intelligence. With the advances in modern SAT solvers, SAT-based approach has shown great potential in solving the satisfiability problem of S5. The scale of the SAT encoding for S5 is strongly influenced by the upper bound on the number of possible worlds. In this paper, we present a novel SAT-based approach for S5 satisfiability problem. We show a normal form for S5 formulas. Based on this normal form, a conflict graph can be derived whose chromatic number provides an upper bound of the possible worlds and a lot of unnecessary search spaces can be eliminated in this process. A heuristic graph coloring algorithm is adopted to balance the efficiency and optimality. The number of possible worlds can be significantly reduced for many practical instances. Extensive experiments demonstrate that our approach outperforms state-of-the-art S5-SAT solvers.

PDF Details

TCS Journal 2018 Journal Article

Computing and estimating the volume of the solution space of SMT(LA) constraints

Cunjing Ge
Feifei Ma
Peng Zhang
Jian Zhang

The satisfiability modulo theories (SMT) problem is a decision problem, i. e. , deciding the satisfiability of logical formulas with respect to combinations of background theories (like reals, integers, arrays, bit-vectors). In this paper, we study the counting version of SMT with respect to linear arithmetic – SMT(LA), which generalizes both model counting and volume computation of convex polytopes. We describe a method for estimating the volume of convex polytopes based on the Multiphase Monte-Carlo method. It employs a new technique to reutilize random points, so that the number of random points can be significantly reduced. We prove that the reutilization technique has no side-effect on the error. We also investigate a simplified version of hit-and-run method: the coordinate directions method. Based on volume estimation method for polytopes, we present an approach to estimating the volume of the solution space of SMT(LA) formulas. It employs a heuristic strategy to accelerate the volume estimation procedure. In addition, we devise some specific techniques for instances that arise from program analysis.

Details DOI

SAT Conference 2012 Conference Paper

Faulty Interaction Identification via Constraint Solving and Optimization

Jian Zhang 0001
Feifei Ma
Zhiqiang Zhang 0007

Abstract Combinatorial testing (CT) is an important black-box testing method. In CT, the behavior of the system under test (SUT) is affected by several parameters/components. Then CT generates a combinatorial test suite. After the user executes a test suite and starts debugging, some test cases fail and some pass. From the perspective of a black box, the failures are caused by interaction of several parameters. It will be helpful if we can identify a small set of interacting parameters that caused the failures. This paper proposes a new automatic approach to identifying faulty interactions. It uses (pseudo-Boolean) constraint solving and optimization techniques to analyze the execution results of the combinatorial test suite. Experimental results show that the method is quite efficient and it can find faulty combinatorial interactions quickly. They also shed some light on the relation between the size of test suite and the ability of fault localization.

Details