Merging upstream version 1.71.1+dfsg1.

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

4 files changed, 836 insertions, 0 deletions

diff --git a/vendor/varisat-formula/src/cnf.rs b/vendor/varisat-formula/src/cnf.rs
new file mode 100644
index 000000000..ab8cfbf78
--- /dev/null
+++ b/vendor/varisat-formula/src/cnf.rs
@@ -0,0 +1,353 @@
+//! CNF formulas.
+use std::{cmp::max, fmt, ops::Range};
+
+use crate::lit::{Lit, Var};
+
+/// A formula in conjunctive normal form (CNF).
+///
+/// Equivalent to Vec<Vec<Lit>> but more efficient as it uses a single buffer for all literals.
+#[derive(Default, Eq)]
+pub struct CnfFormula {
+    var_count: usize,
+    literals: Vec<Lit>,
+    clause_ranges: Vec<Range<usize>>,
+}
+
+impl CnfFormula {
+    /// Create an empty CNF formula.
+    pub fn new() -> CnfFormula {
+        CnfFormula::default()
+    }
+
+    /// Number of variables in the formula.
+    ///
+    /// This also counts missing variables if a variable with a higher index is present.
+    /// A vector of this length can be indexed with the variable indices present.
+    pub fn var_count(&self) -> usize {
+        self.var_count
+    }
+
+    /// Increase the number of variables in the formula.
+    ///
+    /// If the parameter is less than the current variable count do nothing.
+    pub fn set_var_count(&mut self, count: usize) {
+        self.var_count = max(self.var_count, count)
+    }
+
+    /// Number of clauses in the formula.
+    pub fn len(&self) -> usize {
+        self.clause_ranges.len()
+    }
+
+    /// Whether the set of clauses is empty.
+    pub fn is_empty(&self) -> bool {
+        self.clause_ranges.is_empty()
+    }
+
+    /// Iterator over all clauses.
+    pub fn iter(&self) -> impl Iterator<Item = &[Lit]> {
+        let literals = &self.literals;
+        self.clause_ranges
+            .iter()
+            .map(move |range| &literals[range.clone()])
+    }
+}
+
+/// Convert an iterable of [`Lit`] slices into a CnfFormula
+impl<Clauses, Item> From<Clauses> for CnfFormula
+where
+    Clauses: IntoIterator<Item = Item>,
+    Item: std::borrow::Borrow<[Lit]>,
+{
+    fn from(clauses: Clauses) -> CnfFormula {
+        let mut cnf_formula = CnfFormula::new();
+        for clause in clauses {
+            cnf_formula.add_clause(clause.borrow());
+        }
+        cnf_formula
+    }
+}
+
+impl fmt::Debug for CnfFormula {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        fmt::Debug::fmt(&self.var_count(), f)?;
+        f.debug_list().entries(self.iter()).finish()
+    }
+}
+
+impl PartialEq for CnfFormula {
+    fn eq(&self, other: &CnfFormula) -> bool {
+        self.var_count() == other.var_count()
+            && self.clause_ranges.len() == other.clause_ranges.len()
+            && self
+                .clause_ranges
+                .iter()
+                .zip(other.clause_ranges.iter())
+                .all(|(range_a, range_b)| {
+                    self.literals[range_a.clone()] == other.literals[range_b.clone()]
+                })
+    }
+}
+
+/// Extend a formula with new variables and clauses.
+pub trait ExtendFormula: Sized {
+    /// Appends a clause to the formula.
+    fn add_clause(&mut self, literals: &[Lit]);
+
+    /// Add a new variable to the formula and return it.
+    fn new_var(&mut self) -> Var;
+
+    /// Add a new variable to the formula and return it as positive literal.
+    fn new_lit(&mut self) -> Lit {
+        self.new_var().positive()
+    }
+
+    /// Iterator over multiple new variables.
+    fn new_var_iter(&mut self, count: usize) -> NewVarIter<Self> {
+        NewVarIter {
+            formula: self,
+            vars_left: count,
+            phantom: std::marker::PhantomData,
+        }
+    }
+
+    /// Iterator over multiple new literals.
+    fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit> {
+        NewVarIter {
+            formula: self,
+            vars_left: count,
+            phantom: std::marker::PhantomData,
+        }
+    }
+
+    /// Add multiple new variables and return them.
+    ///
+    /// Returns a uniform tuple of variables. The number of variables is inferred, so it can be used
+    /// like `let (x, y, z) = formula.new_vars()`.
+    fn new_vars<Vars: UniformTuple<Var>>(&mut self) -> Vars {
+        Vars::tuple_from_iter(self.new_var_iter(Vars::tuple_len()))
+    }
+
+    /// Add multiple new variables and return them as positive literals.
+    ///
+    /// Returns a uniform tuple of variables. The number of variables is inferred, so it can be used
+    /// like `let (x, y, z) = formula.new_lits()`.
+    fn new_lits<Lits: UniformTuple<Lit>>(&mut self) -> Lits {
+        Lits::tuple_from_iter(self.new_lit_iter(Lits::tuple_len()))
+    }
+}
+
+/// Iterator over new variables or literals.
+///
+/// Created by the [`new_var_iter`][ExtendFormula::new_var_iter] and
+/// [`new_lit_iter`][ExtendFormula::new_lit_iter] methods of [`ExtendFormula`].
+pub struct NewVarIter<'a, F, V = Var> {
+    formula: &'a mut F,
+    vars_left: usize,
+    phantom: std::marker::PhantomData<V>,
+}
+
+impl<'a, F, V> Iterator for NewVarIter<'a, F, V>
+where
+    F: ExtendFormula,
+    V: From<Var>,
+{
+    type Item = V;
+
+    fn next(&mut self) -> Option<V> {
+        if self.vars_left == 0 {
+            None
+        } else {
+            let var = self.formula.new_var();
+            self.vars_left -= 1;
+            Some(V::from(var))
+        }
+    }
+}
+
+impl ExtendFormula for CnfFormula {
+    fn add_clause(&mut self, clause: &[Lit]) {
+        let begin = self.literals.len();
+        self.literals.extend_from_slice(clause);
+        let end = self.literals.len();
+
+        for &lit in self.literals[begin..end].iter() {
+            self.var_count = max(lit.index() + 1, self.var_count);
+        }
+
+        self.clause_ranges.push(begin..end);
+    }
+
+    fn new_var(&mut self) -> Var {
+        let var = Var::from_index(self.var_count);
+        self.var_count += 1;
+        var
+    }
+}
+
+/// Helper trait to initialize multiple variables of the same type.
+pub trait UniformTuple<Item> {
+    fn tuple_len() -> usize;
+    fn tuple_from_iter(items: impl Iterator<Item = Item>) -> Self;
+}
+
+macro_rules! ignore_first {
+    ($a:tt, $b:tt) => {
+        $b
+    };
+}
+
+macro_rules! array_like_impl {
+    ($count:expr, $($call:tt)*) => {
+        impl<Item> UniformTuple<Item> for ($(ignore_first!($call, Item)),*) {
+            fn tuple_len() -> usize { $count }
+            fn tuple_from_iter(mut items: impl Iterator<Item = Item>) -> Self {
+                ($(items.next().unwrap().into $call),*)
+            }
+        }
+    }
+}
+
+macro_rules! array_like_impl_4 {
+    ($count:expr, $($call:tt)*) => {
+        array_like_impl!($count * 4 + 2, $(()()()$call)* ()());
+        array_like_impl!($count * 4 + 3, $(()()()$call)* ()()());
+        array_like_impl!($count * 4 + 4, $(()()()$call)* ()()()());
+        array_like_impl!($count * 4 + 5, $(()()()$call)* ()()()()());
+    }
+}
+
+array_like_impl_4!(0,);
+array_like_impl_4!(1, ());
+array_like_impl_4!(2, ()());
+array_like_impl_4!(3, ()()());
+array_like_impl_4!(4, ()()()());
+
+#[cfg(any(test, feature = "proptest-strategies"))]
+#[doc(hidden)]
+pub mod strategy {
+    use super::*;
+
+    use proptest::{collection::SizeRange, prelude::*, *};
+
+    use crate::lit::strategy::lit;
+
+    pub fn vec_formula(
+        vars: impl Strategy<Value = usize>,
+        clauses: impl Into<SizeRange>,
+        clause_len: impl Into<SizeRange>,
+    ) -> impl Strategy<Value = Vec<Vec<Lit>>> {
+        let clauses = clauses.into();
+        let clause_len = clause_len.into();
+
+        // Not using ind_flat_map makes shrinking too expensive
+        vars.prop_ind_flat_map(move |vars| {
+            collection::vec(
+                collection::vec(lit(0..vars), clause_len.clone()),
+                clauses.clone(),
+            )
+        })
+    }
+
+    pub fn cnf_formula(
+        vars: impl Strategy<Value = usize>,
+        clauses: impl Into<SizeRange>,
+        clause_len: impl Into<SizeRange>,
+    ) -> impl Strategy<Value = CnfFormula> {
+        let clauses = clauses.into();
+        let clause_len = clause_len.into();
+
+        let clause_lens = collection::vec(collection::vec(Just(()), clause_len), clauses);
+        (vars, clause_lens).prop_flat_map(move |(vars, clause_lens)| {
+            let total_lits: usize = clause_lens.iter().map(|l| l.len()).sum();
+            collection::vec(lit(0..vars), total_lits)
+                .prop_map(move |literals| {
+                    let mut clause_ranges = Vec::with_capacity(clause_lens.len());
+
+                    let mut offset = 0;
+                    for len in clause_lens.iter() {
+                        clause_ranges.push(offset..offset + len.len());
+                        offset += len.len();
+                    }
+
+                    CnfFormula {
+                        var_count: vars,
+                        literals,
+                        clause_ranges,
+                    }
+                })
+                .no_shrink() // Shrinking too expensive without this
+        })
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::{strategy::*, *};
+
+    use proptest::*;
+
+    #[test]
+    fn new_vars() {
+        let mut formula = CnfFormula::new();
+        let (x, y, z) = formula.new_vars();
+
+        assert_ne!(x, y);
+        assert_ne!(y, z);
+        assert_ne!(x, y);
+        assert_eq!(formula.var_count(), 3);
+    }
+
+    #[test]
+    fn simple_roundtrip() {
+        let input = cnf![
+            1, 2, 3;
+            -1, -2;
+            7, 2;
+            ;
+            4, 5;
+        ];
+
+        let formula = CnfFormula::from(input.iter().cloned());
+
+        for (clause, &ref_clause) in formula.iter().zip(input.iter()) {
+            assert_eq!(clause, ref_clause);
+        }
+
+        assert_eq!(formula.var_count(), 7);
+    }
+
+    proptest! {
+        #[test]
+        fn roundtrip_from_vec(input in vec_formula(1..200usize, 0..1000, 0..10)) {
+            let formula = CnfFormula::from(input.clone());
+
+            for (clause, ref_clause) in formula.iter().zip(input.iter()) {
+                prop_assert_eq!(clause, &ref_clause[..]);
+            }
+
+            let var_count = input
+                .iter()
+                .flat_map(|clause| clause.iter().map(|lit| lit.index() + 1))
+                .max()
+                .unwrap_or(0);
+
+            prop_assert_eq!(formula.var_count(), var_count);
+        }
+
+        #[test]
+        fn roundtrip_from_cnf(input in cnf_formula(1..100usize, 0..1000, 0..10)) {
+            let roundtrip = CnfFormula::from(input.iter());
+
+            for (clause_a, clause_b) in input.iter().zip(roundtrip.iter()) {
+                prop_assert_eq!(clause_a, clause_b);
+            }
+
+            prop_assert!(roundtrip.var_count() <= input.var_count());
+
+            if roundtrip.var_count() == input.var_count() {
+                prop_assert_eq!(roundtrip, input);
+            }
+        }
+    }
+}
diff --git a/vendor/varisat-formula/src/lib.rs b/vendor/varisat-formula/src/lib.rs
new file mode 100644
index 000000000..5e51502ae
--- /dev/null
+++ b/vendor/varisat-formula/src/lib.rs
@@ -0,0 +1,64 @@
+//! Basic formula data types used by the Varisat SAT solver.
+
+/// Shortcut for tests
+#[cfg(any(test, feature = "internal-testing"))]
+#[doc(hidden)]
+#[macro_export]
+macro_rules! lit {
+    ($x:expr) => {
+        $crate::lit::Lit::from_dimacs($x)
+    };
+}
+
+/// Shortcut for tests
+#[cfg(any(test, feature = "internal-testing"))]
+#[doc(hidden)]
+#[macro_export]
+macro_rules! var {
+    ($x:expr) => {
+        $crate::lit::Var::from_dimacs($x)
+    };
+}
+
+/// Shortcut for tests
+#[cfg(any(test, feature = "internal-testing"))]
+#[doc(hidden)]
+#[macro_export]
+macro_rules! lits {
+    ( $( $x:expr ),* ) => { [ $( $crate::lit!( $x ) ),* ] };
+    ( $( $x:expr ),* , ) => { $crate::lits! [ $( $ x),* ] };
+}
+
+/// Shortcut for tests
+#[cfg(any(test, feature = "internal-testing"))]
+#[doc(hidden)]
+#[macro_export]
+macro_rules! vars {
+    ( $( $x:expr ),* ) => { [ $( $crate::var!( $x ) ),* ] };
+    ( $( $x:expr ),* , ) => { $crate::vars! [ $( $ x),* ] };
+}
+
+/// Shortcut for tests
+#[cfg(any(test, feature = "internal-testing"))]
+#[doc(hidden)]
+#[macro_export]
+macro_rules! cnf {
+    ( $( $( $x:expr ),* );* ; ) => { [ $( &[ $( $crate::lit!( $x ) ),* ] as &[$crate::Lit] ),* ] };
+}
+
+/// Shortcut for tests
+#[cfg(any(test, feature = "internal-testing"))]
+#[doc(hidden)]
+#[macro_export]
+macro_rules! cnf_formula {
+    ( $( $t:tt )* ) => { $crate::cnf::CnfFormula::from($crate::cnf![ $($t)* ].iter().cloned()) };
+}
+
+pub mod cnf;
+pub mod lit;
+
+#[cfg(any(test, feature = "internal-testing"))]
+pub mod test;
+
+pub use cnf::{CnfFormula, ExtendFormula};
+pub use lit::{Lit, Var};
diff --git a/vendor/varisat-formula/src/lit.rs b/vendor/varisat-formula/src/lit.rs
new file mode 100644
index 000000000..15ed5a629
--- /dev/null
+++ b/vendor/varisat-formula/src/lit.rs
@@ -0,0 +1,288 @@
+//! Literals and variables.
+use std::{fmt, ops};
+
+/// The backing type used to represent literals and variables.
+pub type LitIdx = u32;
+
+/// A boolean variable.
+///
+/// A boolean value is represented by an index. Internally these are 0-based, i.e. the first
+/// variable has the index 0. For user IO a 1-based index is used, to allow denoting negated
+/// variables using negative integers. This convention is also used in the DIMACS CNF format.
+///
+/// Creating a variable with an index larger than `Var::max_var().index()` is unsupported. This
+/// might panic or be interpreted as a different variable.
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[repr(transparent)]
+pub struct Var {
+    index: LitIdx,
+}
+
+impl Var {
+    /// Creates a variable from a 1-based index as used in the DIMCAS CNF encoding.
+    ///
+    /// The parameter must be positive and may not represent a variable past `Var::max_var()`.
+    #[inline]
+    pub fn from_dimacs(number: isize) -> Var {
+        debug_assert!(number > 0);
+        Var::from_index((number - 1) as usize)
+    }
+
+    /// Creates a variable from a 0-based index.
+    ///
+    /// The index may not represent a variable past `Var::max_var()`.
+    #[inline]
+    pub fn from_index(index: usize) -> Var {
+        debug_assert!(index <= Var::max_var().index());
+        Var {
+            index: index as LitIdx,
+        }
+    }
+
+    /// The 1-based index representing this variable in the DIMACS CNF encoding.
+    #[inline]
+    pub fn to_dimacs(self) -> isize {
+        (self.index + 1) as isize
+    }
+
+    /// The 0-based index representing this variable.
+    #[inline]
+    pub const fn index(self) -> usize {
+        self.index as usize
+    }
+
+    /// The variable with largest index that is supported.
+    ///
+    /// This is less than the backing integer type supports. This enables storing a variable index
+    /// and additional bits (as in `Lit`) or sentinel values in a single word.
+    pub const fn max_var() -> Var {
+        // Allow for sign or tag bits
+        Var {
+            index: LitIdx::max_value() >> 4,
+        }
+    }
+
+    /// Largest number of variables supported.
+    ///
+    /// This is exactly `Var::max_var().index() + 1`.
+    pub const fn max_count() -> usize {
+        Self::max_var().index() + 1
+    }
+
+    /// Creates a literal from this var and a `bool` that is `true` when the literal is positive.
+    ///
+    /// Shortcut for `Lit::from_var(var, polarity)`.
+    #[inline]
+    pub fn lit(self, polarity: bool) -> Lit {
+        Lit::from_var(self, polarity)
+    }
+
+    /// Creates a positive literal from this var.
+    ///
+    /// Shortcut for `Lit::positive(var)`.
+    #[inline]
+    pub fn positive(self) -> Lit {
+        Lit::positive(self)
+    }
+
+    /// Creates a negative literal from this var.
+    ///
+    /// Shortcut for `Lit::negative(var)`.
+    #[inline]
+    pub fn negative(self) -> Lit {
+        Lit::negative(self)
+    }
+}
+
+/// Uses the 1-based DIMACS CNF encoding.
+impl fmt::Debug for Var {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "{}", self.to_dimacs())
+    }
+}
+
+/// Uses the 1-based DIMACS CNF encoding.
+impl fmt::Display for Var {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        fmt::Debug::fmt(self, f)
+    }
+}
+
+/// A boolean literal.
+///
+/// A literal is a variable or the negation of a variable.
+///
+/// Conceptually a literal consists of a `Var` and a `bool` indicating whether the literal
+/// represents the variable (positive literal) or its negation (negative literal).
+///
+/// Internally a literal is represented as an integer that is two times the index of its variable
+/// when it is positive or one more when it is negative. This integer is called the `code` of the
+/// literal.
+///
+/// The restriction on the range of allowed indices for `Var` also applies to `Lit`.
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[repr(transparent)]
+pub struct Lit {
+    code: LitIdx,
+}
+
+impl Lit {
+    /// Creates a literal from a `Var` and a `bool` that is `true` when the literal is positive.
+    #[inline]
+    pub fn from_var(var: Var, polarity: bool) -> Lit {
+        Lit::from_litidx(var.index, polarity)
+    }
+
+    /// Create a positive literal from a `Var`.
+    #[inline]
+    pub fn positive(var: Var) -> Lit {
+        Lit::from_var(var, true)
+    }
+
+    /// Create a negative literal from a `Var`.
+    #[inline]
+    pub fn negative(var: Var) -> Lit {
+        Lit::from_var(var, false)
+    }
+
+    /// Create a literal from a variable index and a `bool` that is `true` when the literal is
+    /// positive.
+    #[inline]
+    pub fn from_index(index: usize, polarity: bool) -> Lit {
+        Lit::from_var(Var::from_index(index), polarity)
+    }
+
+    /// Create a literal with the given encoding.
+    #[inline]
+    pub fn from_code(code: usize) -> Lit {
+        debug_assert!(code <= Var::max_var().index() * 2 + 1);
+        Lit {
+            code: code as LitIdx,
+        }
+    }
+
+    #[inline]
+    fn from_litidx(index: LitIdx, polarity: bool) -> Lit {
+        debug_assert!(index <= Var::max_var().index);
+        Lit {
+            code: (index << 1) | (!polarity as LitIdx),
+        }
+    }
+
+    /// Creates a literal from an integer.
+    ///
+    /// The absolute value is used as 1-based index, the sign of
+    /// the integer is used as sign of the literal.
+    #[inline]
+    pub fn from_dimacs(number: isize) -> Lit {
+        Lit::from_var(Var::from_dimacs(number.abs()), number > 0)
+    }
+
+    /// 1-based Integer representation of the literal, opposite of `from_dimacs`.
+    #[inline]
+    pub fn to_dimacs(self) -> isize {
+        let mut number = self.var().to_dimacs();
+        if self.is_negative() {
+            number = -number
+        }
+        number
+    }
+
+    /// 0-based index of the literal's _variable_.
+    #[inline]
+    pub fn index(self) -> usize {
+        (self.code >> 1) as usize
+    }
+
+    /// The literal's variable.
+    #[inline]
+    pub fn var(self) -> Var {
+        Var {
+            index: self.code >> 1,
+        }
+    }
+
+    /// Whether the literal is negative, i.e. a negated variable.
+    #[inline]
+    pub fn is_negative(self) -> bool {
+        (self.code & 1) != 0
+    }
+
+    /// Whether the literal is positive, i.e. a non-negated variable.
+    #[inline]
+    pub fn is_positive(self) -> bool {
+        !self.is_negative()
+    }
+
+    /// Two times the variable's index for positive literals and one more for negative literals.
+    ///
+    /// This is also the internal encoding.
+    #[inline]
+    pub fn code(self) -> usize {
+        self.code as usize
+    }
+
+    /// Apply a function to the variable of the literal, without changing the polarity.
+    #[inline]
+    pub fn map_var(self, f: impl FnOnce(Var) -> Var) -> Lit {
+        f(self.var()).lit(self.is_positive())
+    }
+}
+
+impl ops::Not for Lit {
+    type Output = Lit;
+
+    #[inline]
+    fn not(self) -> Lit {
+        Lit {
+            code: self.code ^ 1,
+        }
+    }
+}
+
+impl ops::BitXor<bool> for Lit {
+    type Output = Lit;
+
+    #[inline]
+    fn bitxor(self, rhs: bool) -> Lit {
+        Lit {
+            code: self.code ^ (rhs as LitIdx),
+        }
+    }
+}
+
+impl From<Var> for Lit {
+    #[inline]
+    fn from(var: Var) -> Lit {
+        Lit::positive(var)
+    }
+}
+
+/// Uses the 1-based DIMACS CNF encoding.
+impl fmt::Debug for Lit {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "{}", self.to_dimacs())
+    }
+}
+
+/// Uses the 1-based DIMACS CNF encoding.
+impl fmt::Display for Lit {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        fmt::Debug::fmt(self, f)
+    }
+}
+
+#[cfg(any(test, feature = "proptest-strategies"))]
+#[doc(hidden)]
+pub mod strategy {
+    use super::*;
+    use proptest::{prelude::*, *};
+
+    pub fn var(index: impl Strategy<Value = usize>) -> impl Strategy<Value = Var> {
+        index.prop_map(Var::from_index)
+    }
+
+    pub fn lit(index: impl Strategy<Value = usize>) -> impl Strategy<Value = Lit> {
+        (var(index), bool::ANY).prop_map(|(var, polarity)| var.lit(polarity))
+    }
+}
diff --git a/vendor/varisat-formula/src/test.rs b/vendor/varisat-formula/src/test.rs
new file mode 100644
index 000000000..22562d0f8
--- /dev/null
+++ b/vendor/varisat-formula/src/test.rs
@@ -0,0 +1,131 @@
+use proptest::{prelude::*, *};
+
+use rand::{distributions::Bernoulli, seq::SliceRandom};
+
+use crate::{cnf::CnfFormula, lit::Lit};
+
+/// Generate small hard unsat instances.
+///
+/// Implementation of http://www.cs.qub.ac.uk/~i.spence/sgen/ but with random partitions
+pub fn sgen_unsat_formula(
+    blocks: impl Strategy<Value = usize>,
+) -> impl Strategy<Value = CnfFormula> {
+    blocks.prop_flat_map(|blocks| {
+        collection::vec(bool::ANY, blocks * 4 + 1).prop_perturb(|polarity, mut rng| {
+            let mut clauses: Vec<Vec<Lit>> = vec![];
+            let mut lits = polarity
+                .into_iter()
+                .enumerate()
+                .map(|(index, polarity)| Lit::from_index(index, polarity))
+                .collect::<Vec<_>>();
+
+            for &invert in [false, true].iter() {
+                lits.shuffle(&mut rng);
+                for block in lits.chunks_exact(4) {
+                    for a in 0..4 {
+                        for b in 0..a {
+                            for c in 0..b {
+                                let mut clause =
+                                    vec![block[a] ^ invert, block[b] ^ invert, block[c] ^ invert];
+                                clause.shuffle(&mut rng);
+                                clauses.push(clause);
+                            }
+                        }
+                    }
+                }
+                let &lit_a = lits.last().unwrap();
+                for b in 0..4 {
+                    for c in 0..b {
+                        let mut clause = vec![lit_a ^ invert, lits[b] ^ invert, lits[c] ^ invert];
+                        clause.shuffle(&mut rng);
+                        clauses.push(clause);
+                    }
+                }
+            }
+
+            clauses.shuffle(&mut rng);
+            CnfFormula::from(clauses)
+        })
+    })
+}
+
+/// Generate a sat instance.
+///
+/// This generates a random full assignment and then only generates clauses compatible with that
+/// assignment.
+pub fn sat_formula(
+    vars: impl Strategy<Value = usize>,
+    clause_count: impl Strategy<Value = usize>,
+    density: impl Strategy<Value = f64>,
+    polarity_dist: impl Strategy<Value = f64>,
+) -> impl Strategy<Value = CnfFormula> {
+    (vars, clause_count, density, polarity_dist).prop_flat_map(
+        |(vars, clause_count, density, polarity_dist)| {
+            let density = Bernoulli::new(density).unwrap();
+            let polarity_dist = Bernoulli::new(polarity_dist).unwrap();
+
+            collection::vec(bool::ANY, vars).prop_perturb(move |polarity, mut rng| {
+                let mut clauses: Vec<Vec<Lit>> = vec![];
+                let lits = polarity
+                    .into_iter()
+                    .enumerate()
+                    .map(|(index, polarity)| Lit::from_index(index, polarity))
+                    .collect::<Vec<_>>();
+
+                for _ in 0..clause_count {
+                    let &fixed_lit = lits.choose(&mut rng).unwrap();
+                    let mut clause = vec![fixed_lit];
+                    for &lit in lits.iter() {
+                        if lit != fixed_lit && rng.sample(density) {
+                            clause.push(lit ^ rng.sample(polarity_dist));
+                        }
+                    }
+                    clause.shuffle(&mut rng);
+                    clauses.push(clause);
+                }
+
+                clauses.shuffle(&mut rng);
+                CnfFormula::from(clauses)
+            })
+        },
+    )
+}
+
+/// Generates a conditional pigeon hole principle formula.
+pub fn conditional_pigeon_hole(
+    columns: impl Strategy<Value = usize>,
+    extra_rows: impl Strategy<Value = usize>,
+) -> impl Strategy<Value = (Vec<Lit>, usize, CnfFormula)> {
+    (columns, extra_rows).prop_flat_map(|(columns, extra_rows)| {
+        let rows = columns + extra_rows;
+        let vars = (columns + 1) * rows;
+
+        collection::vec(bool::ANY, vars).prop_perturb(move |polarity, mut rng| {
+            let mut clauses: Vec<Vec<Lit>> = vec![];
+            let lits = polarity
+                .into_iter()
+                .enumerate()
+                .map(|(index, polarity)| Lit::from_index(index, polarity))
+                .collect::<Vec<_>>();
+
+            for i in 1..columns + 1 {
+                for j in 0..rows {
+                    for k in 0..j {
+                        let mut clause = [lits[i * rows + j], lits[i * rows + k]];
+                        clause.shuffle(&mut rng);
+                        clauses.push(clause[..].to_owned());
+                    }
+                }
+            }
+
+            for j in 0..rows {
+                let mut clause: Vec<_> = (0..columns + 1).map(|i| !lits[i * rows + j]).collect();
+                clause.shuffle(&mut rng);
+                clauses.push(clause[..].to_owned());
+            }
+
+            clauses.shuffle(&mut rng);
+            (lits[0..rows].to_owned(), columns, CnfFormula::from(clauses))
+        })
+    })
+}