pindakaas 0.5.0

Encoding Integer and Pseudo Boolean constraints into CNF
Documentation 
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

//! This module contains the pindakaas interface to the
//! [Intel SAT](https://github.com/alexander-nadel/intel_sat_solver) solver.

use std::ffi::{c_int, c_void};

use pindakaas_intel_sat::{
	intel_sat_add, intel_sat_assume, intel_sat_failed, intel_sat_init, intel_sat_release,
	intel_sat_set_learn, intel_sat_set_terminate, intel_sat_solve, intel_sat_val,
};

use crate::{
	solver::{
		ipasir::{
			var_factory_next_var, var_factory_next_var_range, AccessIpasirStore,
			IpasirAssumptionMethods, IpasirLearnCallbackMethod, IpasirLiteralMethods,
			IpasirSolverMethods, IpasirStore, IpasirTermCallbackMethod,
		},
		VarFactory,
	},
	ClauseDatabaseTools, Cnf,
};

#[derive(Debug, Default)]
/// Representation of an instance of the [Intel
/// SAT](https://github.com/alexander-nadel/intel_sat_solver) solver.
pub struct IntelSat {
	store: IpasirStore<IntelSat, VarFactory, 1, 1, 0>,
}

impl AccessIpasirStore for IntelSat {
	type Store = IpasirStore<IntelSat, VarFactory, 1, 1, 0>;

	fn ipasir_store(&self) -> &Self::Store {
		&self.store
	}
	fn ipasir_store_mut(&mut self) -> &mut Self::Store {
		&mut self.store
	}
}

impl From<&Cnf> for IntelSat {
	fn from(value: &Cnf) -> Self {
		let mut slv: Self = Default::default();
		slv.store.store.vars = value.nvar;
		for cl in value.iter() {
			// Ignore early detected unsatisfiability
			let _ = slv.add_clause(cl.iter().copied());
		}
		slv
	}
}

impl IpasirAssumptionMethods for IntelSat {
	const IPASIR_ASSUME: unsafe extern "C" fn(slv: *mut c_void, lit: i32) = intel_sat_assume;
	const IPASIR_FAILED: unsafe extern "C" fn(slv: *mut c_void, lit: i32) -> c_int =
		intel_sat_failed;
}

impl IpasirLiteralMethods for IntelSat {
	const IPASIR_NEW_RANGE: fn(slv: *mut c_void, vars: *mut c_void, len: usize) -> [i32; 2] =
		var_factory_next_var_range;
	const IPASIR_NEW_VAR: fn(slv: *mut c_void, vars: *mut c_void) -> i32 = var_factory_next_var;
}

impl IpasirLearnCallbackMethod for IntelSat {
	const IPASIR_SET_LEARN_CALLBACK: unsafe extern "C" fn(
		*mut c_void,
		*mut c_void,
		c_int,
		Option<unsafe extern "C" fn(*mut c_void, *const i32)>,
	) = intel_sat_set_learn;
}

impl IpasirSolverMethods for IntelSat {
	const IPASIR_ADD: unsafe extern "C" fn(slv: *mut c_void, lit_or_zero: i32) = intel_sat_add;
	const IPASIR_INIT: unsafe extern "C" fn() -> *mut c_void = intel_sat_init;
	const IPASIR_RELEASE: unsafe extern "C" fn(slv: *mut c_void) = intel_sat_release;
	const IPASIR_SOLVE: unsafe extern "C" fn(slv: *mut c_void) -> c_int = intel_sat_solve;
	const IPASIR_VAL: unsafe extern "C" fn(slv: *mut c_void, lit: i32) -> i32 = intel_sat_val;
}

impl IpasirTermCallbackMethod for IntelSat {
	const IPASIR_SET_TERMINATE_CALLBACK: unsafe extern "C" fn(
		*mut c_void,
		*mut c_void,
		Option<unsafe extern "C" fn(*mut c_void) -> c_int>,
	) = intel_sat_set_terminate;
}

#[cfg(test)]
mod tests {
	use traced_test::test;

	use crate::{
		bool_linear::LimitComp,
		cardinality_one::{CardinalityOne, PairwiseEncoder},
		solver::{intel_sat::IntelSat, SolveResult, Solver},
		ClauseDatabaseTools, Encoder, Valuation,
	};

	#[test]
	fn solve() {
		let mut slv = IntelSat::default();

		let a = slv.new_var().into();
		let b = slv.new_var().into();
		PairwiseEncoder::default()
			.encode(
				&mut slv,
				&CardinalityOne {
					lits: vec![a, b],
					cmp: LimitComp::Equal,
				},
			)
			.unwrap();
		let SolveResult::Satisfied(solution) = slv.solve() else {
			unreachable!()
		};
		assert!(
			(solution.value(!a) && solution.value(b)) || (solution.value(a) && solution.value(!b))
		);
	}
}