xlog-prob 0.9.2

Probabilistic inference engines for XLOG
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153

use std::sync::Arc;

use xlog_core::MemoryBudget;
use xlog_cuda::{CudaDevice, CudaKernelProvider, GpuMemoryManager};
use xlog_prob::compilation::{compile_gpu_d4_and_verify, GpuCompileConfig};
use xlog_solve::{Clause, GpuCnf, Literal, SolveInstance};

fn try_provider() -> Option<Arc<CudaKernelProvider>> {
    let device = match CudaDevice::new(0) {
        Ok(d) => Arc::new(d),
        Err(e) => {
            eprintln!("Skipping test: CUDA runtime unavailable: {}", e);
            return None;
        }
    };
    let budget = MemoryBudget::with_limit(1024 * 1024 * 1024); // 1 GiB
    let memory = Arc::new(GpuMemoryManager::new(device.clone(), budget));
    match CudaKernelProvider::new(device, memory) {
        Ok(p) => Some(Arc::new(p)),
        Err(e) => {
            eprintln!(
                "Skipping test: failed to create CUDA kernel provider: {}",
                e
            );
            None
        }
    }
}

/// Build a shared GpuCompileConfig with the given `incremental_verify` setting.
fn make_config(incremental_verify: bool) -> GpuCompileConfig {
    GpuCompileConfig {
        frontier_depth: 0,
        max_frontier_items: 8,
        max_depth: 32,
        smooth_node_cap: 1024,
        smooth_edge_cap: 4096,
        cdcl_restart_interval: 32,
        cdcl_learned_bytes: 4 * 1024 * 1024,
        cdcl_conflict_budget: None,
        incremental_verify,
    }
}

/// Original smoke test: workspace path succeeds on a unit clause.
#[test]
fn gpu_workspace_verify_unit_clause() {
    let Some(provider) = try_provider() else {
        return;
    };

    let instance = SolveInstance::new(1, vec![Clause::new(vec![Literal::positive(0)])]);
    let phi = GpuCnf::from_host(&instance, &provider).expect("GpuCnf upload");

    let config = make_config(true);

    let circuit = compile_gpu_d4_and_verify(&phi, &phi.num_vars, &provider, &config)
        .expect("compile must succeed");
    assert!(circuit.num_nodes() > 0);
}

/// Parity test: default path (incremental_verify=false) and workspace path
/// (incremental_verify=true) produce identical node counts on a unit clause.
#[test]
fn gpu_workspace_verify_parity_unit_clause() {
    let Some(provider) = try_provider() else {
        return;
    };

    let instance = SolveInstance::new(1, vec![Clause::new(vec![Literal::positive(0)])]);
    let phi = GpuCnf::from_host(&instance, &provider).expect("GpuCnf upload");

    // Run default path (no workspace reuse).
    let config_default = make_config(false);
    let circuit_default =
        compile_gpu_d4_and_verify(&phi, &phi.num_vars, &provider, &config_default)
            .expect("default path must succeed");

    // Run workspace path (incremental verify).
    let config_workspace = make_config(true);
    let circuit_workspace =
        compile_gpu_d4_and_verify(&phi, &phi.num_vars, &provider, &config_workspace)
            .expect("workspace path must succeed");

    assert!(
        circuit_default.num_nodes() > 0,
        "default path produced zero nodes"
    );
    assert_eq!(
        circuit_default.num_nodes(),
        circuit_workspace.num_nodes(),
        "node count mismatch: default={} vs workspace={}",
        circuit_default.num_nodes(),
        circuit_workspace.num_nodes(),
    );

    eprintln!(
        "parity_unit_clause: both paths produced {} nodes",
        circuit_default.num_nodes()
    );
}

/// Parity test on a nontrivial multi-variable, multi-clause formula.
///
/// Formula (3 vars, 4 clauses):
///   (x0 | x1)  &  (!x0 | x2)  &  (!x1 | !x2)  &  (x0 | x2)
///
/// This exercises meaningful selector growth across the compilation/verification
/// pipeline, unlike a trivial unit clause.
#[test]
fn gpu_workspace_verify_parity_multi_clause() {
    let Some(provider) = try_provider() else {
        return;
    };

    let clauses = vec![
        Clause::new(vec![Literal::positive(0), Literal::positive(1)]),
        Clause::new(vec![Literal::negative(0), Literal::positive(2)]),
        Clause::new(vec![Literal::negative(1), Literal::negative(2)]),
        Clause::new(vec![Literal::positive(0), Literal::positive(2)]),
    ];
    let instance = SolveInstance::new(3, clauses);
    let phi = GpuCnf::from_host(&instance, &provider).expect("GpuCnf upload");

    // Run default path.
    let config_default = make_config(false);
    let circuit_default =
        compile_gpu_d4_and_verify(&phi, &phi.num_vars, &provider, &config_default)
            .expect("default path must succeed on multi-clause formula");

    // Run workspace path.
    let config_workspace = make_config(true);
    let circuit_workspace =
        compile_gpu_d4_and_verify(&phi, &phi.num_vars, &provider, &config_workspace)
            .expect("workspace path must succeed on multi-clause formula");

    assert!(
        circuit_default.num_nodes() > 0,
        "default path produced zero nodes on multi-clause formula"
    );
    assert_eq!(
        circuit_default.num_nodes(),
        circuit_workspace.num_nodes(),
        "node count mismatch on multi-clause: default={} vs workspace={}",
        circuit_default.num_nodes(),
        circuit_workspace.num_nodes(),
    );

    eprintln!(
        "parity_multi_clause: both paths produced {} nodes",
        circuit_default.num_nodes()
    );
}