Research

There is a growing concern on algorithm fairness, according to wider adoption of machine learning techniques in our daily life. Testing of individual fairness is an approach to algorithm fairness concern. Verification Based Testing (VBT) is a state-of-the-art testing technique for individual fairness, that leverages verification techniques using constraint solving. In this paper, we develop a black-box individual fairness testing technique Vbt-X, which applies hash-based sampling techniques to the test case generation part of Vbt, aiming to improve its testing ability. Our evaluation by experiments confirms that Vbt-X improves the testing ability of Vbt by 2.92 times in average.

The conflict-driven clause learning (CDCL) is a standard algorithmic framework on which almost state-of-the-art SAT solvers are based. During the solving process of the CDCL solver, many learnt clauses are generated, and those turned out to be useless in terms of some criteria are removed. Since the decision commonly relies on heuristics, the same clauses can appear multiple times. Hence, the evaluation of the learnt clause utility has a significant impact on the solver’s performance. The recently proposed DL heuristic determines the utility in terms of the number of times clauses are generated. To improve this, we introduce the similarity of learnt clauses and propose a similarity-based clause management method. In experiments we compared our method with the DL, both implemented on top of CaDiCal, and we confirmed that our method outperforms the DL as well as the intact CaDiCal in both PAR-2 scores and the number of solved instances.