The alldifferent constraint is one of the most essential global constraints that has been used to model many classic Constraint Satisfaction Problems (CSPs). To tackle this constraint, previous work generally focuses on proposing filtering algorithms to reduce the value domain of variables, thereby pruning the backtracking search. However, due to the inherent complexity of alldifferent constraints, it remains challenging to solve CSPs containing large-scale alldifferent constraints for the existing search-based solvers. In this paper, we propose an efficient local search algorithm, called AllDiff-LS. We first represent the set of alldifferent constraints as graphs and simplify the graphs by two polynomial-time reduction rules. Afterward, we propose a new two-step strategy for selecting moves, as well as the carefully crafted tabu and restart strategies, to enable the algorithm to explore the search space more efficiently. Experiments on a representative set of benchmarks show that AllDiff-LS successfully solves more instances compared with state-of-the-art complete and heuristic methods, especially on large-scale instances, with much less running time.

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.

The equitable p-coloring problem involves dividing the vertices of a graph into p separate color sets, ensuring that the sizes of any two sets differ by at most one. In practical applications, the size of the color class produced by traditional graph coloring can vary significantly, which may lead to suboptimal outcomes in scheduling problems. It has led to extensive research on the equitable coloring problem. The goal is to determine the smallest value of p (equitable chromatic number) required to achieve equitable p-coloring for a given graph. This paper introduces a new three-stage approach to address this problem. The approach begins by obtaining an initial solution, then utilizes Integer Linear Programming (ILP) formulations to encode the properties of equitable coloring and iteratively solve these formulations using ILP solvers. Finally, SAT formulations are employed to enhance the results obtained from ILP solvers. We propose three techniques to improve solving efficiency, including Clique Extracting, Fixed Mapping, and Unsorted Formula. The first technique aims to acquire a better initial solution, while the latter two techniques reduce the search space for ILP and SAT solvers. Computational experiments demonstrate that our approach outperforms the state-of-the-art algorithm proposed by [ 1]. We improve the lower bound of the equitable chromatic number on almost half of the benchmark instances, and get the same results on the remaining instances except one.

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 multi-instruction 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 self-correction mechanism. Moreover, we construct and release IndusCP, the first industrial-level 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. Code and data are available at: https://github.com/william4s/ConstraintLLM.

Automated reasoning is a symbolic algorithmic technique that aims to simulate the logical reasoning ability of human.The overall goal is to mechanize different forms of reasoning with a computer system.Although the theoretical framework of the field has not yet supported the simulation of the full range of human reasoning capabilities,developments in the field have reached a point where automated reasoning programs are being used by researchers to attack open problems in mathematics and logic and provide important applications in computing science.This paper briefly reviews common approaches of automatic reasoning in dealing with open problems in combinatorial mathematics and highlights the latest developments in this field in China and abroad.Then the strengths and weaknesses of various approaches are analyzed,and reasoning strategies that have emerged in recent years to enhance the trustworthiness of automated reasoning results are introduced.Finally,future research directions and challenges are discussed.

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.

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.

Grain number per spike (GNS) is a pivotal determinant of grain yield in wheat. Pubing 3228 (PB3228), a wheat-Agropyron cristatum germplasm, exhibits a notably higher GNS. In this study, we developed a recombinant inbred line (RIL) population derived from PB3228/Gao8901 (PG-RIL) and constructed a high-density genetic map comprising 101,136 loci, spanning 4357.3 cM using the Wheat 660 K SNP array. The genetic map demonstrated high collinearity with the wheat assembly IWGSC RefSeq v1.0. Traits related to grain number and spikelet number per spike were evaluated in seven environments for quantitative trait locus (QTL) analysis. Five environmentally stable QTLs were detected in at least three environments. Among these, two major QTLs, QGns-4A.2 and QGns-1A.1, associated with GNS, exhibited positive alleles contributed by PB3228. Further, the conditional QTL analysis revealed a predominant contribution of PB3228 to the GNS QTLs, with both grain number per spikelet (GNSL) and spikelet number per spike (SNS) contributing to the overall GNS trait. Four kompetitive allele-specific PCR (KASP) markers that linked to QGns-4A.2 and QGns-1A.1 were developed and found to be effective in verifying the QTL effect within a diversity panel. Compared to previous studies, QGns-4A.2 exhibited stability across different trials, while QGns-1A.1 represents a novel QTL. The results from unconditional and conditional QTL analyses are valuable for dissecting the genetic contribution of the component traits to GNS at the individual QTL level and for understanding the genetic basis of the superior grain number character in PB3228. The KASP markers can be utilized in marker-assisted selection for enhancing GNS. Five environmentally stable QTLs related to grain number and spikelet number per spike were identified. PB3228 contributed to the majority of the QTLs associated with GNS.

Holey Latin square (HLS) is a special combinatorial design of interest to mathematicians and is helpful in the construction of many important structures in design theory. In this paper, we investigate the existence of HLSs satisfying the seven kinds of identities with automated reasoning techniques. We formulate this problem as propositional logic formulae. Since state-of-the-art SAT solvers have difficulty solving many HLS problems, we further propose a symmetry breaking method, called partially ordered HLS (POHLS), to eliminate isomorphic solutions. We have achieved the following goals through experimental evaluation. First, we have solved a dozen of open problems interested by mathematicians. Second, we identify the impact of different encodings. Third, we demonstrate the advantages of SAT solver over other FOL-based solvers. Fourth, we show that the proposed POHLS reduction can improve the efficiency of solving and find the complementarity between two types of symmetry breaking techniques.

Recent years have seen the wide application of natural language processing (NLP) models in crucial areas such as finance, medical treatment, and news media, raising concerns about the model robustness and vulnerabilities. We find that prompt paradigm can probe special robust defects of pre-trained language models. Malicious prompt texts are first constructed for inputs and a pre-trained language model can generate adversarial examples for victim models via mask-filling. Experimental results show that prompt paradigm can efficiently generate more diverse adversarial examples besides synonym substitution. Then, we propose a novel robust training approach based on prompt paradigm which incorporates prompt texts as the alternatives to adversarial examples and enhances robustness under a lightweight minimax-style optimization framework. Experiments on three real-world tasks and two deep neural models show that our approach can significantly improve the robustness of models to resist adversarial attacks.

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. In this paper, we focus on improving the efficiency of bit-blasting based method. To decide on a proper search space, we proposed an adaptive function for hard nonlinear multiplications, and heuristic strategies to analyze specific constraints. We also found that different orders in successive additions will result in bit vectors with different bit-widths. We proposed an optimal order decision algorithm to save redundancy in successive additions. We implement a solver with the proposed methods named BLAN. Experiments demonstrate that BLAN outperforms other state-of-the-art SMT solvers (APROVE, CVC5, MATHSAT, YICES2, Z3) on the satisfiable SMT(QF_NIA) instances in SMT-LIB. We provide an outlook of BLAN on solving unsatisfiable instances via combining with other solvers. Sensitivity analysis also demonstrates the effectiveness of the proposed methods.

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.

With the rapid development of deep learning techniques, various recent work has tried to apply graph neural networks (GNNs) to solve NP-hard problems such as Boolean Satisfiability (SAT), which shows the potential in bridging the gap between machine learning and symbolic reasoning. However, the quality of solutions predicted by GNNs has not been well investigated in the literature. In this paper, we study the capability of GNNs in learning to solve Maximum Satisfiability (MaxSAT) problem, both from theoretical and practical perspectives. We build two kinds of GNN models to learn the solution of MaxSAT instances from benchmarks, and show that GNNs have attractive potential to solve MaxSAT problem through experimental evaluation. We also present a theoretical explanation of the effect that GNNs can learn to solve MaxSAT problem to some extent for the first time, based on the algorithmic alignment theory.

IntroductionIdentification of stable major quantitative trait loci (QTLs) for yield-related traits is important for yield potential improvement in wheat breeding.MethodsIn the present study, we genotyped a recombinant inbred line (RIL) population using the Wheat 660K SNP array and constructed a high-density genetic map. The genetic map showed high collinearity with the wheat genome assembly. Fourteen yield-related traits were evaluated in six environments for QTL analysis.Results and DiscussionA total of 12 environmentally stable QTLs were identified in at least three environments, explaining up to 34.7% of the phenotypic variation. Of these, QTkw-1B.2 for thousand kernel weight (TKW), QPh-2D.1 (QSl-2D.2/QScn-2D.1) for plant height (PH), spike length (SL) and spikelet compactness (SCN), QPh-4B.1 for PH, and QTss-7A.3 for total spikelet number per spike (TSS) were detected in at least five environments. A set of Kompetitive Allele Specific PCR (KASP) markers were converted based on the above QTLs and used to genotype a diversity panel comprising of 190 wheat accessions across four growing seasons. QPh-2D.1 (QSl-2D.2/QScn-2D.1), QPh-4B.1 and QTss-7A.3 were successfully validated. Compared with previous studies, QTkw-1B.2 and QPh-4B.1 should be novel QTLs. These results provided a solid foundation for further positional cloning and marker-assisted selection of the targeted QTLs in wheat breeding programs.

Deep-learning-based NLP models are found to be vulnerable to word substitution perturbations. Before they are widely adopted, the fundamental issues of robustness need to be addressed. Along this line, we propose a formal framework to evaluate word-level robustness. First, to study safe regions for a model, we introduce robustness radius which is the boundary where the model can resist any perturbation. As calculating the maximum robustness radius is computationally hard, we estimate its upper and lower bound. We repurpose attack methods as ways of seeking an upper bound and design a pseudo-dynamic programming algorithm for a tighter upper bound. Then verification method is utilized for a lower bound. Further, for evaluating the robustness of regions outside a safe radius, we reexamine robustness from another view: quantification. A robustness metric with a rigorous statistical guarantee is introduced to measure the quantification of adversarial examples, which indicates the model’s susceptibility to perturbations outside the safe radius. The metric helps us figure out why state-of-the-art models like BERT can be easily fooled by a few word substitutions, but generalize well in the presence of real-world noises.

Additional file 1: Table S1. Marker sequences for map construction and marker-assisted selection.

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.

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.