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.

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.

Constraint programming (CP) is a crucial technology for solving real-world constraint optimization problems (COPs), with the advantages of rich modeling semantics and high solving efficiency.Using large language models (LLMs) to generate formal modeling automatically for COPs is becoming a promising approach, which aims to build trustworthy neuro-symbolic AI with the help of symbolic solvers.However, CP has received less attention compared to works based on operations research (OR) models.We introduce ConstraintLLM, the first LLM specifically designed for CP modeling, which is trained on an open-source LLM with multiinstruction supervised fine-tuning.We propose the Constraint-Aware Retrieval Module (CARM) to increase the in-context learning capabilities, which is integrated in a Tree-of-Thoughts (ToT) framework with guided selfcorrection mechanism.Moreover, we construct and release IndusCP, the first industriallevel benchmark for CP modeling, which contains 140 challenging tasks from various domains.Our experiments demonstrate that ConstraintLLM achieves state-of-the-art solving accuracy across multiple benchmarks and outperforms the baselines by 2x on the new IndusCP benchmark.

Deep neural networks can be vulnerable to adversarial attacks, even for the mainstream Transformer-based models. Although several robustness enhancement approaches have been proposed, they usually focus on some certain type of perturbation. As the types of attack can be various and unpredictable in practical scenarios, a general and strong defense method is urgently in require. We notice that most well-trained models can be weakly robust in the perturbation space, i.e., only a small ratio of adversarial examples exist. Inspired by the weak robust property, this paper presents a novel ensemble method for enhancing robustness. We propose a lightweight framework PAD to save computational resources in realizing an ensemble. Instead of training multiple models, a plugin module is designed to perturb the parameters of a base model which can achieve the effect of multiple models. Then, to diversify adversarial example distributions among different models, we promote each model to have different attention patterns via optimizing a diversity measure we defined. Experiments on various widely-used datasets and target models show that PAD can consistently improve the defense ability against many types of adversarial attacks while maintaining accuracy on clean data. Besides, PAD also presents good interpretability via visualizing diverse attention patterns.

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.

Nonlinear integer constraints are common and difficult in the verification and analysis of software/hardware. SMT(QF_NIA) generalizes such constraints, which is a boolean combination of nonlinear integer arithmetic constraints. A classical method to solve SMT(QF_NIA) is bit-blasting, which reduces them to boolean satisfiability problems. Currently, the existing pure bit-blasting based solvers are noncompetitive with other state-of-the-art SMT solvers. The bit-blasting based methods have some problems: First, the bit-blasting method is hampered by nonlinear multiplication operations; second, it sometimes does not search in a proper search space; and third, it contains some redundancy.

SMT (Satisfiability Modulo Theories) has been widely used in program verification, analysis, and test generation. But sometimes, SMT solver outputs incomprehensible solutions, especially for practical instances. Besides, due to the design of the deterministic algorithms, for a given formula, the result of each run is the same. In this paper, we concentrate on combining SMT solving with probability, which will instruct the SMT solver to give some plausible solutions. We define a special problem: PSMT, which allows solving an SMT instance with variables conforming to a certain distribution. We define distribution under constraint for PSMT, which is based on MCSAT (Model Constructing Satisfiability), a mainstream SMT-solving algorithm. We propose the Prob-MCSAT algorithm, which combines the MCSAT algorithm and introduces the probability to variables. The visualized examples show that the resulting assignments will form a clear trend based on Prob-SMT.

The satisfiability problem modulo the nonlinear real arithmetic (NRA) theory serves as the foundation for a wide range of important applications, such as model checking, program analysis, and software testing. However, due to the high computational complexity, developing efficient solving algorithms for this problem has consistently presented a substantial challenge. We present a hybrid SMT(NRA) solver, called NRAgo, which combines the efficiency of gradient-based optimization method with the completeness of algebraic solving algorithm. With our approach, the practical performance on many satisfiable instances is substantially improved. The experimental evaluation shows that NRAgo achieves remarkable acceleration effects on a set of challenging SMT(NRA) benchmarks that are hard to solve for state-of-the-art SMT solvers.

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.

State-of-the-art deep NLP models have achieved impressive improvements on many tasks. However, they are found to be vulnerable to some perturbations. Before they are widely adopted, the fundamental issues of robustness need to be addressed. 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 well-trained 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.

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.

Deep neural networks have been widely adopted for many real-world applications and their reliability has been widely concerned. This paper introduces a notion of ε-weakened robustness (briefly as ε-robustness) for analyzing the reliability and some related quality issues of deep neural networks. Unlike the conventional robustness, which focuses on the “perfect” safe region in the absence of adversarial examples, ε-weakened robustness focuses on the region where the proportion of adversarial examples is bounded by user-specified ε. The smaller the value of ε is, the less vulnerable a neural network is to be fooled by a random perturbation. Under such a robustness definition, we can give conclusive results for the regions where conventional robustness ignores. We propose an efficient testing-based method with user-controllable error bounds to analyze it. The time complexity of our algorithms is polynomial in the dimension and size of the network. So, they are scalable to large networks. One of the important applications of our ε-robustness is to build a robustness enhanced classifier to resist adversarial attack. Based on this theory, we design a robustness enhancement method with good interpretability and rigorous robustness guarantee. The basic idea is to resist perturbation with perturbation. Experimental results show that our robustness enhancement method can significantly improve the ability of deep models to resist adversarial attacks while maintaining the prediction performance on the original clean data. Besides, we also show the other potential value of ε-robustness in neural networks analysis.

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.

Recent works have made great progress in semantic segmentation by exploiting richer context, most of which are designed from a spatial perspective. In contrast to previous works, we present the concept of class center which extracts the global context from a categorical perspective. This class-level context describes the overall representation of each class in an image. We further propose a novel module, named Attentional Class Feature (ACF) module, to calculate and adaptively combine different class centers according to each pixel. Based on the ACF module, we introduce a coarse-to-fine segmentation network, called Attentional Class Feature Network (ACFNet), which can be composed of an ACF module and any off-the-shell segmentation network (base network). In this paper, we use two types of base networks to evaluate the effectiveness of ACFNet. We achieve new state-of-the-art performance of 81.85% mIoU on Cityscapes dataset with only finely annotated data used for training.

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.

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.

A collection of n-2 idempotent symmetric quasigroups of order n is called a golf design if all the quasigroups in the collection are mutually disjoint. Two golf designs are said to be orthogonal if any idempotent symmetric quasigroup from one golf design has an orthogonal mate in the other golf design, and it is also called an orthogonal golf design (OG(n)). The existence of orthogonal golf designs is an open problem in combinatorial design theory. In this paper, we describe a method for solving some open cases using automated reasoning tools, employing both symmetry breaking and heuristic decision. The experimental results show that our method is highly efficient and it indeed allowed us to get some positive results in reasonable time. In particular, we apply state-of-the-art SAT solvers and constraint solvers to decide the non-existence of some instances, which can produce a formal proof.

Network-on-Chip (NoC) is a promising interconnecting paradigm in the state-of-the-art multi-core architectures. Its communication network can increase the capacity of parallel data transfer such that system performance is improved. In the design of MPSoC-based applications, multiple objectives exist, such as minimizing time and energy consumption, which may conflict and certain trade-off needs to be evaluated. Heuristic-based methods such as evolutionary algorithms are always adopted to find near-optimal solutions for such applications. However, it is hard to evaluate the accuracy of those solutions. As most of the constraints on the mapping and scheduling process of NoCs can be described as logic formulas, we apply SMT-based methods for the multi-objective optimization of NoC-based MPSoCs. Moreover, to improve the scalability of the optimization problem, we propose to reduce the search space with respect to the symmetry feature of NoC architecture, and to decompose the search process according to the feature of non-dominated solutions. Extensive experimental results from random and real-case benchmarks demonstrate the accuracy of SMT-based methods in finding all the Pareto-fronts, and the efficiency of the proposed strategies.

MPSoCs are increasingly being adopted in the design of emerging complex embedded systems. Resource limitations require designers to find optimizations among various design considerations. Task mapping and scheduling become one of the key issues in designing such systems. To meet the requirements of makespan minimization and workload balance for energy-aware MPSoCs, the paper presents a unified formulation to find satisfied task mapping and scheduling solutions. The model considers both computation and communication cost, and enables applying dynamic power management (DPM) for energy optimization. To efficiently approximate the Pareto front of the optimization problem, we propose a multi-objective hybrid algorithm (MOHA) by integrating a Pareto local search into an evolutionary process, with a problem-specific initialization. Experimental results from realistic benchmarks demonstrate that the proposed techniques are able to generate high-quality solutions of realistic applications on the target architecture, compared with state-of-the-art methods.

The energy consumption problem is a hot topic in Android communities. The high energy cost caused by improper development brings lots of complaints from users. An effective and efficient energy consumption analysis technique can guide the developers to improve the energy efficiency of their apps. Existing researches on this problem focus on either system entity level that gives the energy consumption of the hardware, or source line level that calculates the energy cost of source codes. With the consideration of accuracy and cost of analysis, this paper proposes a lightweight and automatic approach to estimate the method-level energy consumption for Android apps. We construct a statistical model from a set of energy values obtained by Dalvik bytecode based instrumentation and software-based measurement, to predict the energy consumption of execution sequences of methods. The experiments on several real-world apps show that the proposed techniques have low overhead while persisting acceptable accuracy.

Software testing and analysis are very important research topics in software engineering. We are interested in improving the accuracy of analysis, as well as automation of test generation. In particular, we have been working on the automatic generation of small Orthogonal Arrays which can be used for combinatorial testing, and the computation of path execution frequency for a program path. The basic idea is to reduce the original problems to constraint satisfaction problems and develop effective constraint solving techniques for solving the problems.