From e2979862269c942eab664df5ec7b7b1002453898 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Sun, 9 Mar 2025 11:07:31 +0200 Subject: [PATCH 1/3] feat: SIS MaxSAT algorithm --- .config/names.dic | 3 +- src/algs.rs | 8 +++++ src/algs/maxsat.rs | 84 ++++++++++++++++++++++++++++++++++++++++++++ src/instances/opt.rs | 30 ++++++++++++++++ src/lib.rs | 1 + tests/maxsat.rs | 11 ++++++ 6 files changed, 136 insertions(+), 1 deletion(-) create mode 100644 src/algs.rs create mode 100644 src/algs/maxsat.rs create mode 100644 tests/maxsat.rs diff --git a/.config/names.dic b/.config/names.dic index 2eb4b2cf..f5cbcbb2 100644 --- a/.config/names.dic +++ b/.config/names.dic @@ -1,4 +1,4 @@ -58 +59 Argelich Armin Audemard @@ -13,6 +13,7 @@ bzip2 CaDiCaL CaDiCaL's Eén +Fahiem Fazekas Fleury Gihwon diff --git a/src/algs.rs b/src/algs.rs new file mode 100644 index 00000000..5c9bb162 --- /dev/null +++ b/src/algs.rs @@ -0,0 +1,8 @@ +//! # SAT-Related Algorithms +//! +//! This module contains implementations of algorithms that build on top of SAT solvers. +//! The implementations here are typically intended to be relatively simple and are not optimized +//! for maximum performance. + +#[cfg(feature = "optimization")] +pub mod maxsat; diff --git a/src/algs/maxsat.rs b/src/algs/maxsat.rs new file mode 100644 index 00000000..4c84a3d1 --- /dev/null +++ b/src/algs/maxsat.rs @@ -0,0 +1,84 @@ +//! # MaxSAT Algorithms +//! +//! This module contains simple implementations of some MaxSAT algorithms. +//! Note that these implementations do not form competitive MaxSAT solvers and are not optimized +//! for maximum performance. + +use crate::{ + encodings::pb, + instances::{BasicVarManager, ManageVars, Objective}, + solvers::{SolveIncremental, SolveStats, SolverResult}, + types::{Assignment, Clause, Lit}, +}; + +/// Performs solution-improving search on an optimization instance +/// +/// The generic `S` is the SAT solver to be used. The generic `PBE` is the pseudo-Boolean encoding +/// to be used for encoding the objective. +/// +/// # References +/// +/// - Fahiem Bacchus and Matti Järvisalo and Ruben Martins: _Maximum Satisfiability_, in Handbook +/// of Satisfiability 2021. +/// +/// # Panics +/// +/// - If any interaction with the solver errors +/// - If the objective value overflows [`isize::MAX`] +pub fn solution_improving_search( + solver: &mut S, + objective: &Objective, +) -> Option<(Assignment, isize)> +where + S: SolveIncremental + SolveStats, + PBE: FromIterator<(Lit, usize)> + pb::BoundUpperIncremental, +{ + let Some(max_var) = std::cmp::max(solver.max_var(), objective.max_var()) else { + return Some((Assignment::default(), objective.offset())); + }; + let mut vm = BasicVarManager::from_next_free(max_var + 1); + let handle_soft_cls = |(mut cl, w): (Clause, usize)| { + debug_assert!(!cl.is_empty()); + if cl.len() == 1 { + return Some((!cl[0], w)); + } + let blit = vm.new_lit(); + cl.add(blit); + solver + .add_clause(cl) + .expect("error adding clause to solver"); + Some((!blit, w)) + }; + let mut enc: PBE = objective + .iter_soft_cls() + .into_iter() + .filter_map(handle_soft_cls) + .collect(); + + let mut sol = None; + + loop { + match solver.solve().expect("solver error while solving") { + SolverResult::Sat => { + let assign = solver.solution(max_var).expect("failed getting solution"); + let val = objective.evaluate_no_offset(&assign); + sol = Some(( + assign, + objective.offset() + isize::try_from(val).expect("objective value overflow"), + )); + if val == 0 { + return sol; + } + enc.encode_ub(val - 1..val, solver, &mut vm) + .expect("error adding clauses to solver"); + for unit in enc.enforce_ub(val - 1).expect("invalid encoding usage") { + solver + .add_unit(unit) + .expect("error adding clause to solver"); + } + } + SolverResult::Unsat => return sol, + SolverResult::Interrupted => unreachable!(), + } + } +} diff --git a/src/instances/opt.rs b/src/instances/opt.rs index 4189a44e..2024e4b9 100644 --- a/src/instances/opt.rs +++ b/src/instances/opt.rs @@ -9,8 +9,10 @@ use std::{ }; use crate::{ + algs::maxsat, clause, encodings::{card, pb}, + solvers::{SolveIncremental, SolveStats}, types::{ constraints::{CardConstraint, PbConstraint}, Assignment, Clause, ClsIter, Lit, LitIter, RsHashMap, TernaryVal, Var, WClsIter, WLitIter, @@ -472,7 +474,15 @@ impl Objective { /// Adds a soft clause or updates its weight. Returns the old weight, if /// the clause was already in the objective. + /// + /// # Panics + /// + /// If the clause is empty and `w` is larger than [`isize::MAX`] pub fn add_soft_clause(&mut self, w: usize, cl: Clause) -> Option { + if cl.is_empty() { + self.increase_offset(isize::try_from(w).expect("weight overflow")); + return None; + } if cl.len() == 1 { return self.add_soft_lit(w, !cl[0]); } @@ -1590,6 +1600,26 @@ impl Instance { let mut reader = fio::open_compressed_uncompressed_read(path)?; Self::from_opb_with_idx(&mut reader, obj_idx, opts) } + + /// Find the optimal solution to this instance with solution improving search as implemented in + /// [`crate::algs::maxsat::solution_improving_search`] + /// + /// # Panics + /// + /// - If any interaction with the solver errors + /// - If the objective value overflows [`isize::MAX`] + pub fn solution_improving_search(self) -> Option<(Assignment, isize)> + where + S: Default + SolveIncremental + SolveStats, + PBE: FromIterator<(Lit, usize)> + pb::BoundUpperIncremental, + { + let mut solver = S::default(); + let (cnf, _) = self.constrs.into_cnf(); + solver + .add_cnf(cnf) + .expect("failed adding clauses to solver"); + maxsat::solution_improving_search::(&mut solver, &self.obj) + } } impl FromIterator for Instance { diff --git a/src/lib.rs b/src/lib.rs index 25ff651b..d475b81b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -74,6 +74,7 @@ use std::collections::TryReserveError; use thiserror::Error; +pub mod algs; pub mod encodings; pub mod instances; pub mod solvers; diff --git a/tests/maxsat.rs b/tests/maxsat.rs new file mode 100644 index 00000000..9b1b0dde --- /dev/null +++ b/tests/maxsat.rs @@ -0,0 +1,11 @@ +use rustsat::instances::OptInstance; + +#[test] +fn sis() { + let inst: OptInstance = OptInstance::from_dimacs_path("./data/inc-sis-fails.wcnf").unwrap(); + let sol = inst + .solution_improving_search::( + ); + dbg!(&sol); + assert!(matches!(sol, Some((_, 8632)))); +} From 1edeb6a479143d3fc688060693ec8b3866160ad3 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Mon, 10 Mar 2025 13:55:29 +0200 Subject: [PATCH 2/3] fixup! feat: SIS MaxSAT algorithm --- .../auctions_wt-cat_sched_60_70_0003.txt.wcnf | 2387 +++++++++++++++++ src/algs/maxsat.rs | 118 +- src/instances/opt.rs | 42 +- tests/maxsat.rs | 19 +- 4 files changed, 2498 insertions(+), 68 deletions(-) create mode 100755 data/auctions_wt-cat_sched_60_70_0003.txt.wcnf diff --git a/data/auctions_wt-cat_sched_60_70_0003.txt.wcnf b/data/auctions_wt-cat_sched_60_70_0003.txt.wcnf new file mode 100755 index 00000000..8d694f02 --- /dev/null +++ b/data/auctions_wt-cat_sched_60_70_0003.txt.wcnf @@ -0,0 +1,2387 @@ +c Standarized MaxSat Instance +c{ +c "sha1sum": "55adbe9144022c38689ec2e2a9714765f2cccc21", +c "nvars": 86, +c "ncls": 2345, +c "total_lits": 4604, +c "nhards": 2259, +c "nhard_nlits": 4518, +c "nhard_len_stats": +c { "min": 2, +c "max": 2, +c "ave": 2.0000, +c "stddev": 0.0000 }, +c "nsofts": 86, +c "nsoft_nlits": 86, +c "nsoft_len_stats": +c { "min": 1, +c "max": 1, +c "ave": 1.0000, +c "stddev": 0.0000 }, +c "nsoft_wts": 3, +c "soft_wt_stats": +c { "min": 114, +c "max": 1085, +c "ave": 728.2209, +c "stddev": 447.0376 } +c} +c------------------------------------------------------------ +c +c %% The CATS webpage is http://robotics.stanford.edu/CATS +c +c %% PARAMETER SETTINGS: +c % Goods: 60; Bids: 70; Distribution: scheduling; Runs: 30; Seed: 1151601997 +c % Scheduling Distribution Parameters: +c % max_length = 10 +c % deviation = 0.500000 +c % prob_additional_deadline = 0.700000 +c % additivity = 0.200000 +c +c +c +c PSEUDOBOOLEAN 62628 +1085 1 0 +1085 2 0 +1085 3 0 +1085 4 0 +1085 5 0 +1085 6 0 +1085 7 0 +1085 8 0 +1085 9 0 +1085 10 0 +1085 11 0 +1085 12 0 +1085 13 0 +1085 14 0 +1085 15 0 +1085 16 0 +1085 17 0 +1085 18 0 +1085 19 0 +1085 20 0 +1085 21 0 +1085 22 0 +1085 23 0 +1085 24 0 +1085 25 0 +1085 26 0 +1085 27 0 +1085 28 0 +1085 29 0 +1085 30 0 +1085 31 0 +1085 32 0 +1085 33 0 +1085 34 0 +1085 35 0 +1085 36 0 +1085 37 0 +1085 38 0 +1085 39 0 +1085 40 0 +1085 41 0 +1085 42 0 +1085 43 0 +1085 44 0 +1085 45 0 +1085 46 0 +1085 47 0 +1085 48 0 +1085 49 0 +1085 50 0 +1085 51 0 +1085 52 0 +373 53 0 +373 54 0 +373 55 0 +373 56 0 +373 57 0 +373 58 0 +373 59 0 +373 60 0 +373 61 0 +114 62 0 +114 63 0 +114 64 0 +114 65 0 +114 66 0 +114 67 0 +114 68 0 +114 69 0 +114 70 0 +114 71 0 +114 72 0 +114 73 0 +114 74 0 +114 75 0 +114 76 0 +114 77 0 +114 78 0 +114 79 0 +114 80 0 +114 81 0 +114 82 0 +114 83 0 +114 84 0 +114 85 0 +114 86 0 +h -1 -53 0 +h -1 -2 0 +h -1 -54 0 +h -1 -3 0 +h -1 -55 0 +h -1 -4 0 +h -1 -56 0 +h -1 -5 0 +h -1 -57 0 +h -1 -6 0 +h -1 -58 0 +h -1 -7 0 +h -1 -59 0 +h -1 -8 0 +h -1 -60 0 +h -1 -9 0 +h -1 -61 0 +h -1 -10 0 +h -1 -11 0 +h -1 -12 0 +h -1 -13 0 +h -1 -14 0 +h -1 -15 0 +h -1 -16 0 +h -1 -17 0 +h -1 -18 0 +h -1 -19 0 +h -1 -20 0 +h -1 -21 0 +h -1 -22 0 +h -1 -23 0 +h -1 -24 0 +h -1 -25 0 +h -1 -26 0 +h -1 -27 0 +h -1 -28 0 +h -1 -29 0 +h -1 -30 0 +h -1 -31 0 +h -1 -32 0 +h -1 -33 0 +h -1 -34 0 +h -1 -35 0 +h -1 -36 0 +h -1 -37 0 +h -1 -38 0 +h -1 -39 0 +h -1 -40 0 +h -1 -41 0 +h -1 -42 0 +h -1 -43 0 +h -1 -44 0 +h -1 -45 0 +h -1 -46 0 +h -1 -47 0 +h -1 -48 0 +h -1 -49 0 +h -1 -50 0 +h -1 -51 0 +h -1 -52 0 +h -2 -53 0 +h -2 -54 0 +h -2 -3 0 +h -2 -55 0 +h -2 -4 0 +h -2 -56 0 +h -2 -5 0 +h -2 -57 0 +h -2 -6 0 +h -2 -58 0 +h -2 -7 0 +h -2 -59 0 +h -2 -8 0 +h -2 -60 0 +h -2 -9 0 +h -2 -61 0 +h -2 -10 0 +h -2 -62 0 +h -2 -11 0 +h -2 -12 0 +h -2 -13 0 +h -2 -14 0 +h -2 -15 0 +h -2 -16 0 +h -2 -17 0 +h -2 -18 0 +h -2 -19 0 +h -2 -20 0 +h -2 -21 0 +h -2 -22 0 +h -2 -23 0 +h -2 -24 0 +h -2 -25 0 +h -2 -26 0 +h -2 -27 0 +h -2 -28 0 +h -2 -29 0 +h -2 -30 0 +h -2 -31 0 +h -2 -32 0 +h -2 -33 0 +h -2 -34 0 +h -2 -35 0 +h -2 -36 0 +h -2 -37 0 +h -2 -38 0 +h -2 -39 0 +h -2 -40 0 +h -2 -41 0 +h -2 -42 0 +h -2 -43 0 +h -2 -44 0 +h -2 -45 0 +h -2 -46 0 +h -2 -47 0 +h -2 -48 0 +h -2 -49 0 +h -2 -50 0 +h -2 -51 0 +h -2 -52 0 +h -3 -53 0 +h -3 -54 0 +h -3 -55 0 +h -3 -4 0 +h -3 -56 0 +h -3 -5 0 +h -3 -57 0 +h -3 -6 0 +h -3 -58 0 +h -3 -7 0 +h -3 -59 0 +h -3 -8 0 +h -3 -60 0 +h -3 -9 0 +h -3 -61 0 +h -3 -10 0 +h -3 -62 0 +h -3 -11 0 +h -3 -63 0 +h -3 -12 0 +h -3 -13 0 +h -3 -14 0 +h -3 -15 0 +h -3 -16 0 +h -3 -17 0 +h -3 -18 0 +h -3 -19 0 +h -3 -20 0 +h -3 -21 0 +h -3 -22 0 +h -3 -23 0 +h -3 -24 0 +h -3 -25 0 +h -3 -26 0 +h -3 -27 0 +h -3 -28 0 +h -3 -29 0 +h -3 -30 0 +h -3 -31 0 +h -3 -32 0 +h -3 -33 0 +h -3 -34 0 +h -3 -35 0 +h -3 -36 0 +h -3 -37 0 +h -3 -38 0 +h -3 -39 0 +h -3 -40 0 +h -3 -41 0 +h -3 -42 0 +h -3 -43 0 +h -3 -44 0 +h -3 -45 0 +h -3 -46 0 +h -3 -47 0 +h -3 -48 0 +h -3 -49 0 +h -3 -50 0 +h -3 -51 0 +h -3 -52 0 +h -4 -53 0 +h -4 -54 0 +h -4 -55 0 +h -4 -56 0 +h -4 -5 0 +h -4 -57 0 +h -4 -6 0 +h -4 -58 0 +h -4 -7 0 +h -4 -59 0 +h -4 -8 0 +h -4 -60 0 +h -4 -9 0 +h -4 -61 0 +h -4 -10 0 +h -4 -62 0 +h -4 -11 0 +h -4 -63 0 +h -4 -12 0 +h -4 -64 0 +h -4 -13 0 +h -4 -14 0 +h -4 -15 0 +h -4 -16 0 +h -4 -17 0 +h -4 -18 0 +h -4 -19 0 +h -4 -20 0 +h -4 -21 0 +h -4 -22 0 +h -4 -23 0 +h -4 -24 0 +h -4 -25 0 +h -4 -26 0 +h -4 -27 0 +h -4 -28 0 +h -4 -29 0 +h -4 -30 0 +h -4 -31 0 +h -4 -32 0 +h -4 -33 0 +h -4 -34 0 +h -4 -35 0 +h -4 -36 0 +h -4 -37 0 +h -4 -38 0 +h -4 -39 0 +h -4 -40 0 +h -4 -41 0 +h -4 -42 0 +h -4 -43 0 +h -4 -44 0 +h -4 -45 0 +h -4 -46 0 +h -4 -47 0 +h -4 -48 0 +h -4 -49 0 +h -4 -50 0 +h -4 -51 0 +h -4 -52 0 +h -5 -54 0 +h -5 -55 0 +h -5 -56 0 +h -5 -57 0 +h -5 -6 0 +h -5 -58 0 +h -5 -7 0 +h -5 -59 0 +h -5 -8 0 +h -5 -60 0 +h -5 -9 0 +h -5 -61 0 +h -5 -10 0 +h -5 -62 0 +h -5 -11 0 +h -5 -63 0 +h -5 -12 0 +h -5 -64 0 +h -5 -13 0 +h -5 -65 0 +h -5 -14 0 +h -5 -15 0 +h -5 -16 0 +h -5 -17 0 +h -5 -18 0 +h -5 -19 0 +h -5 -20 0 +h -5 -21 0 +h -5 -22 0 +h -5 -23 0 +h -5 -24 0 +h -5 -25 0 +h -5 -26 0 +h -5 -27 0 +h -5 -28 0 +h -5 -29 0 +h -5 -30 0 +h -5 -31 0 +h -5 -32 0 +h -5 -33 0 +h -5 -34 0 +h -5 -35 0 +h -5 -36 0 +h -5 -37 0 +h -5 -38 0 +h -5 -39 0 +h -5 -40 0 +h -5 -41 0 +h -5 -42 0 +h -5 -43 0 +h -5 -44 0 +h -5 -45 0 +h -5 -46 0 +h -5 -47 0 +h -5 -48 0 +h -5 -49 0 +h -5 -50 0 +h -5 -51 0 +h -5 -52 0 +h -6 -55 0 +h -6 -56 0 +h -6 -57 0 +h -6 -58 0 +h -6 -7 0 +h -6 -59 0 +h -6 -8 0 +h -6 -60 0 +h -6 -9 0 +h -6 -61 0 +h -6 -10 0 +h -6 -62 0 +h -6 -11 0 +h -6 -63 0 +h -6 -12 0 +h -6 -64 0 +h -6 -13 0 +h -6 -65 0 +h -6 -14 0 +h -6 -66 0 +h -6 -15 0 +h -6 -16 0 +h -6 -17 0 +h -6 -18 0 +h -6 -19 0 +h -6 -20 0 +h -6 -21 0 +h -6 -22 0 +h -6 -23 0 +h -6 -24 0 +h -6 -25 0 +h -6 -26 0 +h -6 -27 0 +h -6 -28 0 +h -6 -29 0 +h -6 -30 0 +h -6 -31 0 +h -6 -32 0 +h -6 -33 0 +h -6 -34 0 +h -6 -35 0 +h -6 -36 0 +h -6 -37 0 +h -6 -38 0 +h -6 -39 0 +h -6 -40 0 +h -6 -41 0 +h -6 -42 0 +h -6 -43 0 +h -6 -44 0 +h -6 -45 0 +h -6 -46 0 +h -6 -47 0 +h -6 -48 0 +h -6 -49 0 +h -6 -50 0 +h -6 -51 0 +h -6 -52 0 +h -7 -56 0 +h -7 -57 0 +h -7 -58 0 +h -7 -59 0 +h -7 -8 0 +h -7 -60 0 +h -7 -9 0 +h -7 -61 0 +h -7 -10 0 +h -7 -62 0 +h -7 -11 0 +h -7 -63 0 +h -7 -12 0 +h -7 -64 0 +h -7 -13 0 +h -7 -65 0 +h -7 -14 0 +h -7 -66 0 +h -7 -15 0 +h -7 -67 0 +h -7 -16 0 +h -7 -17 0 +h -7 -18 0 +h -7 -19 0 +h -7 -20 0 +h -7 -21 0 +h -7 -22 0 +h -7 -23 0 +h -7 -24 0 +h -7 -25 0 +h -7 -26 0 +h -7 -27 0 +h -7 -28 0 +h -7 -29 0 +h -7 -30 0 +h -7 -31 0 +h -7 -32 0 +h -7 -33 0 +h -7 -34 0 +h -7 -35 0 +h -7 -36 0 +h -7 -37 0 +h -7 -38 0 +h -7 -39 0 +h -7 -40 0 +h -7 -41 0 +h -7 -42 0 +h -7 -43 0 +h -7 -44 0 +h -7 -45 0 +h -7 -46 0 +h -7 -47 0 +h -7 -48 0 +h -7 -49 0 +h -7 -50 0 +h -7 -51 0 +h -7 -52 0 +h -8 -57 0 +h -8 -58 0 +h -8 -59 0 +h -8 -60 0 +h -8 -9 0 +h -8 -61 0 +h -8 -10 0 +h -8 -62 0 +h -8 -11 0 +h -8 -63 0 +h -8 -12 0 +h -8 -64 0 +h -8 -13 0 +h -8 -65 0 +h -8 -14 0 +h -8 -66 0 +h -8 -15 0 +h -8 -67 0 +h -8 -16 0 +h -8 -68 0 +h -8 -17 0 +h -8 -18 0 +h -8 -19 0 +h -8 -20 0 +h -8 -21 0 +h -8 -22 0 +h -8 -23 0 +h -8 -24 0 +h -8 -25 0 +h -8 -26 0 +h -8 -27 0 +h -8 -28 0 +h -8 -29 0 +h -8 -30 0 +h -8 -31 0 +h -8 -32 0 +h -8 -33 0 +h -8 -34 0 +h -8 -35 0 +h -8 -36 0 +h -8 -37 0 +h -8 -38 0 +h -8 -39 0 +h -8 -40 0 +h -8 -41 0 +h -8 -42 0 +h -8 -43 0 +h -8 -44 0 +h -8 -45 0 +h -8 -46 0 +h -8 -47 0 +h -8 -48 0 +h -8 -49 0 +h -8 -50 0 +h -8 -51 0 +h -8 -52 0 +h -9 -58 0 +h -9 -59 0 +h -9 -60 0 +h -9 -61 0 +h -9 -10 0 +h -9 -62 0 +h -9 -11 0 +h -9 -63 0 +h -9 -12 0 +h -9 -64 0 +h -9 -13 0 +h -9 -65 0 +h -9 -14 0 +h -9 -66 0 +h -9 -15 0 +h -9 -67 0 +h -9 -16 0 +h -9 -68 0 +h -9 -17 0 +h -9 -69 0 +h -9 -18 0 +h -9 -19 0 +h -9 -20 0 +h -9 -21 0 +h -9 -22 0 +h -9 -23 0 +h -9 -24 0 +h -9 -25 0 +h -9 -26 0 +h -9 -27 0 +h -9 -28 0 +h -9 -29 0 +h -9 -30 0 +h -9 -31 0 +h -9 -32 0 +h -9 -33 0 +h -9 -34 0 +h -9 -35 0 +h -9 -36 0 +h -9 -37 0 +h -9 -38 0 +h -9 -39 0 +h -9 -40 0 +h -9 -41 0 +h -9 -42 0 +h -9 -43 0 +h -9 -44 0 +h -9 -45 0 +h -9 -46 0 +h -9 -47 0 +h -9 -48 0 +h -9 -49 0 +h -9 -50 0 +h -9 -51 0 +h -9 -52 0 +h -10 -59 0 +h -10 -60 0 +h -10 -61 0 +h -10 -62 0 +h -10 -11 0 +h -10 -63 0 +h -10 -12 0 +h -10 -64 0 +h -10 -13 0 +h -10 -65 0 +h -10 -14 0 +h -10 -66 0 +h -10 -15 0 +h -10 -67 0 +h -10 -16 0 +h -10 -68 0 +h -10 -17 0 +h -10 -69 0 +h -10 -18 0 +h -10 -70 0 +h -10 -19 0 +h -10 -20 0 +h -10 -21 0 +h -10 -22 0 +h -10 -23 0 +h -10 -24 0 +h -10 -25 0 +h -10 -26 0 +h -10 -27 0 +h -10 -28 0 +h -10 -29 0 +h -10 -30 0 +h -10 -31 0 +h -10 -32 0 +h -10 -33 0 +h -10 -34 0 +h -10 -35 0 +h -10 -36 0 +h -10 -37 0 +h -10 -38 0 +h -10 -39 0 +h -10 -40 0 +h -10 -41 0 +h -10 -42 0 +h -10 -43 0 +h -10 -44 0 +h -10 -45 0 +h -10 -46 0 +h -10 -47 0 +h -10 -48 0 +h -10 -49 0 +h -10 -50 0 +h -10 -51 0 +h -10 -52 0 +h -11 -60 0 +h -11 -61 0 +h -11 -62 0 +h -11 -63 0 +h -11 -12 0 +h -11 -64 0 +h -11 -13 0 +h -11 -65 0 +h -11 -14 0 +h -11 -66 0 +h -11 -15 0 +h -11 -67 0 +h -11 -16 0 +h -11 -68 0 +h -11 -17 0 +h -11 -69 0 +h -11 -18 0 +h -11 -70 0 +h -11 -19 0 +h -11 -71 0 +h -11 -20 0 +h -11 -21 0 +h -11 -22 0 +h -11 -23 0 +h -11 -24 0 +h -11 -25 0 +h -11 -26 0 +h -11 -27 0 +h -11 -28 0 +h -11 -29 0 +h -11 -30 0 +h -11 -31 0 +h -11 -32 0 +h -11 -33 0 +h -11 -34 0 +h -11 -35 0 +h -11 -36 0 +h -11 -37 0 +h -11 -38 0 +h -11 -39 0 +h -11 -40 0 +h -11 -41 0 +h -11 -42 0 +h -11 -43 0 +h -11 -44 0 +h -11 -45 0 +h -11 -46 0 +h -11 -47 0 +h -11 -48 0 +h -11 -49 0 +h -11 -50 0 +h -11 -51 0 +h -11 -52 0 +h -12 -61 0 +h -12 -62 0 +h -12 -63 0 +h -12 -64 0 +h -12 -13 0 +h -12 -65 0 +h -12 -14 0 +h -12 -66 0 +h -12 -15 0 +h -12 -67 0 +h -12 -16 0 +h -12 -68 0 +h -12 -17 0 +h -12 -69 0 +h -12 -18 0 +h -12 -70 0 +h -12 -19 0 +h -12 -71 0 +h -12 -20 0 +h -12 -72 0 +h -12 -21 0 +h -12 -22 0 +h -12 -23 0 +h -12 -24 0 +h -12 -25 0 +h -12 -26 0 +h -12 -27 0 +h -12 -28 0 +h -12 -29 0 +h -12 -30 0 +h -12 -31 0 +h -12 -32 0 +h -12 -33 0 +h -12 -34 0 +h -12 -35 0 +h -12 -36 0 +h -12 -37 0 +h -12 -38 0 +h -12 -39 0 +h -12 -40 0 +h -12 -41 0 +h -12 -42 0 +h -12 -43 0 +h -12 -44 0 +h -12 -45 0 +h -12 -46 0 +h -12 -47 0 +h -12 -48 0 +h -12 -49 0 +h -12 -50 0 +h -12 -51 0 +h -12 -52 0 +h -13 -62 0 +h -13 -63 0 +h -13 -64 0 +h -13 -65 0 +h -13 -14 0 +h -13 -66 0 +h -13 -15 0 +h -13 -67 0 +h -13 -16 0 +h -13 -68 0 +h -13 -17 0 +h -13 -69 0 +h -13 -18 0 +h -13 -70 0 +h -13 -19 0 +h -13 -71 0 +h -13 -20 0 +h -13 -72 0 +h -13 -21 0 +h -13 -73 0 +h -13 -22 0 +h -13 -23 0 +h -13 -24 0 +h -13 -25 0 +h -13 -26 0 +h -13 -27 0 +h -13 -28 0 +h -13 -29 0 +h -13 -30 0 +h -13 -31 0 +h -13 -32 0 +h -13 -33 0 +h -13 -34 0 +h -13 -35 0 +h -13 -36 0 +h -13 -37 0 +h -13 -38 0 +h -13 -39 0 +h -13 -40 0 +h -13 -41 0 +h -13 -42 0 +h -13 -43 0 +h -13 -44 0 +h -13 -45 0 +h -13 -46 0 +h -13 -47 0 +h -13 -48 0 +h -13 -49 0 +h -13 -50 0 +h -13 -51 0 +h -13 -52 0 +h -14 -63 0 +h -14 -64 0 +h -14 -65 0 +h -14 -66 0 +h -14 -15 0 +h -14 -67 0 +h -14 -16 0 +h -14 -68 0 +h -14 -17 0 +h -14 -69 0 +h -14 -18 0 +h -14 -70 0 +h -14 -19 0 +h -14 -71 0 +h -14 -20 0 +h -14 -72 0 +h -14 -21 0 +h -14 -73 0 +h -14 -22 0 +h -14 -74 0 +h -14 -23 0 +h -14 -24 0 +h -14 -25 0 +h -14 -26 0 +h -14 -27 0 +h -14 -28 0 +h -14 -29 0 +h -14 -30 0 +h -14 -31 0 +h -14 -32 0 +h -14 -33 0 +h -14 -34 0 +h -14 -35 0 +h -14 -36 0 +h -14 -37 0 +h -14 -38 0 +h -14 -39 0 +h -14 -40 0 +h -14 -41 0 +h -14 -42 0 +h -14 -43 0 +h -14 -44 0 +h -14 -45 0 +h -14 -46 0 +h -14 -47 0 +h -14 -48 0 +h -14 -49 0 +h -14 -50 0 +h -14 -51 0 +h -14 -52 0 +h -15 -64 0 +h -15 -65 0 +h -15 -66 0 +h -15 -67 0 +h -15 -16 0 +h -15 -68 0 +h -15 -17 0 +h -15 -69 0 +h -15 -18 0 +h -15 -70 0 +h -15 -19 0 +h -15 -71 0 +h -15 -20 0 +h -15 -72 0 +h -15 -21 0 +h -15 -73 0 +h -15 -22 0 +h -15 -74 0 +h -15 -23 0 +h -15 -75 0 +h -15 -24 0 +h -15 -25 0 +h -15 -26 0 +h -15 -27 0 +h -15 -28 0 +h -15 -29 0 +h -15 -30 0 +h -15 -31 0 +h -15 -32 0 +h -15 -33 0 +h -15 -34 0 +h -15 -35 0 +h -15 -36 0 +h -15 -37 0 +h -15 -38 0 +h -15 -39 0 +h -15 -40 0 +h -15 -41 0 +h -15 -42 0 +h -15 -43 0 +h -15 -44 0 +h -15 -45 0 +h -15 -46 0 +h -15 -47 0 +h -15 -48 0 +h -15 -49 0 +h -15 -50 0 +h -15 -51 0 +h -15 -52 0 +h -16 -65 0 +h -16 -66 0 +h -16 -67 0 +h -16 -68 0 +h -16 -17 0 +h -16 -69 0 +h -16 -18 0 +h -16 -70 0 +h -16 -19 0 +h -16 -71 0 +h -16 -20 0 +h -16 -72 0 +h -16 -21 0 +h -16 -73 0 +h -16 -22 0 +h -16 -74 0 +h -16 -23 0 +h -16 -75 0 +h -16 -24 0 +h -16 -76 0 +h -16 -25 0 +h -16 -26 0 +h -16 -27 0 +h -16 -28 0 +h -16 -29 0 +h -16 -30 0 +h -16 -31 0 +h -16 -32 0 +h -16 -33 0 +h -16 -34 0 +h -16 -35 0 +h -16 -36 0 +h -16 -37 0 +h -16 -38 0 +h -16 -39 0 +h -16 -40 0 +h -16 -41 0 +h -16 -42 0 +h -16 -43 0 +h -16 -44 0 +h -16 -45 0 +h -16 -46 0 +h -16 -47 0 +h -16 -48 0 +h -16 -49 0 +h -16 -50 0 +h -16 -51 0 +h -16 -52 0 +h -17 -66 0 +h -17 -67 0 +h -17 -68 0 +h -17 -69 0 +h -17 -18 0 +h -17 -70 0 +h -17 -19 0 +h -17 -71 0 +h -17 -20 0 +h -17 -72 0 +h -17 -21 0 +h -17 -73 0 +h -17 -22 0 +h -17 -74 0 +h -17 -23 0 +h -17 -75 0 +h -17 -24 0 +h -17 -76 0 +h -17 -25 0 +h -17 -77 0 +h -17 -26 0 +h -17 -27 0 +h -17 -28 0 +h -17 -29 0 +h -17 -30 0 +h -17 -31 0 +h -17 -32 0 +h -17 -33 0 +h -17 -34 0 +h -17 -35 0 +h -17 -36 0 +h -17 -37 0 +h -17 -38 0 +h -17 -39 0 +h -17 -40 0 +h -17 -41 0 +h -17 -42 0 +h -17 -43 0 +h -17 -44 0 +h -17 -45 0 +h -17 -46 0 +h -17 -47 0 +h -17 -48 0 +h -17 -49 0 +h -17 -50 0 +h -17 -51 0 +h -17 -52 0 +h -18 -67 0 +h -18 -68 0 +h -18 -69 0 +h -18 -70 0 +h -18 -19 0 +h -18 -71 0 +h -18 -20 0 +h -18 -72 0 +h -18 -21 0 +h -18 -73 0 +h -18 -22 0 +h -18 -74 0 +h -18 -23 0 +h -18 -75 0 +h -18 -24 0 +h -18 -76 0 +h -18 -25 0 +h -18 -77 0 +h -18 -26 0 +h -18 -78 0 +h -18 -27 0 +h -18 -28 0 +h -18 -29 0 +h -18 -30 0 +h -18 -31 0 +h -18 -32 0 +h -18 -33 0 +h -18 -34 0 +h -18 -35 0 +h -18 -36 0 +h -18 -37 0 +h -18 -38 0 +h -18 -39 0 +h -18 -40 0 +h -18 -41 0 +h -18 -42 0 +h -18 -43 0 +h -18 -44 0 +h -18 -45 0 +h -18 -46 0 +h -18 -47 0 +h -18 -48 0 +h -18 -49 0 +h -18 -50 0 +h -18 -51 0 +h -18 -52 0 +h -19 -68 0 +h -19 -69 0 +h -19 -70 0 +h -19 -71 0 +h -19 -20 0 +h -19 -72 0 +h -19 -21 0 +h -19 -73 0 +h -19 -22 0 +h -19 -74 0 +h -19 -23 0 +h -19 -75 0 +h -19 -24 0 +h -19 -76 0 +h -19 -25 0 +h -19 -77 0 +h -19 -26 0 +h -19 -78 0 +h -19 -27 0 +h -19 -79 0 +h -19 -28 0 +h -19 -29 0 +h -19 -30 0 +h -19 -31 0 +h -19 -32 0 +h -19 -33 0 +h -19 -34 0 +h -19 -35 0 +h -19 -36 0 +h -19 -37 0 +h -19 -38 0 +h -19 -39 0 +h -19 -40 0 +h -19 -41 0 +h -19 -42 0 +h -19 -43 0 +h -19 -44 0 +h -19 -45 0 +h -19 -46 0 +h -19 -47 0 +h -19 -48 0 +h -19 -49 0 +h -19 -50 0 +h -19 -51 0 +h -19 -52 0 +h -20 -69 0 +h -20 -70 0 +h -20 -71 0 +h -20 -72 0 +h -20 -21 0 +h -20 -73 0 +h -20 -22 0 +h -20 -74 0 +h -20 -23 0 +h -20 -75 0 +h -20 -24 0 +h -20 -76 0 +h -20 -25 0 +h -20 -77 0 +h -20 -26 0 +h -20 -78 0 +h -20 -27 0 +h -20 -79 0 +h -20 -28 0 +h -20 -80 0 +h -20 -29 0 +h -20 -30 0 +h -20 -31 0 +h -20 -32 0 +h -20 -33 0 +h -20 -34 0 +h -20 -35 0 +h -20 -36 0 +h -20 -37 0 +h -20 -38 0 +h -20 -39 0 +h -20 -40 0 +h -20 -41 0 +h -20 -42 0 +h -20 -43 0 +h -20 -44 0 +h -20 -45 0 +h -20 -46 0 +h -20 -47 0 +h -20 -48 0 +h -20 -49 0 +h -20 -50 0 +h -20 -51 0 +h -20 -52 0 +h -21 -70 0 +h -21 -71 0 +h -21 -72 0 +h -21 -73 0 +h -21 -22 0 +h -21 -74 0 +h -21 -23 0 +h -21 -75 0 +h -21 -24 0 +h -21 -76 0 +h -21 -25 0 +h -21 -77 0 +h -21 -26 0 +h -21 -78 0 +h -21 -27 0 +h -21 -79 0 +h -21 -28 0 +h -21 -80 0 +h -21 -29 0 +h -21 -81 0 +h -21 -30 0 +h -21 -31 0 +h -21 -32 0 +h -21 -33 0 +h -21 -34 0 +h -21 -35 0 +h -21 -36 0 +h -21 -37 0 +h -21 -38 0 +h -21 -39 0 +h -21 -40 0 +h -21 -41 0 +h -21 -42 0 +h -21 -43 0 +h -21 -44 0 +h -21 -45 0 +h -21 -46 0 +h -21 -47 0 +h -21 -48 0 +h -21 -49 0 +h -21 -50 0 +h -21 -51 0 +h -21 -52 0 +h -22 -71 0 +h -22 -72 0 +h -22 -73 0 +h -22 -74 0 +h -22 -23 0 +h -22 -75 0 +h -22 -24 0 +h -22 -76 0 +h -22 -25 0 +h -22 -77 0 +h -22 -26 0 +h -22 -78 0 +h -22 -27 0 +h -22 -79 0 +h -22 -28 0 +h -22 -80 0 +h -22 -29 0 +h -22 -81 0 +h -22 -30 0 +h -22 -82 0 +h -22 -31 0 +h -22 -32 0 +h -22 -33 0 +h -22 -34 0 +h -22 -35 0 +h -22 -36 0 +h -22 -37 0 +h -22 -38 0 +h -22 -39 0 +h -22 -40 0 +h -22 -41 0 +h -22 -42 0 +h -22 -43 0 +h -22 -44 0 +h -22 -45 0 +h -22 -46 0 +h -22 -47 0 +h -22 -48 0 +h -22 -49 0 +h -22 -50 0 +h -22 -51 0 +h -22 -52 0 +h -23 -72 0 +h -23 -73 0 +h -23 -74 0 +h -23 -75 0 +h -23 -24 0 +h -23 -76 0 +h -23 -25 0 +h -23 -77 0 +h -23 -26 0 +h -23 -78 0 +h -23 -27 0 +h -23 -79 0 +h -23 -28 0 +h -23 -80 0 +h -23 -29 0 +h -23 -81 0 +h -23 -30 0 +h -23 -82 0 +h -23 -31 0 +h -23 -83 0 +h -23 -32 0 +h -23 -33 0 +h -23 -34 0 +h -23 -35 0 +h -23 -36 0 +h -23 -37 0 +h -23 -38 0 +h -23 -39 0 +h -23 -40 0 +h -23 -41 0 +h -23 -42 0 +h -23 -43 0 +h -23 -44 0 +h -23 -45 0 +h -23 -46 0 +h -23 -47 0 +h -23 -48 0 +h -23 -49 0 +h -23 -50 0 +h -23 -51 0 +h -23 -52 0 +h -24 -73 0 +h -24 -74 0 +h -24 -75 0 +h -24 -76 0 +h -24 -25 0 +h -24 -77 0 +h -24 -26 0 +h -24 -78 0 +h -24 -27 0 +h -24 -79 0 +h -24 -28 0 +h -24 -80 0 +h -24 -29 0 +h -24 -81 0 +h -24 -30 0 +h -24 -82 0 +h -24 -31 0 +h -24 -83 0 +h -24 -32 0 +h -24 -84 0 +h -24 -33 0 +h -24 -34 0 +h -24 -35 0 +h -24 -36 0 +h -24 -37 0 +h -24 -38 0 +h -24 -39 0 +h -24 -40 0 +h -24 -41 0 +h -24 -42 0 +h -24 -43 0 +h -24 -44 0 +h -24 -45 0 +h -24 -46 0 +h -24 -47 0 +h -24 -48 0 +h -24 -49 0 +h -24 -50 0 +h -24 -51 0 +h -24 -52 0 +h -25 -74 0 +h -25 -75 0 +h -25 -76 0 +h -25 -77 0 +h -25 -26 0 +h -25 -78 0 +h -25 -27 0 +h -25 -79 0 +h -25 -28 0 +h -25 -80 0 +h -25 -29 0 +h -25 -81 0 +h -25 -30 0 +h -25 -82 0 +h -25 -31 0 +h -25 -83 0 +h -25 -32 0 +h -25 -84 0 +h -25 -33 0 +h -25 -85 0 +h -25 -34 0 +h -25 -35 0 +h -25 -36 0 +h -25 -37 0 +h -25 -38 0 +h -25 -39 0 +h -25 -40 0 +h -25 -41 0 +h -25 -42 0 +h -25 -43 0 +h -25 -44 0 +h -25 -45 0 +h -25 -46 0 +h -25 -47 0 +h -25 -48 0 +h -25 -49 0 +h -25 -50 0 +h -25 -51 0 +h -25 -52 0 +h -26 -75 0 +h -26 -76 0 +h -26 -77 0 +h -26 -78 0 +h -26 -27 0 +h -26 -79 0 +h -26 -28 0 +h -26 -80 0 +h -26 -29 0 +h -26 -81 0 +h -26 -30 0 +h -26 -82 0 +h -26 -31 0 +h -26 -83 0 +h -26 -32 0 +h -26 -84 0 +h -26 -33 0 +h -26 -85 0 +h -26 -34 0 +h -26 -86 0 +h -26 -35 0 +h -26 -36 0 +h -26 -37 0 +h -26 -38 0 +h -26 -39 0 +h -26 -40 0 +h -26 -41 0 +h -26 -42 0 +h -26 -43 0 +h -26 -44 0 +h -26 -45 0 +h -26 -46 0 +h -26 -47 0 +h -26 -48 0 +h -26 -49 0 +h -26 -50 0 +h -26 -51 0 +h -26 -52 0 +h -27 -76 0 +h -27 -77 0 +h -27 -78 0 +h -27 -79 0 +h -27 -28 0 +h -27 -80 0 +h -27 -29 0 +h -27 -81 0 +h -27 -30 0 +h -27 -82 0 +h -27 -31 0 +h -27 -83 0 +h -27 -32 0 +h -27 -84 0 +h -27 -33 0 +h -27 -85 0 +h -27 -34 0 +h -27 -86 0 +h -27 -35 0 +h -27 -36 0 +h -27 -37 0 +h -27 -38 0 +h -27 -39 0 +h -27 -40 0 +h -27 -41 0 +h -27 -42 0 +h -27 -43 0 +h -27 -44 0 +h -27 -45 0 +h -27 -46 0 +h -27 -47 0 +h -27 -48 0 +h -27 -49 0 +h -27 -50 0 +h -27 -51 0 +h -27 -52 0 +h -28 -77 0 +h -28 -78 0 +h -28 -79 0 +h -28 -80 0 +h -28 -29 0 +h -28 -81 0 +h -28 -30 0 +h -28 -82 0 +h -28 -31 0 +h -28 -83 0 +h -28 -32 0 +h -28 -84 0 +h -28 -33 0 +h -28 -85 0 +h -28 -34 0 +h -28 -86 0 +h -28 -35 0 +h -28 -36 0 +h -28 -37 0 +h -28 -38 0 +h -28 -39 0 +h -28 -40 0 +h -28 -41 0 +h -28 -42 0 +h -28 -43 0 +h -28 -44 0 +h -28 -45 0 +h -28 -46 0 +h -28 -47 0 +h -28 -48 0 +h -28 -49 0 +h -28 -50 0 +h -28 -51 0 +h -28 -52 0 +h -29 -78 0 +h -29 -79 0 +h -29 -80 0 +h -29 -81 0 +h -29 -30 0 +h -29 -82 0 +h -29 -31 0 +h -29 -83 0 +h -29 -32 0 +h -29 -84 0 +h -29 -33 0 +h -29 -85 0 +h -29 -34 0 +h -29 -86 0 +h -29 -35 0 +h -29 -36 0 +h -29 -37 0 +h -29 -38 0 +h -29 -39 0 +h -29 -40 0 +h -29 -41 0 +h -29 -42 0 +h -29 -43 0 +h -29 -44 0 +h -29 -45 0 +h -29 -46 0 +h -29 -47 0 +h -29 -48 0 +h -29 -49 0 +h -29 -50 0 +h -29 -51 0 +h -29 -52 0 +h -30 -79 0 +h -30 -80 0 +h -30 -81 0 +h -30 -82 0 +h -30 -31 0 +h -30 -83 0 +h -30 -32 0 +h -30 -84 0 +h -30 -33 0 +h -30 -85 0 +h -30 -34 0 +h -30 -86 0 +h -30 -35 0 +h -30 -36 0 +h -30 -37 0 +h -30 -38 0 +h -30 -39 0 +h -30 -40 0 +h -30 -41 0 +h -30 -42 0 +h -30 -43 0 +h -30 -44 0 +h -30 -45 0 +h -30 -46 0 +h -30 -47 0 +h -30 -48 0 +h -30 -49 0 +h -30 -50 0 +h -30 -51 0 +h -30 -52 0 +h -31 -80 0 +h -31 -81 0 +h -31 -82 0 +h -31 -83 0 +h -31 -32 0 +h -31 -84 0 +h -31 -33 0 +h -31 -85 0 +h -31 -34 0 +h -31 -86 0 +h -31 -35 0 +h -31 -36 0 +h -31 -37 0 +h -31 -38 0 +h -31 -39 0 +h -31 -40 0 +h -31 -41 0 +h -31 -42 0 +h -31 -43 0 +h -31 -44 0 +h -31 -45 0 +h -31 -46 0 +h -31 -47 0 +h -31 -48 0 +h -31 -49 0 +h -31 -50 0 +h -31 -51 0 +h -31 -52 0 +h -32 -81 0 +h -32 -82 0 +h -32 -83 0 +h -32 -84 0 +h -32 -33 0 +h -32 -85 0 +h -32 -34 0 +h -32 -86 0 +h -32 -35 0 +h -32 -36 0 +h -32 -37 0 +h -32 -38 0 +h -32 -39 0 +h -32 -40 0 +h -32 -41 0 +h -32 -42 0 +h -32 -43 0 +h -32 -44 0 +h -32 -45 0 +h -32 -46 0 +h -32 -47 0 +h -32 -48 0 +h -32 -49 0 +h -32 -50 0 +h -32 -51 0 +h -32 -52 0 +h -33 -82 0 +h -33 -83 0 +h -33 -84 0 +h -33 -85 0 +h -33 -34 0 +h -33 -86 0 +h -33 -35 0 +h -33 -36 0 +h -33 -37 0 +h -33 -38 0 +h -33 -39 0 +h -33 -40 0 +h -33 -41 0 +h -33 -42 0 +h -33 -43 0 +h -33 -44 0 +h -33 -45 0 +h -33 -46 0 +h -33 -47 0 +h -33 -48 0 +h -33 -49 0 +h -33 -50 0 +h -33 -51 0 +h -33 -52 0 +h -34 -83 0 +h -34 -84 0 +h -34 -85 0 +h -34 -86 0 +h -34 -35 0 +h -34 -36 0 +h -34 -37 0 +h -34 -38 0 +h -34 -39 0 +h -34 -40 0 +h -34 -41 0 +h -34 -42 0 +h -34 -43 0 +h -34 -44 0 +h -34 -45 0 +h -34 -46 0 +h -34 -47 0 +h -34 -48 0 +h -34 -49 0 +h -34 -50 0 +h -34 -51 0 +h -34 -52 0 +h -35 -84 0 +h -35 -85 0 +h -35 -86 0 +h -35 -36 0 +h -35 -37 0 +h -35 -38 0 +h -35 -39 0 +h -35 -40 0 +h -35 -41 0 +h -35 -42 0 +h -35 -43 0 +h -35 -44 0 +h -35 -45 0 +h -35 -46 0 +h -35 -47 0 +h -35 -48 0 +h -35 -49 0 +h -35 -50 0 +h -35 -51 0 +h -35 -52 0 +h -36 -85 0 +h -36 -86 0 +h -36 -37 0 +h -36 -38 0 +h -36 -39 0 +h -36 -40 0 +h -36 -41 0 +h -36 -42 0 +h -36 -43 0 +h -36 -44 0 +h -36 -45 0 +h -36 -46 0 +h -36 -47 0 +h -36 -48 0 +h -36 -49 0 +h -36 -50 0 +h -36 -51 0 +h -36 -52 0 +h -37 -86 0 +h -37 -38 0 +h -37 -39 0 +h -37 -40 0 +h -37 -41 0 +h -37 -42 0 +h -37 -43 0 +h -37 -44 0 +h -37 -45 0 +h -37 -46 0 +h -37 -47 0 +h -37 -48 0 +h -37 -49 0 +h -37 -50 0 +h -37 -51 0 +h -37 -52 0 +h -38 -39 0 +h -38 -40 0 +h -38 -41 0 +h -38 -42 0 +h -38 -43 0 +h -38 -44 0 +h -38 -45 0 +h -38 -46 0 +h -38 -47 0 +h -38 -48 0 +h -38 -49 0 +h -38 -50 0 +h -38 -51 0 +h -38 -52 0 +h -39 -40 0 +h -39 -41 0 +h -39 -42 0 +h -39 -43 0 +h -39 -44 0 +h -39 -45 0 +h -39 -46 0 +h -39 -47 0 +h -39 -48 0 +h -39 -49 0 +h -39 -50 0 +h -39 -51 0 +h -39 -52 0 +h -40 -41 0 +h -40 -42 0 +h -40 -43 0 +h -40 -44 0 +h -40 -45 0 +h -40 -46 0 +h -40 -47 0 +h -40 -48 0 +h -40 -49 0 +h -40 -50 0 +h -40 -51 0 +h -40 -52 0 +h -41 -42 0 +h -41 -43 0 +h -41 -44 0 +h -41 -45 0 +h -41 -46 0 +h -41 -47 0 +h -41 -48 0 +h -41 -49 0 +h -41 -50 0 +h -41 -51 0 +h -41 -52 0 +h -42 -43 0 +h -42 -44 0 +h -42 -45 0 +h -42 -46 0 +h -42 -47 0 +h -42 -48 0 +h -42 -49 0 +h -42 -50 0 +h -42 -51 0 +h -42 -52 0 +h -43 -44 0 +h -43 -45 0 +h -43 -46 0 +h -43 -47 0 +h -43 -48 0 +h -43 -49 0 +h -43 -50 0 +h -43 -51 0 +h -43 -52 0 +h -44 -45 0 +h -44 -46 0 +h -44 -47 0 +h -44 -48 0 +h -44 -49 0 +h -44 -50 0 +h -44 -51 0 +h -44 -52 0 +h -45 -46 0 +h -45 -47 0 +h -45 -48 0 +h -45 -49 0 +h -45 -50 0 +h -45 -51 0 +h -45 -52 0 +h -46 -47 0 +h -46 -48 0 +h -46 -49 0 +h -46 -50 0 +h -46 -51 0 +h -46 -52 0 +h -47 -48 0 +h -47 -49 0 +h -47 -50 0 +h -47 -51 0 +h -47 -52 0 +h -48 -49 0 +h -48 -50 0 +h -48 -51 0 +h -48 -52 0 +h -49 -50 0 +h -49 -51 0 +h -49 -52 0 +h -50 -51 0 +h -50 -52 0 +h -51 -52 0 +h -53 -54 0 +h -53 -55 0 +h -53 -56 0 +h -53 -57 0 +h -53 -58 0 +h -53 -59 0 +h -53 -60 0 +h -53 -61 0 +h -53 -62 0 +h -53 -63 0 +h -53 -64 0 +h -53 -65 0 +h -53 -66 0 +h -53 -67 0 +h -53 -68 0 +h -53 -69 0 +h -53 -70 0 +h -53 -71 0 +h -53 -72 0 +h -53 -73 0 +h -53 -74 0 +h -53 -75 0 +h -53 -76 0 +h -53 -77 0 +h -53 -78 0 +h -53 -79 0 +h -53 -80 0 +h -53 -81 0 +h -53 -82 0 +h -53 -83 0 +h -53 -84 0 +h -53 -85 0 +h -53 -86 0 +h -54 -55 0 +h -54 -56 0 +h -54 -57 0 +h -54 -58 0 +h -54 -59 0 +h -54 -60 0 +h -54 -61 0 +h -54 -62 0 +h -54 -63 0 +h -54 -64 0 +h -54 -65 0 +h -54 -66 0 +h -54 -67 0 +h -54 -68 0 +h -54 -69 0 +h -54 -70 0 +h -54 -71 0 +h -54 -72 0 +h -54 -73 0 +h -54 -74 0 +h -54 -75 0 +h -54 -76 0 +h -54 -77 0 +h -54 -78 0 +h -54 -79 0 +h -54 -80 0 +h -54 -81 0 +h -54 -82 0 +h -54 -83 0 +h -54 -84 0 +h -54 -85 0 +h -54 -86 0 +h -55 -56 0 +h -55 -57 0 +h -55 -58 0 +h -55 -59 0 +h -55 -60 0 +h -55 -61 0 +h -55 -62 0 +h -55 -63 0 +h -55 -64 0 +h -55 -65 0 +h -55 -66 0 +h -55 -67 0 +h -55 -68 0 +h -55 -69 0 +h -55 -70 0 +h -55 -71 0 +h -55 -72 0 +h -55 -73 0 +h -55 -74 0 +h -55 -75 0 +h -55 -76 0 +h -55 -77 0 +h -55 -78 0 +h -55 -79 0 +h -55 -80 0 +h -55 -81 0 +h -55 -82 0 +h -55 -83 0 +h -55 -84 0 +h -55 -85 0 +h -55 -86 0 +h -56 -57 0 +h -56 -58 0 +h -56 -59 0 +h -56 -60 0 +h -56 -61 0 +h -56 -62 0 +h -56 -63 0 +h -56 -64 0 +h -56 -65 0 +h -56 -66 0 +h -56 -67 0 +h -56 -68 0 +h -56 -69 0 +h -56 -70 0 +h -56 -71 0 +h -56 -72 0 +h -56 -73 0 +h -56 -74 0 +h -56 -75 0 +h -56 -76 0 +h -56 -77 0 +h -56 -78 0 +h -56 -79 0 +h -56 -80 0 +h -56 -81 0 +h -56 -82 0 +h -56 -83 0 +h -56 -84 0 +h -56 -85 0 +h -56 -86 0 +h -57 -58 0 +h -57 -59 0 +h -57 -60 0 +h -57 -61 0 +h -57 -62 0 +h -57 -63 0 +h -57 -64 0 +h -57 -65 0 +h -57 -66 0 +h -57 -67 0 +h -57 -68 0 +h -57 -69 0 +h -57 -70 0 +h -57 -71 0 +h -57 -72 0 +h -57 -73 0 +h -57 -74 0 +h -57 -75 0 +h -57 -76 0 +h -57 -77 0 +h -57 -78 0 +h -57 -79 0 +h -57 -80 0 +h -57 -81 0 +h -57 -82 0 +h -57 -83 0 +h -57 -84 0 +h -57 -85 0 +h -57 -86 0 +h -58 -59 0 +h -58 -60 0 +h -58 -61 0 +h -58 -62 0 +h -58 -63 0 +h -58 -64 0 +h -58 -65 0 +h -58 -66 0 +h -58 -67 0 +h -58 -68 0 +h -58 -69 0 +h -58 -70 0 +h -58 -71 0 +h -58 -72 0 +h -58 -73 0 +h -58 -74 0 +h -58 -75 0 +h -58 -76 0 +h -58 -77 0 +h -58 -78 0 +h -58 -79 0 +h -58 -80 0 +h -58 -81 0 +h -58 -82 0 +h -58 -83 0 +h -58 -84 0 +h -58 -85 0 +h -58 -86 0 +h -59 -60 0 +h -59 -61 0 +h -59 -62 0 +h -59 -63 0 +h -59 -64 0 +h -59 -65 0 +h -59 -66 0 +h -59 -67 0 +h -59 -68 0 +h -59 -69 0 +h -59 -70 0 +h -59 -71 0 +h -59 -72 0 +h -59 -73 0 +h -59 -74 0 +h -59 -75 0 +h -59 -76 0 +h -59 -77 0 +h -59 -78 0 +h -59 -79 0 +h -59 -80 0 +h -59 -81 0 +h -59 -82 0 +h -59 -83 0 +h -59 -84 0 +h -59 -85 0 +h -59 -86 0 +h -60 -61 0 +h -60 -62 0 +h -60 -63 0 +h -60 -64 0 +h -60 -65 0 +h -60 -66 0 +h -60 -67 0 +h -60 -68 0 +h -60 -69 0 +h -60 -70 0 +h -60 -71 0 +h -60 -72 0 +h -60 -73 0 +h -60 -74 0 +h -60 -75 0 +h -60 -76 0 +h -60 -77 0 +h -60 -78 0 +h -60 -79 0 +h -60 -80 0 +h -60 -81 0 +h -60 -82 0 +h -60 -83 0 +h -60 -84 0 +h -60 -85 0 +h -60 -86 0 +h -61 -62 0 +h -61 -63 0 +h -61 -64 0 +h -61 -65 0 +h -61 -66 0 +h -61 -67 0 +h -61 -68 0 +h -61 -69 0 +h -61 -70 0 +h -61 -71 0 +h -61 -72 0 +h -61 -73 0 +h -61 -74 0 +h -61 -75 0 +h -61 -76 0 +h -61 -77 0 +h -61 -78 0 +h -61 -79 0 +h -61 -80 0 +h -61 -81 0 +h -61 -82 0 +h -61 -83 0 +h -61 -84 0 +h -61 -85 0 +h -61 -86 0 +h -62 -63 0 +h -62 -64 0 +h -62 -65 0 +h -62 -66 0 +h -62 -67 0 +h -62 -68 0 +h -62 -69 0 +h -62 -70 0 +h -62 -71 0 +h -62 -72 0 +h -62 -73 0 +h -62 -74 0 +h -62 -75 0 +h -62 -76 0 +h -62 -77 0 +h -62 -78 0 +h -62 -79 0 +h -62 -80 0 +h -62 -81 0 +h -62 -82 0 +h -62 -83 0 +h -62 -84 0 +h -62 -85 0 +h -62 -86 0 +h -63 -64 0 +h -63 -65 0 +h -63 -66 0 +h -63 -67 0 +h -63 -68 0 +h -63 -69 0 +h -63 -70 0 +h -63 -71 0 +h -63 -72 0 +h -63 -73 0 +h -63 -74 0 +h -63 -75 0 +h -63 -76 0 +h -63 -77 0 +h -63 -78 0 +h -63 -79 0 +h -63 -80 0 +h -63 -81 0 +h -63 -82 0 +h -63 -83 0 +h -63 -84 0 +h -63 -85 0 +h -63 -86 0 +h -64 -65 0 +h -64 -66 0 +h -64 -67 0 +h -64 -68 0 +h -64 -69 0 +h -64 -70 0 +h -64 -71 0 +h -64 -72 0 +h -64 -73 0 +h -64 -74 0 +h -64 -75 0 +h -64 -76 0 +h -64 -77 0 +h -64 -78 0 +h -64 -79 0 +h -64 -80 0 +h -64 -81 0 +h -64 -82 0 +h -64 -83 0 +h -64 -84 0 +h -64 -85 0 +h -64 -86 0 +h -65 -66 0 +h -65 -67 0 +h -65 -68 0 +h -65 -69 0 +h -65 -70 0 +h -65 -71 0 +h -65 -72 0 +h -65 -73 0 +h -65 -74 0 +h -65 -75 0 +h -65 -76 0 +h -65 -77 0 +h -65 -78 0 +h -65 -79 0 +h -65 -80 0 +h -65 -81 0 +h -65 -82 0 +h -65 -83 0 +h -65 -84 0 +h -65 -85 0 +h -65 -86 0 +h -66 -67 0 +h -66 -68 0 +h -66 -69 0 +h -66 -70 0 +h -66 -71 0 +h -66 -72 0 +h -66 -73 0 +h -66 -74 0 +h -66 -75 0 +h -66 -76 0 +h -66 -77 0 +h -66 -78 0 +h -66 -79 0 +h -66 -80 0 +h -66 -81 0 +h -66 -82 0 +h -66 -83 0 +h -66 -84 0 +h -66 -85 0 +h -66 -86 0 +h -67 -68 0 +h -67 -69 0 +h -67 -70 0 +h -67 -71 0 +h -67 -72 0 +h -67 -73 0 +h -67 -74 0 +h -67 -75 0 +h -67 -76 0 +h -67 -77 0 +h -67 -78 0 +h -67 -79 0 +h -67 -80 0 +h -67 -81 0 +h -67 -82 0 +h -67 -83 0 +h -67 -84 0 +h -67 -85 0 +h -67 -86 0 +h -68 -69 0 +h -68 -70 0 +h -68 -71 0 +h -68 -72 0 +h -68 -73 0 +h -68 -74 0 +h -68 -75 0 +h -68 -76 0 +h -68 -77 0 +h -68 -78 0 +h -68 -79 0 +h -68 -80 0 +h -68 -81 0 +h -68 -82 0 +h -68 -83 0 +h -68 -84 0 +h -68 -85 0 +h -68 -86 0 +h -69 -70 0 +h -69 -71 0 +h -69 -72 0 +h -69 -73 0 +h -69 -74 0 +h -69 -75 0 +h -69 -76 0 +h -69 -77 0 +h -69 -78 0 +h -69 -79 0 +h -69 -80 0 +h -69 -81 0 +h -69 -82 0 +h -69 -83 0 +h -69 -84 0 +h -69 -85 0 +h -69 -86 0 +h -70 -71 0 +h -70 -72 0 +h -70 -73 0 +h -70 -74 0 +h -70 -75 0 +h -70 -76 0 +h -70 -77 0 +h -70 -78 0 +h -70 -79 0 +h -70 -80 0 +h -70 -81 0 +h -70 -82 0 +h -70 -83 0 +h -70 -84 0 +h -70 -85 0 +h -70 -86 0 +h -71 -72 0 +h -71 -73 0 +h -71 -74 0 +h -71 -75 0 +h -71 -76 0 +h -71 -77 0 +h -71 -78 0 +h -71 -79 0 +h -71 -80 0 +h -71 -81 0 +h -71 -82 0 +h -71 -83 0 +h -71 -84 0 +h -71 -85 0 +h -71 -86 0 +h -72 -73 0 +h -72 -74 0 +h -72 -75 0 +h -72 -76 0 +h -72 -77 0 +h -72 -78 0 +h -72 -79 0 +h -72 -80 0 +h -72 -81 0 +h -72 -82 0 +h -72 -83 0 +h -72 -84 0 +h -72 -85 0 +h -72 -86 0 +h -73 -74 0 +h -73 -75 0 +h -73 -76 0 +h -73 -77 0 +h -73 -78 0 +h -73 -79 0 +h -73 -80 0 +h -73 -81 0 +h -73 -82 0 +h -73 -83 0 +h -73 -84 0 +h -73 -85 0 +h -73 -86 0 +h -74 -75 0 +h -74 -76 0 +h -74 -77 0 +h -74 -78 0 +h -74 -79 0 +h -74 -80 0 +h -74 -81 0 +h -74 -82 0 +h -74 -83 0 +h -74 -84 0 +h -74 -85 0 +h -74 -86 0 +h -75 -76 0 +h -75 -77 0 +h -75 -78 0 +h -75 -79 0 +h -75 -80 0 +h -75 -81 0 +h -75 -82 0 +h -75 -83 0 +h -75 -84 0 +h -75 -85 0 +h -75 -86 0 +h -76 -77 0 +h -76 -78 0 +h -76 -79 0 +h -76 -80 0 +h -76 -81 0 +h -76 -82 0 +h -76 -83 0 +h -76 -84 0 +h -76 -85 0 +h -76 -86 0 +h -77 -78 0 +h -77 -79 0 +h -77 -80 0 +h -77 -81 0 +h -77 -82 0 +h -77 -83 0 +h -77 -84 0 +h -77 -85 0 +h -77 -86 0 +h -78 -79 0 +h -78 -80 0 +h -78 -81 0 +h -78 -82 0 +h -78 -83 0 +h -78 -84 0 +h -78 -85 0 +h -78 -86 0 +h -79 -80 0 +h -79 -81 0 +h -79 -82 0 +h -79 -83 0 +h -79 -84 0 +h -79 -85 0 +h -79 -86 0 +h -80 -81 0 +h -80 -82 0 +h -80 -83 0 +h -80 -84 0 +h -80 -85 0 +h -80 -86 0 +h -81 -82 0 +h -81 -83 0 +h -81 -84 0 +h -81 -85 0 +h -81 -86 0 +h -82 -83 0 +h -82 -84 0 +h -82 -85 0 +h -82 -86 0 +h -83 -84 0 +h -83 -85 0 +h -83 -86 0 +h -84 -85 0 +h -84 -86 0 +h -85 -86 0 diff --git a/src/algs/maxsat.rs b/src/algs/maxsat.rs index 4c84a3d1..4a1a2d93 100644 --- a/src/algs/maxsat.rs +++ b/src/algs/maxsat.rs @@ -4,81 +4,91 @@ //! Note that these implementations do not form competitive MaxSAT solvers and are not optimized //! for maximum performance. +use std::marker::PhantomData; + use crate::{ encodings::pb, - instances::{BasicVarManager, ManageVars, Objective}, + instances::BasicVarManager, solvers::{SolveIncremental, SolveStats, SolverResult}, - types::{Assignment, Clause, Lit}, + types::{Assignment, Lit, TernaryVal}, }; -/// Performs solution-improving search on an optimization instance +/// Trait for SAT-based MaxSAT solving algorithms +pub trait Solve { + /// The SAT solver used in solving + type Solver: SolveIncremental + SolveStats; + + /// Solves the MaxSAT instance + /// + /// The constraints need to all be in the [`Self::Solver`] instance already. + fn solve(solver: &mut Self::Solver, objective: &[(Lit, usize)]) -> Option<(Assignment, usize)>; +} + +fn objective_value(obj: &[(Lit, usize)], sol: &Assignment) -> usize { + obj.iter().fold(0, |sum, (l, w)| { + if sol.lit_value(*l) == TernaryVal::True { + sum + w + } else { + sum + } + }) +} + +/// Abstract type for solution-improving MaxSAT algorithm /// -/// The generic `S` is the SAT solver to be used. The generic `PBE` is the pseudo-Boolean encoding -/// to be used for encoding the objective. +/// The generic `Solver` is the SAT solver to be used. The generic `PbEnc` is the pseudo-Boolean +/// encoding to be used for encoding the objective. /// /// # References /// /// - Fahiem Bacchus and Matti Järvisalo and Ruben Martins: _Maximum Satisfiability_, in Handbook -/// of Satisfiability 2021. +/// of Satisfiability 2021. /// /// # Panics /// /// - If any interaction with the solver errors /// - If the objective value overflows [`isize::MAX`] -pub fn solution_improving_search( - solver: &mut S, - objective: &Objective, -) -> Option<(Assignment, isize)> +pub struct SolutionImprovingSearch { + slv: PhantomData, + enc: PhantomData, +} + +impl Solve for SolutionImprovingSearch where - S: SolveIncremental + SolveStats, - PBE: FromIterator<(Lit, usize)> + pb::BoundUpperIncremental, + Solver: SolveIncremental + SolveStats, + PbEnc: FromIterator<(Lit, usize)> + pb::BoundUpperIncremental, { - let Some(max_var) = std::cmp::max(solver.max_var(), objective.max_var()) else { - return Some((Assignment::default(), objective.offset())); - }; - let mut vm = BasicVarManager::from_next_free(max_var + 1); - let handle_soft_cls = |(mut cl, w): (Clause, usize)| { - debug_assert!(!cl.is_empty()); - if cl.len() == 1 { - return Some((!cl[0], w)); - } - let blit = vm.new_lit(); - cl.add(blit); - solver - .add_clause(cl) - .expect("error adding clause to solver"); - Some((!blit, w)) - }; - let mut enc: PBE = objective - .iter_soft_cls() - .into_iter() - .filter_map(handle_soft_cls) - .collect(); + type Solver = Solver; - let mut sol = None; + fn solve(solver: &mut Self::Solver, objective: &[(Lit, usize)]) -> Option<(Assignment, usize)> { + let Some(max_var) = solver.max_var() else { + return Some((Assignment::default(), 0)); + }; + let mut vm = BasicVarManager::from_next_free(max_var + 1); + let mut enc: PbEnc = objective.iter().copied().collect(); - loop { - match solver.solve().expect("solver error while solving") { - SolverResult::Sat => { - let assign = solver.solution(max_var).expect("failed getting solution"); - let val = objective.evaluate_no_offset(&assign); - sol = Some(( - assign, - objective.offset() + isize::try_from(val).expect("objective value overflow"), - )); - if val == 0 { - return sol; - } - enc.encode_ub(val - 1..val, solver, &mut vm) - .expect("error adding clauses to solver"); - for unit in enc.enforce_ub(val - 1).expect("invalid encoding usage") { - solver - .add_unit(unit) - .expect("error adding clause to solver"); + let mut sol = None; + + loop { + match solver.solve().expect("solver error while solving") { + SolverResult::Sat => { + let assign = solver.solution(max_var).expect("failed getting solution"); + let val = objective_value(&objective, &assign); + sol = Some((assign, val)); + if val == 0 { + return sol; + } + enc.encode_ub(val - 1..val, solver, &mut vm) + .expect("error adding clauses to solver"); + for unit in enc.enforce_ub(val - 1).expect("invalid encoding usage") { + solver + .add_unit(unit) + .expect("error adding clause to solver"); + } } + SolverResult::Unsat => return sol, + SolverResult::Interrupted => unreachable!(), } - SolverResult::Unsat => return sol, - SolverResult::Interrupted => unreachable!(), } } } diff --git a/src/instances/opt.rs b/src/instances/opt.rs index 2024e4b9..832ec719 100644 --- a/src/instances/opt.rs +++ b/src/instances/opt.rs @@ -12,7 +12,7 @@ use crate::{ algs::maxsat, clause, encodings::{card, pb}, - solvers::{SolveIncremental, SolveStats}, + solvers::Solve, types::{ constraints::{CardConstraint, PbConstraint}, Assignment, Clause, ClsIter, Lit, LitIter, RsHashMap, TernaryVal, Var, WClsIter, WLitIter, @@ -1601,24 +1601,48 @@ impl Instance { Self::from_opb_with_idx(&mut reader, obj_idx, opts) } - /// Find the optimal solution to this instance with solution improving search as implemented in - /// [`crate::algs::maxsat::solution_improving_search`] + /// Solves the instance with a [`maxsat::Solve`] algorithm /// /// # Panics /// /// - If any interaction with the solver errors /// - If the objective value overflows [`isize::MAX`] - pub fn solution_improving_search(self) -> Option<(Assignment, isize)> + pub fn solve_maxsat(self) -> Option<(Assignment, isize)> where - S: Default + SolveIncremental + SolveStats, - PBE: FromIterator<(Lit, usize)> + pb::BoundUpperIncremental, + Alg: maxsat::Solve, + Alg::Solver: Default, { - let mut solver = S::default(); - let (cnf, _) = self.constrs.into_cnf(); + let mut solver = Alg::Solver::default(); + let (cnf, vm) = self.constrs.into_cnf(); + let mut vm = if let Some(max_var) = cmp::max(vm.max_var(), self.obj.max_var()) { + BasicVarManager::from_next_free(max_var + 1) + } else { + BasicVarManager::default() + }; solver .add_cnf(cnf) .expect("failed adding clauses to solver"); - maxsat::solution_improving_search::(&mut solver, &self.obj) + let handle_soft_cls = |(mut cl, weight): (Clause, usize)| { + debug_assert!(!cl.is_empty()); + if cl.len() == 1 { + return (!cl[0], weight); + } + let blit = vm.new_lit(); + cl.add(!blit); + solver + .add_clause(cl) + .expect("failed adding clause to solver"); + (blit, weight) + }; + let (iter, offset) = self.obj.into_soft_cls(); + let obj: Vec<_> = iter.into_iter().map(handle_soft_cls).collect(); + let (sol, cost) = Alg::solve(&mut solver, &obj)?; + Some(( + sol, + offset + .checked_add_unsigned(cost) + .expect("objective value overflow"), + )) } } diff --git a/tests/maxsat.rs b/tests/maxsat.rs index 9b1b0dde..354dd808 100644 --- a/tests/maxsat.rs +++ b/tests/maxsat.rs @@ -1,11 +1,20 @@ -use rustsat::instances::OptInstance; +use rustsat::{algs::maxsat, encodings::pb, instances::OptInstance}; #[test] -fn sis() { +fn sis_small() { + type Alg = maxsat::SolutionImprovingSearch; let inst: OptInstance = OptInstance::from_dimacs_path("./data/inc-sis-fails.wcnf").unwrap(); - let sol = inst - .solution_improving_search::( - ); + let sol = inst.solve_maxsat::(); dbg!(&sol); assert!(matches!(sol, Some((_, 8632)))); } + +#[test] +fn sis() { + type Alg = maxsat::SolutionImprovingSearch; + let inst: OptInstance = + OptInstance::from_dimacs_path("./data/auctions_wt-cat_sched_60_70_0003.txt.wcnf").unwrap(); + let sol = inst.solve_maxsat::(); + dbg!(&sol); + assert!(matches!(sol, Some((_, 61169)))); +} From dc54982448f745e695ade41766aa4b32bad87c8c Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Mon, 10 Mar 2025 14:10:35 +0200 Subject: [PATCH 3/3] fixup! feat: SIS MaxSAT algorithm --- src/algs/maxsat.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algs/maxsat.rs b/src/algs/maxsat.rs index 4a1a2d93..ef06b481 100644 --- a/src/algs/maxsat.rs +++ b/src/algs/maxsat.rs @@ -73,7 +73,7 @@ where match solver.solve().expect("solver error while solving") { SolverResult::Sat => { let assign = solver.solution(max_var).expect("failed getting solution"); - let val = objective_value(&objective, &assign); + let val = objective_value(objective, &assign); sol = Some((assign, val)); if val == 0 { return sol;