conjure_cp_core/ast/
sat_decision.rs

1//! Semantic SAT encoding decisions. Clauses and solver literals belong to the adaptor.
2use crate::ast::Expression;
3use serde::{Deserialize, Serialize};
4use std::fmt::{Display, Formatter};
5use uniplate::Uniplate;
6
7// One listing defines each family's labels, parsing and heuristic iteration order.
8macro_rules! encoding_labels {
9    ($type:ident, $family:literal, $len:literal, [$($variant:ident => $label:literal),+ $(,)?]) => {
10        impl $type {
11            /// Algorithms in heuristic and command-line order.
12            pub const ALL: [Self; $len] = [$(Self::$variant),+];
13            /// Canonical command-line labels in the same order as `ALL`.
14            pub const LABELS: [&'static str; $len] = [$($label),+];
15        }
16        impl Display for $type {
17            fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
18                f.write_str(match self { $(Self::$variant => $label),+ })
19            }
20        }
21        impl std::str::FromStr for $type {
22            type Err = String;
23            fn from_str(value: &str) -> Result<Self, String> {
24                match value {
25                    $($label => Ok(Self::$variant),)+
26                    _ => Err(format!(concat!("unknown ", $family, " '{}'; expected {}"), value, Self::LABELS.join(", "))),
27                }
28            }
29        }
30    };
31}
32
33/// A Boolean operation whose truth is asserted or bound to a named output.
34#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]
35#[biplate(to=Expression)]
36#[biplate(to=crate::ast::DeclarationPtr)]
37pub enum SatEncodingDecision {
38    /// Assert the semantic Boolean expression; the adaptor chooses clauses and witnesses.
39    Assert(Expression),
40    /// At most one input may be true; the selected library algorithm is recorded explicitly.
41    AtMostOne {
42        inputs: Vec<Expression>,
43        encoding: Option<EncodingSelection<AmoEncoding>>,
44    },
45    /// Compare the number of true operands with a mathematical integer bound.
46    Cardinality {
47        inputs: Vec<Expression>,
48        relation: CardinalityRelation,
49        bound: i64,
50        encoding: Option<EncodingSelection<CardinalityEncoding>>,
51    },
52    /// Define the truth of a Boolean count comparison using cardinality and AMO providers.
53    CountRelation {
54        output: Expression,
55        inputs: Vec<Expression>,
56        relation: IntegerRelation,
57        bound: i64,
58        encoding: Option<EncodingSelection<CardinalityEncoding>>,
59        /// Selected when either implication includes an at-most-one threshold.
60        amo_encoding: Option<EncodingSelection<AmoEncoding>>,
61    },
62    /// Compare a signed weighted Boolean sum with an integer bound.
63    PseudoBoolean {
64        terms: Vec<(i64, Expression)>,
65        /// Relationships already guaranteed by the integer representation constraints.
66        #[serde(default, skip_serializing_if = "Vec::is_empty")]
67        groups: Vec<PbTermGroup>,
68        relation: CardinalityRelation,
69        bound: i64,
70        encoding: Option<EncodingSelection<PbEncoding>>,
71    },
72    /// Define an integer relation over a signed weighted view of the numeric operands.
73    IntegerRelation {
74        output: Expression,
75        terms: Vec<(i64, Expression)>,
76        groups: Vec<PbTermGroup>,
77        relation: IntegerRelation,
78        bound: i64,
79        encoding: Option<EncodingSelection<PbEncoding>>,
80    },
81    /// Minimise or maximise an actual-value integer view using the selected PB provider.
82    Objective {
83        minimise: bool,
84        value: SatIntegerView,
85        encoding: Option<EncodingSelection<PbEncoding>>,
86    },
87    /// Define scalar or whole-value distinctness, with an optional repeated exception value.
88    AllDifferent {
89        output: Expression,
90        inputs: Vec<SatIntegerView>,
91        /// Pair conditions for compound values, lowered through the existing equality rules.
92        #[serde(default, skip_serializing_if = "Option::is_none")]
93        comparisons: Option<Vec<Expression>>,
94        /// This value may occur repeatedly.
95        #[serde(default, skip_serializing_if = "Option::is_none")]
96        except: Option<SatIntegerView>,
97        encoding: Option<EncodingSelection<AllDifferentEncoding>>,
98        amo_encoding: Option<EncodingSelection<AmoEncoding>>,
99        pb_encoding: Option<EncodingSelection<PbEncoding>>,
100    },
101    /// Define membership in an integer/Boolean relation.
102    Table {
103        output: Expression,
104        inputs: Vec<SatIntegerView>,
105        rows: Vec<Vec<i64>>,
106        /// Non-constant relation cells retain their numeric representation views.
107        #[serde(default, skip_serializing_if = "Option::is_none")]
108        row_views: Option<Vec<Vec<SatIntegerView>>>,
109        negative: bool,
110        encoding: Option<EncodingSelection<TableEncoding>>,
111        pb_encoding: Option<EncodingSelection<PbEncoding>>,
112    },
113    /// Define a selected scalar value; out-of-domain indices leave it unconstrained.
114    Element {
115        index_view: SatIntegerView,
116        value: SatIntegerView,
117        entries: Vec<(i64, SatIntegerView)>,
118        encoding: Option<EncodingSelection<ElementEncoding>>,
119        pb_encoding: Option<EncodingSelection<PbEncoding>>,
120    },
121    /// Define an output as equivalent to a semantic Boolean expression.
122    Boolean {
123        output: Expression,
124        expression: Expression,
125    },
126}
127
128impl Display for SatEncodingDecision {
129    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
130        match self {
131            Self::AtMostOne { inputs, encoding } => write!(
132                f,
133                "at-most-one({}) using {:?}",
134                inputs
135                    .iter()
136                    .map(ToString::to_string)
137                    .collect::<Vec<_>>()
138                    .join(", "),
139                encoding
140            ),
141            Self::Cardinality {
142                inputs,
143                relation,
144                bound,
145                encoding,
146            } => write!(
147                f,
148                "count({}) {:?} {bound} using {encoding:?}",
149                inputs
150                    .iter()
151                    .map(ToString::to_string)
152                    .collect::<Vec<_>>()
153                    .join(", "),
154                relation
155            ),
156            Self::CountRelation {
157                output,
158                inputs,
159                relation,
160                bound,
161                encoding,
162                amo_encoding,
163            } => write!(
164                f,
165                "define({output} <-> count({}) {relation:?} {bound}) using {encoding:?}, AMO {amo_encoding:?}",
166                inputs
167                    .iter()
168                    .map(ToString::to_string)
169                    .collect::<Vec<_>>()
170                    .join(", "),
171            ),
172            Self::PseudoBoolean {
173                terms,
174                groups,
175                relation,
176                bound,
177                encoding,
178            } => {
179                write!(
180                    f,
181                    "weighted({}) {relation:?} {bound} using {encoding:?}",
182                    terms
183                        .iter()
184                        .map(|(weight, input)| format!("{weight}*{input}"))
185                        .collect::<Vec<_>>()
186                        .join(", ")
187                )?;
188                if !groups.is_empty() {
189                    write!(f, " with {groups:?}")?;
190                }
191                Ok(())
192            }
193            Self::IntegerRelation {
194                output,
195                terms,
196                groups,
197                relation,
198                bound,
199                encoding,
200            } => write!(
201                f,
202                "define({output} <-> integer-weighted({}) {relation:?} {bound}) using {encoding:?} with {groups:?}",
203                terms
204                    .iter()
205                    .map(|(weight, input)| format!("{weight}*{input}"))
206                    .collect::<Vec<_>>()
207                    .join(", ")
208            ),
209            Self::AllDifferent {
210                output,
211                inputs,
212                except,
213                comparisons,
214                encoding,
215                amo_encoding,
216                pb_encoding,
217            } => {
218                let inputs = inputs
219                    .iter()
220                    .map(ToString::to_string)
221                    .collect::<Vec<_>>()
222                    .join(", ");
223                let constraint = if let Some(comparisons) = comparisons {
224                    format!(
225                        "allDifferentComparisons({})",
226                        comparisons
227                            .iter()
228                            .map(ToString::to_string)
229                            .collect::<Vec<_>>()
230                            .join(", ")
231                    )
232                } else {
233                    match except {
234                        Some(value) if value.terms.is_empty() => {
235                            format!("allDifferentExcept({inputs}, {})", value.constant)
236                        }
237                        Some(value) => format!("allDifferentExcept({inputs}, {value})"),
238                        None => format!("allDifferent({inputs})"),
239                    }
240                };
241                write!(
242                    f,
243                    "define({output} <-> {constraint}) using {encoding:?}, AMO {amo_encoding:?}, PB {pb_encoding:?}"
244                )
245            }
246            Self::Table {
247                output,
248                inputs,
249                rows,
250                row_views,
251                negative,
252                encoding,
253                pb_encoding,
254            } => write!(
255                f,
256                "define({output} <-> table({}, {}, negative={negative})) using {encoding:?}, PB {pb_encoding:?}",
257                inputs
258                    .iter()
259                    .map(ToString::to_string)
260                    .collect::<Vec<_>>()
261                    .join(", "),
262                row_views
263                    .as_ref()
264                    .map_or_else(|| format!("{rows:?}"), |views| format!("{views:?}"))
265            ),
266            Self::Element {
267                index_view,
268                value,
269                entries,
270                encoding,
271                pb_encoding,
272            } => write!(
273                f,
274                "element(index={index_view}, value={value}, entries=[{}]) using {encoding:?}, PB {pb_encoding:?}",
275                entries
276                    .iter()
277                    .map(|(label, view)| format!("{label}: {view}"))
278                    .collect::<Vec<_>>()
279                    .join(", ")
280            ),
281            Self::Objective {
282                minimise,
283                value,
284                encoding,
285            } => write!(
286                f,
287                "optimise(minimise={minimise}, value={value}) using {encoding:?}"
288            ),
289            Self::Assert(expression) => write!(f, "assert({expression}) using tseitin"),
290            Self::Boolean { output, expression } => {
291                write!(f, "define({output} <-> {expression}) using tseitin")
292            }
293        }
294    }
295}
296
297/// Numeric relation between a weighted integer view and its bound.
298#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]
299pub enum IntegerRelation {
300    Equal,
301    NotEqual,
302    Less,
303    LessEqual,
304    Greater,
305    GreaterEqual,
306}
307
308/// A contiguous group of weighted terms with an existing representation invariant.
309#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]
310pub struct PbTermGroup {
311    /// First term index, inclusive.
312    pub start: usize,
313    /// Last term index, exclusive.
314    pub end: usize,
315    /// The relationship between these terms, independent of library literals.
316    pub structure: PbTermStructure,
317}
318
319/// Representation structure available to a pseudo-Boolean encoder.
320#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]
321pub enum PbTermStructure {
322    /// At most one Boolean input in the group is true.
323    Choice,
324    /// Each Boolean input is implied by the next input in the group.
325    Chain,
326    /// Binary terms bounded by the representation's inclusive domain.
327    BoundedBinary { lower: i64, upper: i64 },
328}
329
330impl SatEncodingDecision {
331    /// Semantic expressions held by this decision.
332    pub fn expressions(&self) -> Vec<&Expression> {
333        match self {
334            Self::AtMostOne { inputs, .. } | Self::Cardinality { inputs, .. } => {
335                inputs.iter().collect()
336            }
337            Self::Objective { value, .. } => value
338                .terms
339                .iter()
340                .map(|(_, expression)| expression)
341                .collect(),
342            Self::CountRelation { output, inputs, .. } => {
343                std::iter::once(output).chain(inputs).collect()
344            }
345            Self::PseudoBoolean { terms, .. } => terms.iter().map(|(_, input)| input).collect(),
346            Self::IntegerRelation { output, terms, .. } => std::iter::once(output)
347                .chain(terms.iter().map(|(_, input)| input))
348                .collect(),
349            Self::AllDifferent {
350                output,
351                inputs,
352                except,
353                comparisons,
354                ..
355            } => std::iter::once(output)
356                .chain(comparisons.iter().flatten())
357                .chain(inputs.iter().chain(except.iter()).flat_map(|input| {
358                    input
359                        .terms
360                        .iter()
361                        .map(|(_, term)| term)
362                        .chain(input.choices.iter().flatten().map(|(_, term)| term))
363                }))
364                .collect(),
365            Self::Table {
366                output,
367                inputs,
368                row_views,
369                ..
370            } => std::iter::once(output)
371                .chain(
372                    inputs
373                        .iter()
374                        .chain(row_views.iter().flatten().flatten())
375                        .flat_map(|input| {
376                            input
377                                .terms
378                                .iter()
379                                .map(|(_, term)| term)
380                                .chain(input.choices.iter().flatten().map(|(_, term)| term))
381                        }),
382                )
383                .collect(),
384            Self::Element {
385                index_view,
386                value,
387                entries,
388                ..
389            } => std::iter::once(index_view)
390                .chain(std::iter::once(value))
391                .chain(entries.iter().map(|(_, entry)| entry))
392                .flat_map(|view| {
393                    view.terms
394                        .iter()
395                        .map(|(_, term)| term)
396                        .chain(view.choices.iter().flatten().map(|(_, term)| term))
397                })
398                .collect(),
399            Self::Assert(expression) => vec![expression],
400            Self::Boolean { output, expression } => vec![output, expression],
401        }
402    }
403}
404
405/// A numeric view whose representation constraints remain independently enforced.
406#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]
407#[biplate(to=Expression)]
408#[biplate(to=crate::ast::DeclarationPtr)]
409pub struct SatIntegerView {
410    /// Constant contribution to the actual numeric value.
411    pub constant: i64,
412    /// Signed weights over Boolean representation operands.
413    pub terms: Vec<(i64, Expression)>,
414    /// Independently guaranteed representation structure.
415    pub groups: Vec<PbTermGroup>,
416    /// Actual values and their exactly-one indicators, when available.
417    pub choices: Option<Vec<(i64, Expression)>>,
418}
419
420impl Display for SatIntegerView {
421    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
422        write!(
423            f,
424            "{}+weighted({}) with {:?}",
425            self.constant,
426            self.terms
427                .iter()
428                .map(|(weight, input)| format!("{weight}*{input}"))
429                .collect::<Vec<_>>()
430                .join(", "),
431            self.groups
432        )?;
433        if let Some(choices) = &self.choices {
434            write!(
435                f,
436                " choices({})",
437                choices
438                    .iter()
439                    .map(|(value, input)| format!("{value}:{input}"))
440                    .collect::<Vec<_>>()
441                    .join(", ")
442            )?;
443        }
444        Ok(())
445    }
446}
447
448/// Library compositions available for element.
449#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
450pub enum ElementEncoding {
451    /// Each valid index selector implies its scalar equality.
452    Implication,
453    /// One support disjunction, with an explicit out-of-domain alternative.
454    Support,
455}
456encoding_labels!(ElementEncoding, "element encoding", 2, [
457    Implication => "implication",
458    Support => "support",
459]);
460
461/// Library compositions available for table.
462#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
463pub enum TableEncoding {
464    /// Disjunction of matching rows, sharing each numeric cell comparison.
465    Tuple,
466    /// Reduced layered decision diagram, sharing equal suffix relations.
467    Mdd,
468    /// Bidirectional value supports for constant binary relations.
469    BinarySupport,
470}
471encoding_labels!(TableEncoding, "table encoding", 3, [
472    Tuple => "tuple",
473    Mdd => "mdd",
474    BinarySupport => "binary-support",
475]);
476
477/// Library compositions available for allDifferent.
478#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
479pub enum AllDifferentEncoding {
480    /// Pairwise numeric disequalities, for every numeric representation.
481    Pairwise,
482    /// AMO over equal-value indicators; requires choice views for all operands.
483    ValueAmo,
484}
485encoding_labels!(AllDifferentEncoding, "allDifferent encoding", 2, [
486    Pairwise => "pairwise",
487    ValueAmo => "value-amo",
488]);
489
490/// The origin of a resolved compilation choice.
491#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
492pub enum SelectionProvenance {
493    ExplicitConfiguration,
494    Heuristic,
495}
496
497/// A resolved algorithm and the source of that choice, reusable across encoding classes.
498#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
499pub struct EncodingSelection<T> {
500    pub algorithm: T,
501    pub provenance: SelectionProvenance,
502}
503
504/// Library algorithms available for asserted and reified at-most-one constraints.
505#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
506pub enum AmoEncoding {
507    Pairwise,
508    Ladder,
509    Bitwise,
510    Commander,
511    Bimander,
512    TwoProduct,
513    PindakaasPairwise,
514    PindakaasLadder,
515    PindakaasBitwise,
516}
517encoding_labels!(AmoEncoding, "AMO encoding", 9, [
518    Pairwise => "pairwise",
519    Ladder => "ladder",
520    Bitwise => "bitwise",
521    Commander => "commander",
522    Bimander => "bimander",
523    TwoProduct => "two-product",
524    PindakaasPairwise => "pindakaas-pairwise",
525    PindakaasLadder => "pindakaas-ladder",
526    PindakaasBitwise => "pindakaas-bitwise",
527]);
528
529/// Bound direction for a semantic cardinality constraint.
530#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
531pub enum CardinalityRelation {
532    AtMost,
533    AtLeast,
534    Exactly,
535}
536/// Provider and algorithm for a cardinality constraint.
537#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
538pub enum CardinalityEncoding {
539    RustsatTotalizer,
540    PindakaasSortingNetwork,
541}
542encoding_labels!(CardinalityEncoding, "cardinality encoder", 2, [
543    RustsatTotalizer => "rustsat-totalizer",
544    PindakaasSortingNetwork => "pindakaas-sorting-network",
545]);
546/// Provider and algorithm for signed weighted pseudo-Boolean constraints.
547#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
548pub enum PbEncoding {
549    RustsatGeneralizedTotalizer,
550    RustsatBinaryAdder,
551    PindakaasBdd,
552    RustsatDynamicPolyWatchdog,
553    PindakaasSwc,
554}
555encoding_labels!(PbEncoding, "pseudo-Boolean encoder", 5, [
556    RustsatGeneralizedTotalizer => "rustsat-generalized-totalizer",
557    RustsatBinaryAdder => "rustsat-binary-adder",
558    PindakaasBdd => "pindakaas-bdd",
559    RustsatDynamicPolyWatchdog => "rustsat-dynamic-poly-watchdog",
560    PindakaasSwc => "pindakaas-swc",
561]);
conjure_cp_core/ast/sat_decision.rs

conjure_cp_core/ast/
sat_decision.rs
