Jingchao Chen

Zeyan Wang, Zhengmao Liu, Yongxin Cai et al.

Federated Unlearning (FU) aims to efficiently remove the influence of specific client data from a federated model while preserving utility for the remaining clients. However, three key challenges remain: (1) existing unlearning objectives often compromise model utility or increase vulnerability to Membership Inference Attacks (MIA); (2) there is a persistent conflict between forgetting and utility, where further unlearning inevitably harms retained performance; and (3) support for concurrent multi-client unlearning is poor, as gradient conflicts among clients degrade the quality of forgetting. To address these issues, we propose FUPareto, an efficient unlearning framework via Pareto-augmented optimization. We first introduce the Minimum Boundary Shift (MBS) Loss, which enforces unlearning by suppressing the target class logit below the highest non-target class logit; this can improve the unlearning efficiency and mitigate MIA risks. During the unlearning process, FUPareto performs Pareto improvement steps to preserve model utility and executes Pareto expansion to guarantee forgetting. Specifically, during Pareto expansion, the framework integrates a Null-Space Projected Multiple Gradient Descent Algorithm (MGDA) to decouple gradient conflicts. This enables effective, fair, and concurrent unlearning for multiple clients while minimizing utility degradation. Extensive experiments across diverse scenarios demonstrate that FUPareto consistently outperforms state-of-the-art FU methods in both unlearning efficacy and retained utility.

Jingchao Chen, Shiyi Mu, Shugong Xu et al.

Although lots of progress were made in Text Recognition/OCR in recent years, the task of font recognition is remaining challenging. The main challenge lies in the subtle difference between these similar fonts, which is hard to distinguish. This paper proposes a novel font recognizer with a pluggable module solving the font recognition task. The pluggable module hides the most discriminative accessible features and forces the network to consider other complicated features to solve the hard examples of similar fonts, called HE Block. Compared with the available public font recognition systems, our proposed method does not require any interactions at the inference stage. Extensive experiments demonstrate that HENet achieves encouraging performance, including on character-level dataset Explor_all and word-level dataset AdobeVFR

Jingchao Chen

The robustness and correctness of SAT solvers are receiving more and more attention. In recent SAT competitions, a proof of unsatisfiability emitted by SAT solvers must be checked. So far, no proof checker has been efficient for every case. In the SAT competition 2016, some proofs were not verified within 20000 seconds. For this reason, we decided to develop a more efficient proof checker called TreeRat. This new checker uses a window shifting technique to improve the level of efficiency at which it verifies proofs of unsatisfiability. At the same time, we suggest that tree-search-based SAT solvers should use an equivalent relation encoding to emit proofs of subproblems. In our experiments, TreeRat was able to verify almost all proofs within 20000 seconds. On this point, TreeRat is shown to be superior to gratgen, which is an improved version of DRAT-trim. Also, in most cases, TreeRat is faster than gratgen. Like DRAT-trim, TreeRat can output also trace dependency graphs. Its output format is LRAT. The correctness of TreeRat can be ensured by checking its LRAT output.

Jingchao Chen

We improve further the 2015 version of abcdSAT by various heuristics such as at-least-one recently used strategy, learnt clause database approximation reduction etc. Based on the requirement of different tracks at the SAT Competition 2016, we develop three versions of abcdSAT: drup, inc and lim, which participate in the competition of main (agile), incremental library and no-limit track, respectively.

Jingchao Chen

The decision variable selection policy used by the most competitive CDCL (Conflict-Driven Clause Learning) SAT solvers is either VSIDS (Variable State Independent Decaying Sum) or its variants such as exponential version EVSIDS. The common characteristic of VSIDS and its variants is to make use of statistical information in the solving process, but ignore structure information of the problem. For this reason, this paper modifies the decision variable selection policy, and presents a SAT solving technique based on BCD (Blocked Clause Decomposition). Its basic idea is that a part of decision variables are selected by VSIDS heuristic, while another part of decision variables are selected by blocked sets that are obtained by BCD. Compared with the existing BCD-based technique, our technique is simple, and need not to reencode CNF formulas. SAT solvers for certified UNSAT track can apply also our BCD-based technique. Our experiments on application benchmarks demonstrate that the new variables selection policy based on BCD can increase the performance of SAT solvers such as abcdSAT. The solver with BCD solved an instance from the SAT Race 2015 that was not solved by any solver so far. This shows that in some cases, the heuristic based on structure information is more efficient than that based on statistical information.

Jingchao Chen

The phase selection is an important of a SAT Solver based on conflict-driven DPLL. This paper presents a new phase selection strategy, in which the weight of each literal is defined as the sum of its implied-literals static weights. The implied literals of each literal is computed dynamically during the search. Therefore, it is call a dynamic phase selection strategy. In general, computing dynamically a weight is time-consuming. Hence, so far no SAT solver applies successfully a dynamic phase selection. Since the implied literal of our strategy conforms to that of the search process, the usual two watched-literals scheme can be applied here. Thus, the cost of our dynamic phase selection is very low. To improve Glucose 2.0 which won a Gold Medal for application category at SAT 2011 competition, we build five phase selection schemes using the dynamic phase selection policy. On application instances of SAT 2011, Glucose improved by the dynamic phase selection is significantly better than the original Glucose. We conduct also experiments on Lingeling, using the dynamic phase selection policy, and build two phase selection schemes. Experimental results show that the improved Lingeling is better than the original Lingeling.