SMT sampling refers to the task of generating a set of satisfying assignments (samples) for a given SMT formula. An effective SMT sampler should be capable of producing samples with high diversity to maximize coverage of the solution space. However, most SMT samplers struggle to adequately cover the solution space and fail to generate sufficiently diverse solutions. To address these limitations, we propose $$ HighDiv $$ , the first iterative sampling framework that integrates CDCL(T) and local search in a bidirectional guided manner. During the bidirectional guidance process, solutions generated by CDCL(T) guide the variable initialization of the local search. Conversely, solutions produced by the local search guide CDCL(T) to further explore the solution space. Additionally, we design a novel local search algorithm, Context-Constrained Stochastic Search (CCSS), which introduces the Constraint-Partitioned Variable Initialization and the boundary-aware move operator. These components effectively balance exploration and feasibility throughout the search process. We conduct an extensive evaluation on QF_LIA formulas from the SMT-LIB benchmark. The results demonstrate that $$ HighDiv $$ achieves substantial improvements in diversity over the state-of-the-art SMT sampling tools.

Abstract Knowledge compilation (KC) involves compiling propositional constraints into tractable target languages which in turn efficiently support multiple analyses or queries of the constraints. Solving these queries plays a crucial role in the synthesis and verification of hardware and software systems. Recently, we proposed the target language, Constrained Conjunction & Decision Diagrams (CCDD), experimentally shown to be promising for individual model counting queries. Here, we present the compiler, $$\textsf{Panini}$$ Panini , which compiles CNF into CCDD. $$\textsf{Panini}$$ Panini supports a range of queries. We present an empirical evaluation focusing on two fundamental queries, uniform sampling and (multiple) model counting, with a wide range of applications. While counting and sampling have witnessed significant performance improvements over the years, scalability still remains the primary challenge. Our evaluation over 600 instances from model counting competitions 2022–2024 show that $$\textsf{Panini}$$ Panini achieves state of art compilation by solving 322 instances, which is 183, 148, and 38 more than Dsharp, miniC2D, and D4 respectively. Secondly, on repetitive tasks, $$\textsf{Panini}$$ Panini solves 53 and 50 more instances than ExactMC and SharpSAT-TD for model counting, and 175 and 132 more instances than SPUR and KUS for uniform sampling, respectively.

Quantitative information flow analyses (QIF) are a class of techniques for measuring the amount of confidential information leaked by a program to its public outputs. Shannon entropy is an important method to quantify the amount of leakage in QIF. This paper focuses on the programs modeled in Boolean constraints and optimizes the two stages of the Shannon entropy computation to implement a scalable precise tool PSE. In the first stage, we design a knowledge compilation language called ADD[∧] that combines Algebraic Decision Diagrams and conjunctive decomposition. ADD[∧] avoids enumerating possible outputs of a program and supports tractable entropy computation. In the second stage, we optimize the model counting queries that are used to compute the probabilities of outputs. We compare PSE with the state-of-the-art probabilistic approximately correct tool EntropyEstimation, which was shown to significantly outperform the previous precise tools. The experimental results demonstrate that PSE solved 56 more benchmarks compared to EntropyEstimation in a total of 459. For 98% of the benchmarks that both PSE and EntropyEstimation solved, PSE is at least 10× as efficient as EntropyEstimation.

Pseudo-Boolean model counting involves computing the number of satisfying assignments of a given pseudo-Boolean (PB) formula. In recent years, PB model counting has seen increased interest partly owing to the succinctness of PB formulas over typical propositional Boolean formulas in conjunctive normal form (CNF) at describing problem constraints. In particular, the research community has developed tools to tackle exact PB model counting. These recently developed counters follow one of the two existing major designs for model counters, namely the bottom-up model counter design. A natural question would be whether the other major design, the top-down model counter paradigm, would be effective at PB model counting, especially when the top-down design offered superior performance in CNF model counting literature. In this work, we investigate the aforementioned top-down design for PB model counting and introduce the first exact top-down PB model counter, PBMC. PBMC is a top-down search-based counter for PB formulas, with a new variable decision heuristic that considers variable coefficients. Through our evaluations, we highlight the superior performance of PBMC at PB model counting compared to the existing state-of-the-art counters PBCount, PBCounter, and Ganak. In particular, PBMC could count for 1849 instances while the next-best competing method, PBCount, could only count for 1773 instances, demonstrating the potential of a top-down PB counter design.

Propositional model counting is the problem of computing the satisfying assignments count of a given CNF formula. Due to the weak solving ability of the existing exact model counters in large-scale problems, approximate model counting has been proposed as a practical alternative to exact model counting. Most of the best current approaches are based on XOR constraints for approximate model counting, also known as the hashing-based method. In this paper, a new approximate model counter using short XOR constraints is proposed, which integrates bounded solving and controllable randomisation. By constantly adding short XOR constants, the solution space has been reduced to a smaller one. However, a smaller scale of solution space may result in worse result accuracy. Therefore, by limiting the scale of solution space that applies XOR constraints, bounded solving effectively increases the accuracy of a model counter. Controllable randomisation makes use of backbone variables and the constraint level among variables, such that the short XOR constraints can reach the same reduction effect on solution space as the long ones. It improves the quality of XOR constraints as well as the SAT solving efficiency. Experimentally, we demonstrate that in almost every benchmark used in well-known ApproxMC2 and STAC_CNF, our approach outperforms the existing approximate model counters in both accuracy and efficiency.

Digital twins (DT) and mobile networks have evolved forms of intelligence in Internet of Things (IoT). In this work, we consider a Digital Twin Mobile Network (DTMN) scenario with few multimedia samples. Facing challenges of knowledge extraction with few samples, stable interaction with dynamic changes of multimedia data, time and privacy saving in low-resource mobile network, we propose an edge computing and few-shot learning featured intelligent framework. Considering time-sensitive property of transmission and privacy risks of directly uploads in mobile network, we deploy edge computing to locally run networks for analysis, thus saving time to offload computing request and enhancing privacy by encrypting original data. Inspired by remarkable relationship representation of graphs, we build Graph Neural Network (GNN) in cloud to map physical mobile systems to virtual entities with DT, thus performing semantic inferences in cloud with few samples uploaded by edges. Occasionally, node features in GNN could converge to similar, non-discriminative embeddings, causing catastrophic unstable phenomena. An iterative reweight and drop structure (IRDS) is thus constructed in cloud, which nonetheless contributes stability with respect to edge uncertainty. As part of IRDS, a drop Edge&Node scheme is proposed to randomly remove certain nodes and edges, which not only enhances distinguished capability of graph neighbor patterns, but also offers data encryption with random strategy. We show one implementation case of image classification in social network, where experiments on public datasets show that our framework is effective with user-friendly advantages and significant intelligence.

Model counting is a fundamental problem which has been influential in many applications, from artificial intelligence to formal verification. Due to the intrinsic hardness of model counting, approximate techniques have been developed to solve real-world instances of model counting. This paper designs a new anytime approach called PartialKC for approximate model counting. The idea is a form of partial knowledge compilation to provide an unbiased estimate of the model count which can converge to the exact count. Our empirical analysis demonstrates that PartialKC achieves significant scalability and accuracy over prior state-of-the-art approximate counters, including satss and STS. Interestingly, the empirical results show that PartialKC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters.

Deep learning methods have shown significant performance in medical image analysis tasks. However, they generally act like ”black box” without explanations in both feature extraction and decision processes, leading to lack of clinical insights and high risk assessments. To aid deep learning in envisioning diseases with visual clues, we propose Representation Group-Disentangling Network (RGD-Net), which can completely disentangle feature space of input X-ray images into several independent feature groups, each corresponding to a specific disease. Taking several semantically related and labeled X-ray images as input, RGD-Net firstly extracts completely group-disentangled representations of diseases through Group-Disentangle Module, which applies group-swap and linking operations to construct latent space by enforcing semantic consistency of attributes. To prevent learning degenerate representations defined as shortcut problem, we further introduce adversarial constricts on mapping from features to diseases, thus avoiding model collapse with former free-form disentanglement. Experiments on chestxray-14 and ChestXpert datasets demonstrate that RGD-Net are effective in predicting diseases with remarkable advantages, which leverage potential factors contributing to different diseases, thus enhancing interpretability in working patterns of deep learning methods.

The past two decades have seen the significant improvements of the scalability of practical model counters, which have been quite influential in many applications from artificial intelligence to formal verification. While most of exact counters fall into two categories, search-based and compilation-based, Huang and Darwiche's remarkable observation ties these two categories: the trace of a search-based exact model counter corresponds to a Decision-DNNF formula. Taking advantage of literal equivalences, this paper designs an efficient model counting technique such that its trace is a generalization of Decision-DNNF formula. We first propose a generalization of Decision-DNNF, called CCDD, to capture literal equivalences, then show that CCDD supports model counting in linear time, and finally design a model counter, called ExactMC, whose trace corresponds to CCDD. We perform an extensive experimental evaluation over a comprehensive set of benchmarks and conduct performance comparison of ExactMC vis-a-vis the state of the art counters, c2d, Dsharp, miniC2D, D4, ADDMC, and Ganak. Our empirical evaluation demonstrates ExactMC can solve 885 instances while the prior state of the art could solve only 843 instances, representing a significant improvement of 42 instances.

We identify two families of canonical representations called ROBDD[/\i^]_C and ROBDD[/\T^,i]_T by augmenting ROBDD with two types of conjunctive decompositions. These representations cover the three existing languages ROBDD, ROBDD with as many implied literals as possible (ROBDD-L_&infin), and AND/OR BDD. We introduce a new time efficiency criterion called rapidity which reflects the idea that exponential operations may be preferable if the language can be exponentially more succinct. Then we demonstrate that the expressivity, succinctness and operation rapidity do not decrease from ROBDD[/\T^,i]_T to ROBDD[/\i^]_C, and then to ROBDD[/\i+1^]_C. We also demonstrate that ROBDD[/\i^]_C (i > 1) and ROBDD[/\T^,i]_T are not less tractable than ROBDD-L_&infin and ROBDD, respectively. Finally, we develop a compiler for ROBDD[/\&infin^]_C which significantly advances the compiling efficiency of canonical representations.

We identify two families of canonical knowledge compilation languages. Both families augment ROBDD with conjunctive decomposition bounded by an integer i ranging from 0 to ∞. In the former, the decomposition is finest and the decision respects a chain C of variables, while both the decomposition and decision of the latter respect a tree T of variables. In particular, these two families cover the three existing languages ROBDD, ROBDD with as many implied literals as possible, and AND/OR BDD. We demonstrate that each language in the first family is complete, while each one in the second family is incomplete with expressivity that does not decrease with incremental i. We also demonstrate that the succinctness does not decrease from the i-th language in the second family to the i-th language in the first family, and then to the (i+1)-th language in the first family. For the operating efficiency, on the one hand, we show that the two families of languages support a rich class of tractable logical operations, and particularly the tractability of each language in the second family is not less than that of ROBDD; and on the other hand, we introduce a new time efficiency criterion called rapidity which reflects the idea that exponential operations may be preferable if the language can be exponentially more succinct, and we demonstrate that the rapidity of each operation does not decrease from the i-th language in the second family to the i-th language in the first family, and then to the (i+1)-th language in the first family. Furthermore, we develop a compiler for the last language in the first family (i = ∞). Empirical results show that the compiler significantly advances the compiling efficiency of canonical representations. In fact, its compiling efficiency is comparable with that of the state-of-the-art compilers of non-canonical representations. We also provide a compiler for the i-th language in the first family by translating the last language in the first family into the i-th language (i < ∞). Empirical results show that we can sometimes use the i-th language instead of the last language without any obvious loss of space efficiency.