feat(t-wise): add option to only fully cover specific literals

Author: uulm-janbaudisch

bindings/kotlin/src/main/kotlin/de/softvare/ddnnife/java-utils.kt

@@ -43,32 +43,33 @@ fun atomicSets(ddnnf: DdnnfMut, candidates: List<Int>?, assumptions: List<Int>,
     return ddnnf.atomicSets(candidatesUInt, assumptions, cross)
 }
 
-fun sampleTWise(ddnnf: Ddnnf, t: Int): SamplingResult {
+fun sampleTWise(ddnnf: Ddnnf, t: Int, literals: List<Int>?): SamplingResult {
     require(t >= 0) { "t must be positive." }
-    return ddnnf.sampleTWise(t.toULong())
+    return ddnnf.sampleTWise(t.toULong(), literals)
 }
 
-fun isSample(result: SamplingResult): Boolean = when(result) {
+fun isSample(result: SamplingResult): Boolean = when (result) {
     is SamplingResult.ResultWithSample -> true
     else -> false
 }
 
-fun isEmpty(result: SamplingResult): Boolean = when(result) {
+fun isEmpty(result: SamplingResult): Boolean = when (result) {
     is SamplingResult.Empty -> true
     else -> false
 }
 
-fun isVoid(result: SamplingResult): Boolean = when(result) {
+fun isVoid(result: SamplingResult): Boolean = when (result) {
     is SamplingResult.Void -> true
     else -> false
 }
 
 @Throws(IllegalArgumentException::class)
 fun getSample(result: SamplingResult): Sample {
-    when(result) {
+    when (result) {
         is SamplingResult.ResultWithSample -> {
             return result.v1
         }
+
         else -> {
             throw IllegalArgumentException("Invalid sampling result type: ${result::class}")
         }

bindings/kotlin/src/test/java/de/softvare/ddnnife/JavaTest.java

@@ -69,7 +69,7 @@ void atomicSetsTest() {
 
     @Test
     void tWise() {
-        SamplingResult result = sampleTWise(ddnnf, 1);
+        SamplingResult result = sampleTWise(ddnnf, 1, null);
         assertTrue(isSample(result));
 
         Sample sample = getSample(result);

bindings/kotlin/src/test/kotlin/de/softvare/ddnnife/DdnnfTest.kt

@@ -66,7 +66,7 @@ internal class DdnnfTest {
 
     @Test
     fun tWise() {
-        val result = ddnnf.sampleTWise(1u)
+        val result = ddnnf.sampleTWise(1u, null)
         when(result) {
             is SamplingResult.ResultWithSample -> {
                 val sample = result.v1

bindings/python/tests/test_ddnnf.py

@@ -3,6 +3,7 @@
 ddnnf = Ddnnf.from_file("../../example_input/busybox-1.18.0_c2d.nnf", None)
 features = 854
 
+
 def test_sat():
     ddnnf_mut = ddnnf.as_mut()
     assert ddnnf_mut.is_sat([])
@@ -31,6 +32,7 @@ def test_core_and_dead():
     core = ddnnf_mut.dead([])
     assert len(core) == 18
 
+
 def test_core():
     core = ddnnf.get_core()
     assert len(core) == 41
@@ -54,7 +56,7 @@ def test_atomic_sets():
 
 
 def test_t_wise():
-    sample = ddnnf.sample_t_wise(1)
+    sample = ddnnf.sample_t_wise(1, None)
     assert sample.is_RESULT_WITH_SAMPLE()
     assert len(sample[0].vars) == features
 

ddnnife/benches/t_wise.rs

@@ -7,7 +7,7 @@ fn bench_t_wise(c: &mut Criterion, name: &str, path: &Path, t: usize) {
     let ddnnf = Ddnnf::from_file(path, None);
     let id = format!("t-wise {name} t={t}");
     c.bench_function(&id, |bencher| {
-        bencher.iter(|| ddnnf.sample_t_wise(black_box(t)))
+        bencher.iter(|| ddnnf.sample_t_wise(black_box(t), None))
     });
 }
 

ddnnife/src/ddnnf/anomalies/t_wise_sampling.rs

@@ -9,6 +9,7 @@ mod t_wise_sampler;
 
 use crate::ddnnf::extended_ddnnf::ExtendedDdnnf;
 use crate::ddnnf::extended_ddnnf::objective_function::FloatOrd;
+use crate::int_hash::IntSet;
 use crate::{Ddnnf, DdnnfKind};
 use SamplingResult::ResultWithSample;
 pub use config::Config;
@@ -29,17 +30,18 @@ use t_wise_sampler::{complete_partial_configs_optimal, trim_and_resample};
 
 impl Ddnnf {
     /// Generates samples so that all t-wise interactions between literals are covered.
-    pub fn sample_t_wise(&self, t: usize) -> SamplingResult {
+    pub fn sample_t_wise(&self, t: usize, literals: Option<&IntSet<i32>>) -> SamplingResult {
         // Setup everything needed for the sampling process.
         let sat_solver = SatWrapper::new(self);
         let and_merger = ZippingMerger {
             t,
             sat_solver: &sat_solver,
             ddnnf: self,
+            literals,
         };
-        let or_merger = SimilarityMerger { t };
+        let or_merger = SimilarityMerger { t, literals };
 
-        TWiseSampler::new(self, and_merger, or_merger).sample(t)
+        TWiseSampler::new(self, and_merger, or_merger, literals).sample(t)
     }
 }
 
@@ -59,7 +61,7 @@ impl ExtendedDdnnf {
         };
         let or_merger = AttributeSimilarityMerger { t, ext_ddnnf: self };
 
-        let mut sampler = TWiseSampler::new(&self.ddnnf, and_merger, or_merger);
+        let mut sampler = TWiseSampler::new(&self.ddnnf, and_merger, or_merger, None);
 
         for node_id in 0..sampler.ddnnf.nodes.len() {
             let partial_sample = sampler.partial_sample(node_id);
@@ -88,6 +90,7 @@ impl ExtendedDdnnf {
                 t,
                 self.ddnnf.number_of_variables as usize,
                 &sat_solver,
+                None,
             );
 
             complete_partial_configs_optimal(&mut sample, self);
@@ -135,6 +138,7 @@ impl ExtendedDdnnf {
             t,
             self.ddnnf.number_of_variables as usize,
             &sat_solver,
+            None,
         );
         complete_partial_configs_optimal(&mut sample, self);
 
@@ -198,7 +202,7 @@ mod test {
         let vp9: Ddnnf = build_ddnnf(Path::new("tests/data/VP9_d4.nnf"), Some(42));
 
         for t in 1..=4 {
-            check_validity_of_sample(vp9.sample_t_wise(t).get_sample().unwrap(), &vp9, t);
+            check_validity_of_sample(vp9.sample_t_wise(t, None).get_sample().unwrap(), &vp9, t);
         }
     }
 
@@ -207,7 +211,11 @@ mod test {
         let mut auto1: Ddnnf = build_ddnnf(Path::new("tests/data/auto1_d4.nnf"), Some(2513));
         let t = 1;
 
-        check_validity_of_sample(auto1.sample_t_wise(t).get_sample().unwrap(), &mut auto1, t);
+        check_validity_of_sample(
+            auto1.sample_t_wise(t, None).get_sample().unwrap(),
+            &mut auto1,
+            t,
+        );
     }
 
     #[test]

ddnnife/src/ddnnf/anomalies/t_wise_sampling/sample_merger/similarity_merger.rs

@@ -9,14 +9,15 @@ use std::cmp::{Ordering, min};
 use streaming_iterator::StreamingIterator;
 
 #[derive(Debug, Copy, Clone)]
-pub struct SimilarityMerger {
+pub struct SimilarityMerger<'l> {
     pub t: usize,
+    pub literals: Option<&'l IntSet<i32>>,
 }
 
 // Mark SimilarityMerger as an OrMerger
-impl OrMerger for SimilarityMerger {}
+impl OrMerger for SimilarityMerger<'_> {}
 
-impl SampleMerger for SimilarityMerger {
+impl SampleMerger for SimilarityMerger<'_> {
     fn merge<'a>(&self, _node_id: usize, left: &Sample, right: &Sample) -> Sample {
         if left.is_empty() {
             return right.clone();
@@ -48,7 +49,7 @@ impl SampleMerger for SimilarityMerger {
             .map(|(index, _)| index)
         {
             let next = candidates.swap_remove(next);
-            if next.is_t_wise_covered_by(&new_sample, self.t) {
+            if next.is_t_wise_covered_by(&new_sample, self.t, self.literals) {
                 continue;
             }
 
@@ -122,7 +123,12 @@ impl<'a> Candidate<'a> {
         }
     }
 
-    fn is_t_wise_covered_by(&self, sample: &Sample, t: usize) -> bool {
+    fn is_t_wise_covered_by(
+        &self,
+        sample: &Sample,
+        t: usize,
+        literals: Option<&IntSet<i32>>,
+    ) -> bool {
         if self.max_intersect == self.literals.len() {
             return true;
         }
@@ -139,7 +145,18 @@ impl<'a> Candidate<'a> {
             return false;
         }
 
-        let mut literals: Vec<i32> = self.config.get_decided_literals().collect();
+        let mut literals: Vec<i32> = self
+            .config
+            .get_decided_literals()
+            .filter(|literal| {
+                if let Some(literals) = literals {
+                    return literals.contains(literal);
+                }
+
+                true
+            })
+            .collect();
+
         literals.shuffle(&mut rng());
         debug_assert!(!literals.contains(&0));
 
@@ -154,7 +171,10 @@ mod test {
 
     #[test]
     fn test_similarity_merger() {
-        let merger = SimilarityMerger { t: 2 };
+        let merger = SimilarityMerger {
+            t: 2,
+            literals: None,
+        };
 
         let left = Sample::new_from_configs(vec![Config::from(&[1], 1)]);
         let right = Sample::new_from_configs(vec![Config::from(&[1], 1)]);
@@ -182,7 +202,7 @@ mod test {
             .iter()
             .for_each(|c| candidate.update(&c.get_decided_literals().collect::<IntSet<_>>()));
 
-        assert!(candidate.is_t_wise_covered_by(&sample, 2));
+        assert!(candidate.is_t_wise_covered_by(&sample, 2, None));
 
         let mut candidate = Candidate::new(&candidate_config);
         let sample = Sample::new_from_configs(vec![
@@ -195,6 +215,6 @@ mod test {
             .iter()
             .for_each(|c| candidate.update(&c.get_decided_literals().collect::<IntSet<_>>()));
 
-        assert!(!candidate.is_t_wise_covered_by(&sample, 2));
+        assert!(!candidate.is_t_wise_covered_by(&sample, 2, None));
     }
 }

ddnnife/src/ddnnf/anomalies/t_wise_sampling/sample_merger/zipping_merger.rs

@@ -5,21 +5,23 @@ use super::super::{
 use super::{AndMerger, SampleMerger};
 use super::{Config, Sample};
 use crate::Ddnnf;
+use crate::int_hash::IntSet;
 use std::cmp::min;
 use std::collections::HashSet;
 use streaming_iterator::StreamingIterator;
 
 #[derive(Debug, Clone)]
-pub struct ZippingMerger<'a> {
+pub struct ZippingMerger<'a, 'l> {
     pub t: usize,
     pub sat_solver: &'a SatWrapper<'a>,
     pub ddnnf: &'a Ddnnf,
+    pub literals: Option<&'l IntSet<i32>>,
 }
 
 // Mark ZippingMerger as an AndMerger
-impl AndMerger for ZippingMerger<'_> {}
+impl AndMerger for ZippingMerger<'_, '_> {}
 
-impl SampleMerger for ZippingMerger<'_> {
+impl SampleMerger for ZippingMerger<'_, '_> {
     fn merge(&self, node_id: usize, left: &Sample, right: &Sample) -> Sample {
         if left.is_empty() {
             return right.clone();
@@ -31,7 +33,7 @@ impl SampleMerger for ZippingMerger<'_> {
 
         let mut sample = Self::zip_samples(left, right, self.ddnnf.number_of_variables as usize);
 
-        for interaction in Self::interactions(left, right, self.t).iter() {
+        for interaction in self.interactions(left, right, self.t).iter() {
             cover_with_caching_twise(
                 &mut sample,
                 interaction,
@@ -68,12 +70,12 @@ impl SampleMerger for ZippingMerger<'_> {
     }
 }
 
-impl ZippingMerger<'_> {
+impl ZippingMerger<'_, '_> {
     /// Generates all t-wise interactions between two samples.
-    fn interactions(left: &Sample, right: &Sample, t: usize) -> Vec<Vec<i32>> {
+    fn interactions(&self, left: &Sample, right: &Sample, t: usize) -> Vec<Vec<i32>> {
         Self::generate_interactions(
-            Self::generate_self_interactions(left, t),
-            Self::generate_self_interactions(right, t),
+            self.generate_self_interactions(left, t),
+            self.generate_self_interactions(right, t),
         )
     }
 
@@ -125,13 +127,25 @@ impl ZippingMerger<'_> {
     ///
     /// In case no interaction of any given size is found, an empty set is still present.
     fn generate_self_interactions(
+        &self,
         sample: &Sample,
         t: usize,
     ) -> impl DoubleEndedIterator<Item = HashSet<Vec<i32>>> {
         // Extract all decided literals from the existing configs.
         let configs: Vec<Vec<i32>> = sample
             .iter()
-            .map(|config| config.get_decided_literals().collect())
+            .map(|config| {
+                config
+                    .get_decided_literals()
+                    .filter(|literal| {
+                        if let Some(literals) = self.literals {
+                            return literals.contains(literal);
+                        }
+
+                        true
+                    })
+                    .collect()
+            })
             .collect();
 
         // From 1 to t ...
@@ -236,6 +250,7 @@ mod test {
             t: 3,
             sat_solver: &sat_solver,
             ddnnf: &ddnnf,
+            literals: None,
         };
 
         let mut left_sample = new_with_literals([2, 3].into_iter().collect(), vec![-2, 3]);