问卷考试系统设计（四）：质量控制——测谎题、Z3 组卷验证与异常检测

public LieScaleResult calculate(List<Question> lieScaleQuestions,
                                 Map<String, Answer> answers) {
    int totalLieScore = 0;
    for (Question q : lieScaleQuestions) {
        Answer answer = answers.get(q.getId());
        if (answer == null) continue;

        int value = answer.getSelectedValue();
        if (q.getLieAnswerValues().contains(value)) {
            totalLieScore++;
        }
    }

    double lieRatio = (double) totalLieScore / lieScaleQuestions.size();
    String verdict;
    if (lieRatio > 0.8) verdict = "INVALID";
    else if (lieRatio > 0.5) verdict = "SUSPICIOUS";
    else verdict = "VALID";

    return new LieScaleResult(totalLieScore, lieScaleQuestions.size(),
                               lieRatio, verdict);
}

import com.microsoft.z3.*;

public class PaperConstraintVerifier {

    public VerificationResult verify(PaperConfig config) {
        Context ctx = new Context();
        Solver solver = ctx.mkSolver();

        // 为每个维度创建变量，并绑定到当前试卷的实际题目数
        Map<String, IntExpr> dimCounts = new HashMap<>();
        for (String dim : config.getDimensions()) {
            IntExpr count = ctx.mkIntConst("dim_" + dim);
            dimCounts.put(dim, count);
            solver.add(ctx.mkEq(count, ctx.mkInt(config.countQuestionsOfDimension(dim))));
        }

        IntExpr totalQuestions = ctx.mkInt(config.getTotalQuestionCount());
        IntExpr reverseCount = ctx.mkInt(config.getReverseQuestionCount());
        IntExpr lieCount = ctx.mkInt(config.getLieQuestionCount());

        // 约束1: 每个维度至少 3 道题（无孤立维度）
        for (IntExpr dimCount : dimCounts.values()) {
            solver.add(ctx.mkGe(dimCount, ctx.mkInt(3)));
        }

        // 约束2: 总题数在合理范围
        solver.add(ctx.mkGe(totalQuestions, ctx.mkInt(config.getMinQuestions())));
        solver.add(ctx.mkLe(totalQuestions, ctx.mkInt(config.getMaxQuestions())));

        // 约束3: 反向题占比 20%-30%
        solver.add(ctx.mkGe(reverseCount,
            ctx.mkDiv(ctx.mkMul(totalQuestions, ctx.mkInt(20)), ctx.mkInt(100))));
        solver.add(ctx.mkLe(reverseCount,
            ctx.mkDiv(ctx.mkMul(totalQuestions, ctx.mkInt(30)), ctx.mkInt(100))));

        // 约束4: 测谎题至少 4 道，不超过总题数的 15%
        solver.add(ctx.mkGe(lieCount, ctx.mkInt(4)));
        solver.add(ctx.mkLe(lieCount,
            ctx.mkDiv(ctx.mkMul(totalQuestions, ctx.mkInt(15)), ctx.mkInt(100))));

        // 约束5: 各维度题目数之和 = 总题数
        solver.add(ctx.mkEq(totalQuestions,
            dimCounts.values().stream()
                .reduce(ctx.mkInt(0), ctx::mkAdd)));

        // 检查是否可满足
        Status status = solver.check();

        VerificationResult result = new VerificationResult();
        if (status == Status.SATISFIABLE) {
            Model model = solver.getModel();
            result.setSatisfiable(true);
            result.setModel(extractModel(model, dimCounts, totalQuestions,
                                          reverseCount, lieCount));
        } else {
            result.setSatisfiable(false);
            result.setReason("约束不可满足：试卷配置存在冲突，请检查各维度题数、"
                           + "反向题比例和测谎题数量的约束条件");
        }

        ctx.close();
        return result;
    }
}

public class ScoreRangeVerifier {

    public RangeVerificationResult verifyRanges(List<DimensionConfig> dimensions) {
        Context ctx = new Context();
        Solver solver = ctx.mkSolver();

        for (DimensionConfig dim : dimensions) {
            int min = dim.getQuestionCount() * dim.getMinPerQuestion();
            int max = dim.getQuestionCount() * dim.getMaxPerQuestion();

            // 分数范围至少能区分 4 个等级
            solver.add(ctx.mkGe(ctx.mkInt(max - min), ctx.mkInt(3)));

            // 每个等级切点必须落在该维度可达到的原始分范围内
            for (int cutoff : dim.getLevelCutoffs()) {
                solver.add(ctx.mkGe(ctx.mkInt(cutoff), ctx.mkInt(min)));
                solver.add(ctx.mkLe(ctx.mkInt(cutoff), ctx.mkInt(max)));
            }
        }

        Status status = solver.check();
        RangeVerificationResult result = new RangeVerificationResult();
        result.setSatisfiable(status == Status.SATISFIABLE);
        if (status != Status.SATISFIABLE) {
            result.setReason("分数区间配置不合理：题目数、单题分值或等级切点存在冲突");
        }
        return result;
    }
}

Map<Integer, Long> distribution = answers.values().stream()
    .filter(a -> !a.isBlank())
    .collect(Collectors.groupingBy(Answer::getSelectedValue, Collectors.counting()));

long totalAnswered = answers.values().stream()
    .filter(a -> !a.isBlank()).count();

Optional<Map.Entry<Integer, Long>> maxEntry =
    distribution.entrySet().stream().max(Map.Entry.comparingByValue());

double maxRatio = (double) maxEntry.get().getValue() / totalAnswered;
boolean detected = maxRatio > 0.9 && totalAnswered >= 10;

long extremeCount = answers.entrySet().stream()
    .filter(e -> !e.getValue().isBlank())
    .filter(e -> {
        Question q = findQuestion(e.getKey());
        int value = e.getValue().getSelectedValue();
        return value == 1 || value == q.getMaxOptionValue();
    })
    .count();

double extremeRatio = (double) extremeCount / totalAnswered;
boolean detected = extremeRatio > 0.8;

List<String> reasons = new ArrayList<>();

if ("INVALID".equals(lieScale.getVerdict())) {
    reasons.add("测谎分过高");
}
if (!consistency.isReliable()) {
    reasons.add("配对题一致性过低");
}
if (pattern.getStraightLining().isDetected()) {
    reasons.add("直线作答");
}
if (pattern.getSpeeding().isDetected()) {
    reasons.add("作答过快");
}
if (pattern.getExtremePatterning().isDetected()) {
    reasons.add("极端值作答");
}

String grade;
if (reasons.isEmpty()) grade = "A";       // 完全有效
else if (reasons.size() == 1) grade = "B"; // 轻度可疑
else if (reasons.size() == 2) grade = "C"; // 中度可疑
else grade = "D";                          // 严重可疑