Junping Zhou

AAAI Conference 2025 Conference Paper

DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem

• Jiaxin Liang
• Junping Zhou
• Minghao Yin

For many real-world problems, users are often interested not only in finding a single solution but in obtaining a sufficiently diverse collection of solutions. In this work, we consider the Diverse SAT problem, aiming to find a set of diverse satisfying assignments for a given propositional formula. We propose a novel and effective local search algorithm, DiverSAT, to solve the problem. To cope with diversity, we introduce three heuristics and a perturbation strategy based on some relevant information. We conduct extensive experiments on a large number of public benchmarks, collected from semiformal hardware verification, logistics planning, and other domains. The results show that DiverSAT outperforms the existing algorithms on most of these benchmarks.

AAAI Conference 2024 Short Paper

Enhance Diversified Top-k MaxSAT Solving by Incorporating New Strategy for Generating Diversified Initial Assignments (Student Abstract)

• Jiaxin Liang
• Junping Zhou
• Minghao Yin

The Diversified Top-k MaxSAT (DTKMS) problem is an extension of MaxSAT. The objective of DTKMS is to find k feasible assignments of a given formula, such that each assignment satisfies all hard clauses and the k assignments together satisfy the maximum number of soft clauses. This paper presents a local search algorithm, DTKMS-DIA, which incorporates a new approach to generating initial assignments. Experimental results indicate that DTKMS-DIA can achieve attractive performance on 826 instances compared with state-of-the-art solvers.

SAT Conference 2023 Conference Paper

LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem

• Junping Zhou
• Jiaxin Liang
• Minghao Yin
• Bo He

The Maximum Satisfiability (MaxSAT), an important optimization problem, has a range of applications, including network routing, planning and scheduling, and combinatorial auctions. Among these applications, one usually benefits from having not just one single solution, but k diverse solutions. Motivated by this, we study an extension of MaxSAT, named Diversified Top-k MaxSAT (DTKMS) problem, which is to find k feasible assignments of a given formula such that each assignment satisfies all hard clauses and all of them together satisfy the maximum number of soft clauses. This paper presents a local search algorithm, LS-DTKMS, for DTKMS problem, which exploits novel scoring functions to select variables and assignments. Experiments demonstrate that LS-DTKMS outperforms the top-k MaxSAT based DTKMS solvers and state-of-the-art solvers for diversified top-k clique problem.

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.

AAAI Conference 2011 Conference Paper

Hybrid Tractable Classes of Binary Quantified Constraint Satisfaction Problems

• Jian Gao
• Minghao Yin
• Junping Zhou

AAAI Conference 2010 Conference Paper

New Worst-Case Upper Bound for #2-SAT and #3-SAT with the Number of Clauses as the Parameter

• Junping Zhou
• Minghao Yin
• Chunguang Zhou

The rigorous theoretical analyses of algorithms for #SAT have been proposed in the literature. As we know, previous algorithms for solving #SAT have been analyzed only regarding the number of variables as the parameter. However, the time complexity for solving #SAT instances depends not only on the number of variables, but also on the number of clauses. Therefore, it is significant to exploit the time complexity from the other point of view, i. e. the number of clauses. In this paper, we present algorithms for solving #2-SAT and #3-SAT with rigorous complexity analyses using the number of clauses as the parameter. By analyzing the algorithms, we obtain the new worst-case upper bounds O(1. 1892m ) for #2-SAT and O(1. 4142m ) for #3-SAT, where m is the number of clauses.