結果
問題 | No.1421 国勢調査 (Hard) |
ユーザー | togatoga |
提出日時 | 2021-03-08 10:14:23 |
言語 | Rust (1.77.0 + proconio) |
結果 |
TLE
|
実行時間 | - |
コード長 | 64,032 bytes |
コンパイル時間 | 15,422 ms |
コンパイル使用メモリ | 380,084 KB |
実行使用メモリ | 62,592 KB |
最終ジャッジ日時 | 2024-10-09 19:25:22 |
合計ジャッジ時間 | 30,483 ms |
ジャッジサーバーID (参考情報) |
judge3 / judge2 |
(要ログイン)
テストケース
テストケース表示入力 | 結果 | 実行時間 実行使用メモリ |
---|---|---|
testcase_00 | AC | 1 ms
10,496 KB |
testcase_01 | AC | 2 ms
5,248 KB |
testcase_02 | AC | 1,108 ms
32,512 KB |
testcase_03 | AC | 1,352 ms
35,712 KB |
testcase_04 | TLE | - |
testcase_05 | AC | 1,624 ms
39,680 KB |
testcase_06 | AC | 1,904 ms
43,264 KB |
testcase_07 | TLE | - |
testcase_08 | TLE | - |
testcase_09 | -- | - |
testcase_10 | -- | - |
testcase_11 | -- | - |
testcase_12 | -- | - |
testcase_13 | -- | - |
testcase_14 | -- | - |
testcase_15 | -- | - |
testcase_16 | -- | - |
testcase_17 | -- | - |
testcase_18 | -- | - |
testcase_19 | -- | - |
testcase_20 | -- | - |
testcase_21 | -- | - |
testcase_22 | -- | - |
testcase_23 | -- | - |
testcase_24 | -- | - |
testcase_25 | -- | - |
testcase_26 | -- | - |
testcase_27 | -- | - |
testcase_28 | -- | - |
testcase_29 | -- | - |
testcase_30 | -- | - |
testcase_31 | -- | - |
コンパイルメッセージ
warning: unused borrow that must be used --> src/main.rs:1524:26 | 1524 | unsafe { &mut (*watchers_ptr)[!clause[1]].push(w) }; | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the borrow produces a value | = note: `#[warn(unused_must_use)]` on by default help: use `let _ = ...` to ignore the resulting value | 1524 | unsafe { let _ = &mut (*watchers_ptr)[!clause[1]].push(w); }; | +++++++ +
ソースコード
// The main code is at the very bottom. #[allow(unused_imports)] use { lib::byte::ByteChar, std::cell::{Cell, RefCell}, std::cmp::{ self, Ordering::{self, *}, Reverse, }, std::collections::*, std::convert::identity, std::fmt::{self, Debug, Display, Formatter}, std::io::prelude::*, std::iter::{self, FromIterator}, std::marker::PhantomData, std::mem, std::num::Wrapping, std::ops::{Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive}, std::process, std::rc::Rc, std::thread, std::time::{Duration, Instant}, std::{char, f32, f64, i128, i16, i32, i64, i8, isize, str, u128, u16, u32, u64, u8, usize}, }; #[allow(unused_imports)] #[macro_use] pub mod lib { pub mod byte { pub use self::byte_char::*; mod byte_char { use std::error::Error; use std::fmt::{self, Debug, Display, Formatter}; use std::str::FromStr; #[derive(Clone, Copy, Default, PartialEq, Eq, PartialOrd, Ord, Hash)] #[repr(transparent)] pub struct ByteChar(pub u8); impl Debug for ByteChar { fn fmt(&self, f: &mut Formatter) -> fmt::Result { write!(f, "b'{}'", self.0 as char) } } impl Display for ByteChar { fn fmt(&self, f: &mut Formatter) -> fmt::Result { write!(f, "{}", self.0 as char) } } impl FromStr for ByteChar { type Err = ParseByteCharError; fn from_str(s: &str) -> Result<ByteChar, ParseByteCharError> { match s.as_bytes().len() { 1 => Ok(ByteChar(s.as_bytes()[0])), 0 => Err(ParseByteCharErrorKind::EmptyStr.into()), _ => Err(ParseByteCharErrorKind::TooManyBytes.into()), } } } #[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] pub struct ParseByteCharError { kind: ParseByteCharErrorKind, } impl Display for ParseByteCharError { fn fmt(&self, f: &mut Formatter) -> fmt::Result { f.write_str(match self.kind { ParseByteCharErrorKind::EmptyStr => "empty string", ParseByteCharErrorKind::TooManyBytes => "too many bytes", }) } } impl Error for ParseByteCharError {} #[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] enum ParseByteCharErrorKind { EmptyStr, TooManyBytes, } impl From<ParseByteCharErrorKind> for ParseByteCharError { fn from(kind: ParseByteCharErrorKind) -> ParseByteCharError { ParseByteCharError { kind } } } } } pub mod io { pub use self::scanner::*; mod scanner { use std::io::{self, BufRead}; use std::iter; use std::str::FromStr; #[derive(Debug)] pub struct Scanner<R> { reader: R, buf: String, pos: usize, } impl<R: BufRead> Scanner<R> { pub fn new(reader: R) -> Self { Scanner { reader, buf: String::new(), pos: 0, } } pub fn next(&mut self) -> io::Result<&str> { let start = loop { match self.rest().find(|c| c != ' ') { Some(i) => break i, None => self.fill_buf()?, } }; self.pos += start; let len = self.rest().find(' ').unwrap_or(self.rest().len()); let s = &self.buf[self.pos..][..len]; // self.rest()[..len] self.pos += len; Ok(s) } pub fn parse_next<T>(&mut self) -> io::Result<Result<T, T::Err>> where T: FromStr, { Ok(self.next()?.parse()) } pub fn parse_next_n<T>(&mut self, n: usize) -> io::Result<Result<Vec<T>, T::Err>> where T: FromStr, { iter::repeat_with(|| self.parse_next()).take(n).collect() } pub fn map_next_bytes<T, F>(&mut self, mut f: F) -> io::Result<Vec<T>> where F: FnMut(u8) -> T, { Ok(self.next()?.bytes().map(&mut f).collect()) } pub fn map_next_bytes_n<T, F>(&mut self, n: usize, mut f: F) -> io::Result<Vec<Vec<T>>> where F: FnMut(u8) -> T, { iter::repeat_with(|| self.map_next_bytes(&mut f)) .take(n) .collect() } fn rest(&self) -> &str { &self.buf[self.pos..] } fn fill_buf(&mut self) -> io::Result<()> { self.buf.clear(); self.pos = 0; let read = self.reader.read_line(&mut self.buf)?; if read == 0 { return Err(io::ErrorKind::UnexpectedEof.into()); } if *self.buf.as_bytes().last().unwrap() == b'\n' { self.buf.pop(); } Ok(()) } } } } } // https://github.com/togatoga/screwsat/tree/088bdf73960140da090b5132bc635b26c08531cb // // LICENSE: // // MIT License // // Copyright (c) 2019 Hitoshi Togasaki // // Permission is hereby granted, free of charge, to any person obtaining a copy // of this software and associated documentation files (the "Software"), to deal // in the Software without restriction, including without limitation the rights // to use, copy, modify, merge, publish, distribute, sublicense, and/or sell // copies of the Software, and to permit persons to whom the Software is // furnished to do so, subject to the following conditions: // // The above copyright notice and this permission notice shall be included in all // copies or substantial portions of the Software. // // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, // OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE // SOFTWARE. // MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson // Copyright (c) 2007-2010 Niklas Sorensson // RatSat -- Copyright (c) 2018-2018, Masaki Hara // // Permission is hereby granted, free of charge, to any person obtaining a // copy of this software and associated documentation files (the // "Software"), to deal in the Software without restriction, including // without limitation the rights to use, copy, modify, merge, publish, // distribute, sublicense, and/or sell copies of the Software, and to // permit persons to whom the Software is furnished to do so, subject to // the following conditions: // // The above copyright notice and this permission notice shall be included // in all copies or substantial portions of the Software. // // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS // OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #[allow(dead_code)] mod screwsat { pub mod solver { use std::{ fmt, marker::PhantomData, ops::{Index, IndexMut}, time::{Duration, Instant}, vec, }; const TOP_LEVEL: usize = 0; #[derive(Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash, Clone, Copy)] pub struct Var(pub u32); impl Var { #[allow(dead_code)] fn from_idx(x: usize) -> Var { Var(x as u32) } } #[derive(Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash, Clone, Copy)] pub struct Lit(u32); impl Lit { pub fn new(var: u32, positive: bool) -> Lit { Lit(if positive { var << 1 } else { (var << 1) + 1 }) } #[inline] pub fn var(self) -> Var { Var(self.0 >> 1) } #[inline] pub fn pos(&self) -> bool { self.0 & 1 == 0 } #[inline] pub fn neg(&self) -> bool { self.0 & 1 != 0 } } impl From<i32> for Lit { #[inline] fn from(x: i32) -> Self { debug_assert!(x != 0); let d = x.abs() as u32 - 1; if x > 0 { Lit(d << 1) } else { Lit((d << 1) + 1) } } } impl std::ops::Not for Lit { type Output = Self; #[inline] fn not(self) -> Self::Output { Lit(self.0 ^ 1) } } struct ClauseRef<'a> { header: ClauseHeader, clause: &'a [ClauseData], extra: Option<ClauseData>, } impl<'a> ClauseRef<'a> { fn activity(&self) -> f32 { unsafe { self.extra.as_ref().expect("No activity").act } } fn len(&self) -> usize { self.clause.len() } #[allow(dead_code)] fn iter(&self) -> ClauseIter { ClauseIter(self.clause.iter()) } pub fn reloced(&self) -> bool { self.header.reloced() } #[allow(dead_code)] pub fn relocation(&self) -> CRef { debug_assert!(self.reloced()); unsafe { self.clause[0].cref } } } impl<'a> Index<usize> for ClauseRef<'a> { type Output = Lit; fn index(&self, idx: usize) -> &Self::Output { unsafe { &self.clause[idx].lit } } } struct ClauseMut<'a> { header: &'a mut ClauseHeader, clause: &'a mut [ClauseData], extra: Option<&'a mut ClauseData>, } impl<'a> ClauseMut<'a> { fn set_activity(&mut self, act: f32) { self.extra.as_mut().expect("No extra field").act = act; } fn activity(&self) -> f32 { unsafe { self.extra.as_ref().expect("No activity").act } } fn len(&self) -> usize { self.clause.len() } fn swap(&mut self, x: usize, y: usize) { self.clause.swap(x, y); } #[allow(dead_code)] fn iter(&self) -> ClauseIter { ClauseIter(self.clause.iter()) } #[allow(dead_code)] fn iter_mut(&mut self) -> ClauseIterMut { ClauseIterMut(self.clause.iter_mut()) } pub fn reloced(&self) -> bool { self.header.reloced() } pub fn relocation(&self) -> CRef { debug_assert!(self.reloced()); unsafe { self.clause[0].cref } } pub fn set_reloced(&mut self, reloced: bool) { self.header.set_reloced(reloced); } pub fn relocate(mut self, c: CRef) { debug_assert!(!self.reloced()); self.set_reloced(true); self.clause[0].cref = c; } pub fn as_clause_ref(&mut self) -> ClauseRef { ClauseRef { header: *self.header, clause: self.clause, extra: self.extra.as_mut().map(|extra| **extra), } } } impl<'a> Index<usize> for ClauseMut<'a> { type Output = Lit; fn index(&self, idx: usize) -> &Self::Output { unsafe { &self.clause[idx].lit } } } impl<'a> IndexMut<usize> for ClauseMut<'a> { fn index_mut(&mut self, index: usize) -> &mut Self::Output { unsafe { &mut self.clause[index as usize].lit } } } #[derive(Debug, Clone)] pub struct ClauseIter<'a>(std::slice::Iter<'a, ClauseData>); impl<'a> Iterator for ClauseIter<'a> { type Item = &'a Lit; fn next(&mut self) -> Option<Self::Item> { self.0.next().map(|lit| unsafe { &lit.lit }) } fn size_hint(&self) -> (usize, Option<usize>) { self.0.size_hint() } } impl<'a> DoubleEndedIterator for ClauseIter<'a> { fn next_back(&mut self) -> Option<Self::Item> { self.0.next_back().map(|lit| unsafe { &lit.lit }) } } #[derive(Debug)] pub struct ClauseIterMut<'a>(std::slice::IterMut<'a, ClauseData>); impl<'a> Iterator for ClauseIterMut<'a> { type Item = &'a mut Lit; fn next(&mut self) -> Option<Self::Item> { self.0.next().map(|lit| unsafe { &mut lit.lit }) } fn size_hint(&self) -> (usize, Option<usize>) { self.0.size_hint() } } impl<'a> DoubleEndedIterator for ClauseIterMut<'a> { fn next_back(&mut self) -> Option<Self::Item> { self.0.next_back().map(|lit| unsafe { &mut lit.lit }) } } #[derive(Debug)] struct RegionAllocator<T: Copy + Default> { data: Vec<T>, wasted: usize, } #[derive(Debug, Default, Clone, Copy)] struct Ref<T: Copy>(usize, PhantomData<T>); impl<T: Copy> PartialEq for Ref<T> { fn eq(&self, other: &Self) -> bool { self.0 == other.0 } } impl<T: Copy> std::ops::Add<usize> for Ref<T> { type Output = Ref<T>; fn add(self, rhs: usize) -> Self::Output { Ref(self.0 + rhs, PhantomData) } } impl<T: Copy + Default> RegionAllocator<T> { fn new() -> RegionAllocator<T> { RegionAllocator { data: Vec::with_capacity(1024 * 1024), wasted: 0, } } fn with_capacity(n: usize) -> RegionAllocator<T> { RegionAllocator { data: Vec::with_capacity(n), wasted: 0, } } fn len(&self) -> usize { self.data.len() } fn capacity(&self) -> usize { self.data.capacity() } fn free(&mut self, size: usize) { debug_assert!(size <= self.capacity()); self.wasted += size; } fn wasted(&self) -> usize { self.wasted } fn alloc(&mut self, size: usize) -> Ref<T> { let r = self.len(); self.data.extend((0..size).map(|_| T::default())); Ref(r, PhantomData) } pub fn subslice(&self, r: Ref<T>, len: usize) -> &[T] { debug_assert!(len <= self.len()); &self.data[r.0..r.0 + len] } pub fn subslice_mut(&mut self, r: Ref<T>, len: usize) -> &mut [T] { debug_assert!(len <= self.len()); &mut self.data[r.0..r.0 + len] } } impl<T: Copy + Default> Index<Ref<T>> for RegionAllocator<T> { type Output = T; fn index(&self, r: Ref<T>) -> &Self::Output { &self.data[r.0] } } impl<T: Copy + Default> IndexMut<Ref<T>> for RegionAllocator<T> { fn index_mut(&mut self, r: Ref<T>) -> &mut Self::Output { &mut self.data[r.0] } } #[derive(Clone, Copy)] #[repr(C)] union ClauseData { lit: Lit, abs: u32, act: f32, header: ClauseHeader, cref: CRef, } impl Default for ClauseData { fn default() -> Self { ClauseData { abs: 0 } } } impl fmt::Debug for ClauseData { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { f.debug_struct("ClauseData") .field("abs", unsafe { &self.abs }) .finish() } } #[derive(Clone, Copy)] pub struct ClauseHeader(u32); impl ClauseHeader { pub fn new(mark: u32, learnt: bool, has_extra: bool, reloced: bool, size: u32) -> Self { debug_assert!(mark < 4); debug_assert!(size < (1 << 27)); ClauseHeader( (mark << 30) | ((learnt as u32) << 29) | ((has_extra as u32) << 28) | ((reloced as u32) << 27) | size, ) } pub fn mark(&self) -> u32 { self.0 >> 30 } pub fn free(&self) -> bool { self.mark() == 1 } pub fn learnt(&self) -> bool { (self.0 & (1 << 29)) != 0 } pub fn has_extra(&self) -> bool { (self.0 & (1 << 28)) != 0 } pub fn reloced(&self) -> bool { (self.0 & (1 << 27)) != 0 } pub fn size(&self) -> u32 { self.0 & ((1 << 27) - 1) } pub fn set_mark(&mut self, mark: u32) { debug_assert!(mark < 4); self.0 = (self.0 & !(3 << 30)) | (mark << 30); } pub fn set_learnt(&mut self, learnt: bool) { self.0 = (self.0 & !(1 << 29)) | ((learnt as u32) << 29); } pub fn set_has_extra(&mut self, has_extra: bool) { self.0 = (self.0 & !(1 << 28)) | ((has_extra as u32) << 28); } pub fn set_reloced(&mut self, reloced: bool) { self.0 = (self.0 & !(1 << 27)) | ((reloced as u32) << 27); } pub fn set_size(&mut self, size: u32) { debug_assert!(size < (1 << 27)); self.0 = (self.0 & !((1 << 27) - 1)) | size; } } type CRef = Ref<ClauseData>; #[derive(Debug)] struct ClauseAllocator { ra: RegionAllocator<ClauseData>, } impl ClauseAllocator { fn new() -> ClauseAllocator { ClauseAllocator { ra: RegionAllocator::new(), } } fn with_capacity(n: usize) -> ClauseAllocator { ClauseAllocator { ra: RegionAllocator::with_capacity(n), } } fn unit_region(len: usize, extra: bool) -> usize { 1 + len + extra as usize } fn alloc(&mut self, clause: &[Lit], learnt: bool) -> CRef { let use_extra = learnt; let cid = self .ra .alloc(ClauseAllocator::unit_region(clause.len(), learnt)); self.ra[cid].header = ClauseHeader::new(0, learnt, use_extra, false, clause.len() as u32); let clause_ptr = cid + 1; for (i, &lit) in clause.iter().enumerate() { self.ra[clause_ptr + i as usize].lit = lit; } if learnt { self.ra[clause_ptr + clause.len() as usize].act = 0.0; } cid } pub fn alloc_copy(&mut self, from: ClauseRef) -> CRef { let use_extra = from.header.learnt(); let cid = self .ra .alloc(1 + from.header.size() as usize + use_extra as usize); self.ra[cid].header = from.header; unsafe { &mut self.ra[cid].header }.set_has_extra(use_extra); for (i, &lit) in from.iter().enumerate() { self.ra[cid + 1 + i as usize].lit = lit; } if use_extra { self.ra[cid + 1 + from.len() as usize] = from.extra.expect("Extra"); } cid } pub fn free(&mut self, cr: CRef) { let size = { let c = self.get(cr); 1 + c.len() + c.header.has_extra() as usize }; self.ra.free(size); } pub fn reloc(&mut self, cr: &mut CRef, to: &mut ClauseAllocator) { let mut c = self.get_mut(*cr); if c.header.reloced() { *cr = c.relocation(); return; } *cr = to.alloc_copy(c.as_clause_ref()); c.relocate(*cr); } fn get(&self, cref: CRef) -> ClauseRef { let header = unsafe { self.ra[cref].header }; let has_extra = header.has_extra(); let size = header.size(); let clause = self.ra.subslice(cref + 1, size as usize); let extra = if has_extra { Some(self.ra[cref + 1 + size as usize]) } else { None }; ClauseRef { header, clause, extra, } } fn get_mut(&mut self, cref: CRef) -> ClauseMut { let header = unsafe { self.ra[cref].header }; let has_extra = header.has_extra(); let size = header.size(); let len = 1 + size + has_extra as u32; let subslice = self.ra.subslice_mut(cref, len as usize); let (subslice0, subslice) = subslice.split_at_mut(1); let (subslice1, subslice2) = subslice.split_at_mut(size as usize); ClauseMut { header: unsafe { &mut subslice0[0].header }, clause: subslice1, extra: subslice2.first_mut(), } } fn len(&self) -> usize { self.ra.len() } fn wasted(&self) -> usize { self.ra.wasted() } } #[derive(Debug)] struct ClauseDB { clauses: Vec<CRef>, learnts: Vec<CRef>, db: ClauseAllocator, clause_inc: f32, } impl Default for ClauseDB { fn default() -> Self { ClauseDB { clauses: Vec::default(), learnts: Vec::default(), db: ClauseAllocator::new(), clause_inc: 1.0, } } } impl ClauseDB { fn bump_activity(&mut self, cr: CRef) { let act = { let mut clause = self.db.get_mut(cr); let new_act = clause.activity() + self.clause_inc as f32; clause.set_activity(new_act); new_act }; if act > 1e20 { let n: usize = self.learnts.len(); for i in 0..n { let x = self.learnts[i]; let mut clause = self.db.get_mut(x); debug_assert!(clause.header.learnt()); let new_act = clause.activity() * 1e-20; clause.set_activity(new_act); } self.clause_inc *= 1e-20; } } fn decay_inc(&mut self) { self.clause_inc /= 0.999; } pub fn push(&mut self, lits: &[Lit], learnt: bool) -> CRef { let cref = self.db.alloc(lits, learnt); if learnt { self.learnts.push(cref); } else { self.clauses.push(cref); } cref } fn need_collect_garbage(&mut self) -> bool { self.db.wasted() * 10 > self.db.len() * 2 } fn collect_garbage_if_needed( &mut self, watchers: &mut Vec<Vec<Watcher>>, bin_watchers: &mut Vec<Vec<Watcher>>, vardata: &mut VarData, ) { if self.need_collect_garbage() { self.collect_garbage(watchers, bin_watchers, vardata); } } fn collect_garbage( &mut self, watchers: &mut Vec<Vec<Watcher>>, bin_watchers: &mut Vec<Vec<Watcher>>, vardata: &mut VarData, ) { let mut to = ClauseAllocator::with_capacity(self.db.len() - self.db.wasted()); for watcher in watchers.iter_mut() { for ws in watcher.iter_mut() { self.db.reloc(&mut ws.cref, &mut to); } } for watcher in bin_watchers.iter_mut() { for ws in watcher.iter_mut() { self.db.reloc(&mut ws.cref, &mut to); } } { let trail = &vardata.trail.stack; for &lit in trail.iter() { let cond = if let Some(cref) = vardata.reason[lit.var()] { let c = self.db.get(cref); c.reloced() || vardata.locked(c[0], cref) } else { false }; if cond { let mut cref = vardata.reason[lit.var()].as_mut().expect("not found"); self.db.reloc(&mut cref, &mut to); } } } { let mut j = 0; for i in 0..self.learnts.len() { let mut cr = self.learnts[i]; let removed = self.db.get(cr).header.free(); if !removed { self.db.reloc(&mut cr, &mut to); self.learnts[j] = cr; j += 1; } } self.learnts.truncate(j); } { let mut j = 0; for i in 0..self.clauses.len() { let mut cr = self.clauses[i]; let removed = self.db.get(cr).header.free(); if !removed { self.db.reloc(&mut cr, &mut to); self.clauses[j] = cr; j += 1; } } self.clauses.truncate(j); } self.db = to; } } #[derive(PartialEq, Debug, Copy, Clone)] /// The status of a problem that solver solved. /// - `Sat` a solver found that a given problem is SATISFIABLE. /// - `Unsat` a solver found that a given problem is UNSATISFIABLE. /// - `Indeterminate` a solver stopped searching. pub enum Status { Sat, Unsat, Indeterminate, } #[derive(PartialEq, Debug, Copy, Clone)] pub enum LitBool { True = 0, False = 1, Undef = 2, } impl From<i8> for LitBool { #[inline] fn from(x: i8) -> Self { match x { 0 => LitBool::True, 1 => LitBool::False, _ => LitBool::Undef, } } } impl<T> Index<Var> for Vec<T> { type Output = T; #[inline] fn index(&self, var: Var) -> &Self::Output { #[cfg(feature = "unsafe")] unsafe { self.get_unchecked(var.0 as usize) } #[cfg(not(feature = "unsafe"))] &self[var.0 as usize] } } impl<T> IndexMut<Var> for Vec<T> { #[inline] fn index_mut(&mut self, var: Var) -> &mut Self::Output { #[cfg(feature = "unsafe")] unsafe { self.get_unchecked_mut(var.0 as usize) } #[cfg(not(feature = "unsafe"))] &mut self[var.0 as usize] } } impl<T> Index<Lit> for Vec<T> { type Output = T; #[inline] fn index(&self, lit: Lit) -> &Self::Output { #[cfg(feature = "unsafe")] unsafe { &self.get_unchecked(lit.0 as usize) } #[cfg(not(feature = "unsafe"))] &self[lit.0 as usize] } } impl<T> IndexMut<Lit> for Vec<T> { #[inline] fn index_mut(&mut self, lit: Lit) -> &mut Self::Output { #[cfg(feature = "unsafe")] unsafe { self.get_unchecked_mut(lit.0 as usize) } #[cfg(not(feature = "unsafe"))] &mut self[lit.0 as usize] } } #[derive(Debug, Clone)] struct Heap { heap: Vec<Var>, indices: Vec<Option<usize>>, activity: Vec<f64>, bump_inc: f64, } impl Default for Heap { fn default() -> Self { Heap { heap: Vec::default(), indices: Vec::default(), activity: Vec::default(), bump_inc: 1.0, } } } impl Heap { pub fn new(n: usize, bump_inc: f64) -> Heap { Heap { heap: (0..n).map(|x| Var(x as u32)).collect(), indices: (0..n).map(Some).collect(), activity: vec![0.0; n], bump_inc, } } fn gt(&self, left: Var, right: Var) -> bool { self.activity[left] > self.activity[right] } #[allow(dead_code)] fn top(self) -> Option<Var> { if self.heap.is_empty() { return None; } Some(self.heap[0]) } pub fn decay_inc(&mut self) { self.bump_inc /= 0.95; } pub fn bump_activity(&mut self, v: Var) { self.activity[v] += self.bump_inc; if self.activity[v] >= 1e100 { for i in 0..self.activity.len() { self.activity[i] *= 1e-100; } self.bump_inc *= 1e-100; } if self.in_heap(v) { let idx = self.indices[v].expect("No index"); self.up(idx); } } #[allow(dead_code)] fn update(&mut self, v: Var) { if !self.in_heap(v) { self.push(v); } else { let idx = self.indices[v].unwrap(); self.up(idx); self.down(idx); } } fn up(&mut self, i: usize) { if i == 0 { return; } let mut idx = i; let x = self.heap[idx]; let mut par = (idx - 1) >> 1; loop { if !self.gt(x, self.heap[par]) { break; } self.heap[idx] = self.heap[par]; self.indices[self.heap[par]] = Some(idx); idx = par; if idx == 0 { break; } par = (par - 1) >> 1; } self.heap[idx] = x; self.indices[x] = Some(idx); } fn pop(&mut self) -> Option<Var> { if self.heap.is_empty() { return None; } let x = self.heap[0]; self.indices[x] = None; if self.heap.len() > 1 { self.heap[0] = *self.heap.last().unwrap(); self.indices[self.heap[0]] = Some(0); } self.heap.pop(); if self.heap.len() > 1 { self.down(0); } Some(x) } fn down(&mut self, i: usize) { let x = self.heap[i]; let mut idx = i; while 2 * idx + 1 < self.heap.len() { let left = 2 * idx + 1; let right = left + 1; let child = if right < self.heap.len() && self.gt(self.heap[right], self.heap[left]) { right } else { left }; if self.gt(self.heap[child], x) { self.heap[idx] = self.heap[child]; self.indices[self.heap[idx]] = Some(idx); idx = child; } else { break; } } self.heap[idx] = x; self.indices[x] = Some(idx); } fn push(&mut self, v: Var) { if self.in_heap(v) { return; } while (v.0 as usize) >= self.indices.len() { self.indices.push(None); self.activity.push(0.0); } self.indices[v] = Some(self.heap.len()); self.heap.push(v); self.up(self.indices[v].expect("No index")); } fn in_heap(&mut self, v: Var) -> bool { (v.0 as usize) < self.indices.len() && self.indices[v].is_some() } } #[derive(Debug, Default)] struct Analayzer { seen: Vec<bool>, ccmin_stack: Vec<CRef>, ccmin_clear: Vec<Lit>, analyze_toclear: Vec<Lit>, learnt_clause: Vec<Lit>, } impl Analayzer { fn new(n: usize) -> Analayzer { Analayzer { seen: vec![false; n], ccmin_stack: Vec::new(), ccmin_clear: Vec::new(), learnt_clause: Vec::new(), analyze_toclear: Vec::new(), } } } /// The assignment data structure #[derive(Debug, Default)] struct AssignTrail { /// Assignment stack; stores all assigments made in the order they were made. stack: Vec<Lit>, /// Separator indices for different decision levels in `trail`. stack_limit: Vec<usize>, /// Head of the `trail`. peek_head: usize, } impl AssignTrail { fn new() -> AssignTrail { AssignTrail { stack: Vec::new(), stack_limit: Vec::new(), peek_head: 0, } } fn new_descion_level(&mut self) { self.stack_limit.push(self.stack.len()); } #[inline] fn decision_level(&self) -> usize { self.stack_limit.len() } #[inline] fn peekable(&self) -> bool { self.peek_head < self.stack.len() } #[inline] fn peek(&self) -> Lit { self.stack[self.peek_head] } #[inline] fn advance(&mut self) { self.peek_head += 1; } fn push(&mut self, x: Lit) { self.stack.push(x); } } #[derive(Debug, Default)] struct VarData { /// assignments for each variable assigns: Vec<LitBool>, polarity: Vec<bool>, /// decision level(0: minimumlevel) level: Vec<usize>, reason: Vec<Option<CRef>>, trail: AssignTrail, } impl VarData { fn new(n: usize) -> VarData { VarData { assigns: vec![LitBool::Undef; n], polarity: vec![false; n], level: vec![TOP_LEVEL; n], reason: vec![None; n], trail: AssignTrail::new(), } } fn assign(&mut self, var: Var, lb: LitBool, level: usize, reason: Option<CRef>) { self.assigns[var] = lb; self.level[var] = level; self.reason[var] = reason; } fn level(&self, v: Var) -> usize { self.level[v] } #[inline] fn eval(&self, lit: Lit) -> LitBool { LitBool::from(self.assigns[lit.var()] as i8 ^ lit.neg() as i8) } fn locked(&self, c: Lit, cref: CRef) -> bool { if self.eval(c) == LitBool::True { if let Some(reason) = self.reason[c.var()].as_ref() { return *reason == cref; } } false } fn num_assings(&self) -> usize { self.trail.stack.len() } /// Enqueue a variable to assign a `value` to a boolean `assign` fn enqueue(&mut self, lit: Lit, reason: Option<CRef>) { debug_assert!(self.eval(lit) == LitBool::Undef); debug_assert!(self.level(lit.var()) == TOP_LEVEL); self.assign( lit.var(), LitBool::from(lit.neg() as i8), self.trail.decision_level(), reason, ); self.trail.push(lit); } } #[derive(Debug, Clone, Copy)] struct RestartStrategy { /// The initial restart limit. (default 100) first: i32, /// The factor with which the restart limit is multiplied in each restart. (default 2.5) inc: f64, } impl Default for RestartStrategy { fn default() -> Self { RestartStrategy { first: 100, inc: 2.5, } } } impl RestartStrategy { fn luby(&mut self, mut x: i32) -> f64 { let mut size = 1; let mut seq = 0; while size < x + 1 { seq += 1; size = 2 * size + 1; } while size - 1 != x { size = (size - 1) >> 1; seq -= 1; x %= size; } f64::powi(self.inc, seq) * self.first as f64 } } #[derive(Debug, Clone, Copy)] struct LearntSizeStrategy { /// The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) factor: f64, /// The limit for learnt clauses is multiplied with this factor each restart. (default 1.1) inc: f64, /// (default 1.5) adjust_inc: f64, adjust_start_confl: i32, adjust_confl: f64, adjust_cnt: i32, max_learnts: f64, } impl Default for LearntSizeStrategy { fn default() -> Self { LearntSizeStrategy { factor: 1.0 / 3.0, inc: 1.1, adjust_start_confl: 100, adjust_inc: 1.5, adjust_cnt: 0, adjust_confl: 0.0, max_learnts: 0.0, } } } impl LearntSizeStrategy { fn init(&mut self, num_clauses: usize) { self.max_learnts = num_clauses as f64 * self.factor; self.adjust_confl = self.adjust_start_confl as f64; self.reset_adjust_cnt(); } fn dec_adjust_cnt(&mut self) { self.adjust_cnt -= 1; } fn adjust_if_needed(&mut self) { if self.adjust_cnt <= 0 { self.adjust(); } } fn reset_adjust_cnt(&mut self) { self.adjust_cnt = self.adjust_confl as i32; } fn adjust(&mut self) { self.adjust_confl *= self.adjust_inc; self.reset_adjust_cnt(); self.max_learnts *= self.inc; } } #[derive(Debug, Default, Clone, Copy)] struct Watcher { cref: CRef, blocker: Lit, } impl Watcher { fn new(cref: CRef, blocker: Lit) -> Watcher { Watcher { cref, blocker } } } #[derive(Debug, Default, Clone, Copy)] struct SimplifyDB { /// Number of top-level assignments since last execution of 'simplify()'. simp_db_assigns: i32, } #[derive(Debug, Default)] pub struct Solver { n: usize, db: ClauseDB, watchers: Vec<Vec<Watcher>>, bin_watchers: Vec<Vec<Watcher>>, analyzer: Analayzer, vardata: VarData, order_heap: Heap, restart_strat: RestartStrategy, learnt_size_start: LearntSizeStrategy, simplify_db: SimplifyDB, pub models: Vec<LitBool>, pub status: Option<Status>, } impl Solver { /// Create a new `Solver` struct /// /// # Arguments /// * `n` - The number of variable /// * `clauses` - All clauses that solver solves pub fn new(n: usize, clauses: &[Vec<Lit>]) -> Solver { let mut solver = Solver { n, db: ClauseDB::default(), analyzer: Analayzer::new(n), vardata: VarData::new(n), order_heap: Heap::new(n, 1.0), restart_strat: RestartStrategy::default(), learnt_size_start: LearntSizeStrategy::default(), simplify_db: SimplifyDB::default(), watchers: vec![vec![]; 2 * n], bin_watchers: vec![vec![]; 2 * n], status: None, models: vec![LitBool::Undef; n], }; clauses.iter().for_each(|clause| { if clause.len() == 1 { solver.vardata.enqueue(clause[0], None); } else { solver.add_clause(clause); } }); solver } pub fn new_var(&mut self) { let v = Var(self.n as u32); self.n += 1; self.vardata.assigns.push(LitBool::Undef); self.vardata.polarity.push(false); self.vardata.reason.push(None); self.vardata.level.push(TOP_LEVEL); self.order_heap.push(v); self.analyzer.seen.push(false); self.models.push(LitBool::Undef); self.watchers.push(Vec::new()); self.watchers.push(Vec::new()); self.bin_watchers.push(Vec::new()); self.bin_watchers.push(Vec::new()); } /// This method is only for internal usage and almost same as `add_clause` /// But, this method doesn't grow the size of array. fn add_clause_db(&mut self, lits: &[Lit], learnt: bool) -> CRef { let cref = self.db.push(lits, learnt); debug_assert!(lits.len() >= 2); if lits.len() == 2 { self.bin_watchers[!lits[0]].push(Watcher::new(cref, lits[1])); self.bin_watchers[!lits[1]].push(Watcher::new(cref, lits[0])); } else { self.watchers[!lits[0]].push(Watcher::new(cref, lits[1])); self.watchers[!lits[1]].push(Watcher::new(cref, lits[0])); } cref } /// Add a new clause to `clauses` and watch a clause. /// If a variable is greater than the size of array, grow it. /// # Arguments /// * `clause` - a clause has one or some literal variables pub fn add_clause(&mut self, clause: &[Lit]) { debug_assert!(self.vardata.trail.decision_level() == TOP_LEVEL); clause.iter().for_each(|c| { while c.var().0 as usize >= self.vardata.assigns.len() { self.new_var(); } }); let mut clause = clause.to_vec(); clause.sort(); let mut len = 0; for i in 0..clause.len() { let mut remove = false; if i >= 1 { if clause[i] == !clause[i - 1] { return; } if clause[i] == clause[i - 1] { remove = true; } } let lit = clause[i]; match self.vardata.eval(lit) { LitBool::True => { return; } LitBool::False => { remove = true; } _ => {} } if !remove { clause[len] = lit; len += 1; } } clause.truncate(len); if clause.is_empty() { self.status = Some(Status::Unsat); } else if clause.len() == 1 { let c = clause[0]; if self.vardata.eval(c) == LitBool::False { self.status = Some(Status::Unsat); } self.vardata.enqueue(c, None); if self.propagate().is_some() { self.status = Some(Status::Unsat); } } else { debug_assert!(clause.len() >= 2); let l1 = clause[0]; let l2 = clause[1]; let cref = self.db.push(&clause, false); if clause.len() == 2 { self.bin_watchers[!l1].push(Watcher::new(cref, l2)); self.bin_watchers[!l2].push(Watcher::new(cref, l1)); } else { self.watchers[!l1].push(Watcher::new(cref, l2)); self.watchers[!l2].push(Watcher::new(cref, l1)); } } } /// Propagate it by all enqueued values and check conflicts. /// If a conflict is detected, this function returns a conflicted clause index. /// `None` is no conflicts. fn propagate(&mut self) -> Option<CRef> { let mut conflict = None; 'conflict: while self.vardata.trail.peekable() { let p = self.vardata.trail.peek(); self.vardata.trail.advance(); debug_assert!(self.vardata.assigns[p.var()] != LitBool::Undef); { let ws = &self.bin_watchers[p]; for w in ws.iter() { let imp = w.blocker; debug_assert!({ let clause = self.db.db.get(w.cref); debug_assert!(clause.len() == 2); true }); let mut clause = self.db.db.get_mut(w.cref); if clause[0] == !p { clause.swap(0, 1); } match self.vardata.eval(imp) { LitBool::False => { self.vardata.trail.peek_head = self.vardata.trail.stack.len(); return Some(w.cref); } LitBool::Undef => { self.vardata.enqueue(imp, Some(w.cref)); } _ => {} } } } let mut idx = 0; let watchers_ptr = &mut self.watchers as *mut Vec<Vec<Watcher>>; let ws = &mut self.watchers[p]; 'next_clause: while idx < ws.len() { let blocker = ws[idx].blocker; if self.vardata.eval(blocker) == LitBool::True { idx += 1; continue; } let cr = ws[idx].cref; let mut clause = self.db.db.get_mut(cr); debug_assert!(!clause.header.free()); debug_assert!(clause[0] == !p || clause[1] == !p); if clause[0] == !p { clause.swap(0, 1); } let first = clause[0]; let w = Watcher::new(cr, first); if first != blocker && self.vardata.eval(first) == LitBool::True { debug_assert!(first != clause[1]); ws[idx] = w; idx += 1; continue 'next_clause; } for k in 2..clause.len() { let lit = clause[k]; if self.vardata.eval(lit) != LitBool::False { clause.swap(1, k); ws.swap_remove(idx); unsafe { &mut (*watchers_ptr)[!clause[1]].push(w) }; continue 'next_clause; } } ws[idx] = w; if self.vardata.eval(first) == LitBool::False { self.vardata.trail.peek_head = self.vardata.trail.stack.len(); conflict = Some(cr); break 'conflict; } else { self.vardata.enqueue(first, Some(cr)); } idx += 1; } } conflict } fn unwatch_clause(&mut self, cref: CRef) { let clause = self.db.db.get(cref); if clause.len() == 2 { let ws = &mut self.bin_watchers[!clause[0]]; ws.swap_remove(ws.iter().position(|&w| w.cref == cref).expect("Not found")); let ws = &mut self.bin_watchers[!clause[1]]; ws.swap_remove(ws.iter().position(|&w| w.cref == cref).expect("Not found")); } else { let ws = &mut self.watchers[!clause[0]]; ws.swap_remove(ws.iter().position(|&w| w.cref == cref).expect("Not found")); let ws = &mut self.watchers[!clause[1]]; ws.swap_remove(ws.iter().position(|&w| w.cref == cref).expect("Not found")); } } fn reduce_learnts(&mut self) { let extra_lim = self.db.clause_inc / self.db.learnts.len() as f32; debug_assert!(!extra_lim.is_nan()); { let ca = &self.db.db; self.db.learnts.sort_unstable_by(|&x, &y| { let x = ca.get(x); let y = ca.get(y); Ord::cmp(&(x.len() <= 2), &(y.len() <= 2)) .then(PartialOrd::partial_cmp(&x.activity(), &y.activity()).expect("NaN activity")) }); } let mut new_size = 0; for i in 0..self.db.learnts.len() { let cr = self.db.learnts[i]; let cla = self.db.db.get(cr); let act = cla.activity(); let len = cla.len(); if (i < self.db.learnts.len() / 2 || act < extra_lim) && len > 2 && !self.vardata.locked(cla[0], cr) { self.detach_clause(cr); } else { self.db.learnts[new_size] = cr; new_size += 1; } } self.db.learnts.truncate(new_size); self.db.collect_garbage_if_needed( &mut self.watchers, &mut self.bin_watchers, &mut self.vardata, ); } fn pop_trail_until(&mut self, backtrack_level: usize) { if self.vardata.trail.decision_level() <= backtrack_level { return; } let trail = &mut self.vardata.trail; let sep = trail.stack_limit[backtrack_level]; for p in trail.stack.iter().skip(sep).rev() { let x = p.var(); if !self.order_heap.in_heap(x) { self.order_heap.push(x); } self.vardata.polarity[x] = p.pos(); self.vardata.assigns[x] = LitBool::Undef; self.vardata.reason[x] = None; self.vardata.level[x] = TOP_LEVEL; } trail.peek_head = sep; trail.stack.truncate(sep); trail.stack_limit.truncate(backtrack_level); } fn detach_if_satisfied(&mut self, cr: CRef) -> bool { let mut detach = false; let clause = self.db.db.get(cr); for &lit in clause.iter() { if self.vardata.eval(lit) == LitBool::True { self.detach_clause(cr); detach = true; break; } } detach } fn detach_clause(&mut self, cr: CRef) { let lit = self.db.db.get(cr)[0]; self.unwatch_clause(cr); if self.vardata.locked(lit, cr) { debug_assert!(self.vardata.reason[lit.var()].is_some()); self.vardata.reason[lit.var()] = None; } self.db.db.get_mut(cr).header.set_mark(1); self.db.db.free(cr); } fn simplify(&mut self) -> bool { debug_assert!(self.vardata.trail.decision_level() == TOP_LEVEL); if self.propagate().is_some() { return false; } if self.vardata.num_assings() as i32 == self.simplify_db.simp_db_assigns { return true; } { let n: usize = self.db.learnts.len(); let mut new_size = 0; for i in 0..n { let cr = self.db.learnts[i]; let detach = self.detach_if_satisfied(cr); if !detach { self.db.learnts[new_size] = cr; new_size += 1; } } self.db.learnts.truncate(new_size); } { let n: usize = self.db.clauses.len(); let mut new_size = 0; for i in 0..n { let cr = self.db.clauses[i]; let detach = self.detach_if_satisfied(cr); if !detach { self.db.clauses[new_size] = cr; new_size += 1; } } self.db.clauses.truncate(new_size); } self.db.collect_garbage_if_needed( &mut self.watchers, &mut self.bin_watchers, &mut self.vardata, ); self.simplify_db.simp_db_assigns = self.vardata.num_assings() as i32; true } fn lit_redundant(&mut self, cr: CRef, abstract_levels: u32) -> bool { let seen = &mut self.analyzer.seen; let ccmin_stack = &mut self.analyzer.ccmin_stack; let ccmin_clear = &mut self.analyzer.ccmin_clear; ccmin_stack.clear(); ccmin_stack.push(cr); let top = ccmin_clear.len(); let mut redundant = true; 'redundant: while let Some(cr) = ccmin_stack.pop() { let clause = self.db.db.get(cr); for c in clause.iter().skip(1) { if !seen[c.var()] && self.vardata.level(c.var()) > TOP_LEVEL { let intersect = Solver::abstract_level(self.vardata.level(c.var())) & abstract_levels != 0; if !intersect { redundant = false; break 'redundant; } if let Some(cr) = self.vardata.reason[c.var()] { seen[c.var()] = true; ccmin_stack.push(cr); ccmin_clear.push(*c); } else { redundant = false; break 'redundant; } } } } if !redundant { for lit in ccmin_clear.iter().skip(top) { seen[lit.var()] = false; } ccmin_clear.truncate(top); } redundant } fn abstract_level(level: usize) -> u32 { 1 << (level as u32 & 31) } fn minimize_conflict_clause(&mut self) { debug_assert!(self.analyzer.ccmin_stack.is_empty()); debug_assert!(self.analyzer.ccmin_clear.is_empty()); let abstract_levels = self .analyzer .learnt_clause .iter() .skip(1) .fold(0, |als: u32, x| { als | Solver::abstract_level(self.vardata.level(x.var())) }); let n: usize = self.analyzer.learnt_clause.len(); let mut new_size = 1; for i in 1..n { let lit = self.analyzer.learnt_clause[i]; let redundant = { if let Some(cr) = self.vardata.reason[lit.var()] { self.lit_redundant(cr, abstract_levels) } else { false } }; if !redundant { self.analyzer.learnt_clause[new_size] = lit; new_size += 1; } } for lit in self.analyzer.ccmin_clear.iter() { self.analyzer.seen[lit.var()] = false; } self.analyzer.ccmin_stack.clear(); self.analyzer.ccmin_clear.clear(); self.analyzer.learnt_clause.truncate(new_size); } /// Analyze a conflict clause and deduce a learnt clause to avoid a current conflict fn analyze(&mut self, confl: CRef) { debug_assert!(self.analyzer.seen.iter().all(|&x| !x)); let decision_level = self.vardata.trail.decision_level(); self.analyzer.learnt_clause.clear(); self.analyzer.learnt_clause.push(Lit::default()); let mut same_level_cnt = 0; { let learnt = self.db.db.get(confl).header.learnt(); if learnt { self.db.bump_activity(confl); } let clause = self.db.db.get(confl); debug_assert!(!clause.header.free()); for p in clause.iter() { let var = p.var(); debug_assert!(self.vardata.eval(*p) != LitBool::Undef); self.order_heap.bump_activity(var); self.analyzer.seen[var] = true; if self.vardata.level(var) < decision_level { self.analyzer.learnt_clause.push(*p); } else { same_level_cnt += 1; } } } let first_uip = { let mut p = None; for &lit in self.vardata.trail.stack.iter().rev() { let v = lit.var(); if !self.analyzer.seen[v] { continue; } self.analyzer.seen[v] = false; same_level_cnt -= 1; if same_level_cnt <= 0 { p = Some(lit); break; } debug_assert_eq!(self.vardata.level[v], decision_level); let reason = self.vardata.reason[v].as_ref().expect("No reason"); let learnt = self.db.db.get(*reason).header.learnt(); if learnt { self.db.bump_activity(*reason); } let clause = self.db.db.get(*reason); for p in clause.iter().skip(1) { let var = p.var(); if self.analyzer.seen[var] { continue; } self.order_heap.bump_activity(var); self.analyzer.seen[var] = true; debug_assert!(self.vardata.level(var) <= decision_level); if self.vardata.level(var) < decision_level { self.analyzer.learnt_clause.push(*p); } else { same_level_cnt += 1; } } } p }; self.analyzer.learnt_clause[0] = !first_uip.expect("not found first uip"); self .analyzer .analyze_toclear .clone_from(&self.analyzer.learnt_clause); let backtrack_level = if self.analyzer.learnt_clause.len() == 1 { TOP_LEVEL } else { let mut max_idx = 1; let mut max_level = self .vardata .level(self.analyzer.learnt_clause[max_idx].var()); for (i, lit) in self.analyzer.learnt_clause.iter().enumerate().skip(2) { if self.vardata.level(lit.var()) > max_level { max_level = self.vardata.level(lit.var()); max_idx = i; } } self.analyzer.learnt_clause.swap(1, max_idx); max_level }; self.pop_trail_until(backtrack_level); let first = self.analyzer.learnt_clause[0]; if self.analyzer.learnt_clause.len() == 1 { debug_assert_eq!(backtrack_level, TOP_LEVEL); self.vardata.enqueue(first, None); } else { let cr = self.add_clause_db(&self.analyzer.learnt_clause.clone(), true); self.db.bump_activity(cr); self.vardata.enqueue(first, Some(cr)); } for lit in self.analyzer.analyze_toclear.iter() { self.analyzer.seen[lit.var()] = false; } } fn define(&self, x: Var) -> bool { self.vardata.assigns[x] != LitBool::Undef } /// Reserve the space of a clause database /// # Arguments /// * `cla_num` - The number of clause pub fn reserve_clause(&mut self, cla_num: usize) { self.db.clauses.reserve(cla_num); } /// # Arguments /// * `var_num` - The number of variable pub fn reserve_variable(&mut self, var_num: usize) { self.vardata.trail.stack.reserve(var_num); self.db.clauses.reserve(var_num); self.vardata.reason.reserve(var_num); self.vardata.level.reserve(var_num); self.vardata.assigns.reserve(var_num); } fn search(&mut self, nof_conflicts: i32) -> Status { let mut conflict_cnt = 0; loop { if let Some(confl) = self.propagate() { conflict_cnt += 1; if self.vardata.trail.decision_level() == TOP_LEVEL { self.status = Some(Status::Unsat); return Status::Unsat; } self.analyze(confl); self.order_heap.decay_inc(); self.db.decay_inc(); self.learnt_size_start.dec_adjust_cnt(); self.learnt_size_start.adjust_if_needed(); } else { if conflict_cnt >= nof_conflicts { self.pop_trail_until(TOP_LEVEL); return Status::Indeterminate; } if self.vardata.trail.decision_level() == TOP_LEVEL && !self.simplify() { return Status::Unsat; } if self.learnt_size_start.max_learnts + self.vardata.trail.stack.len() as f64 <= self.db.learnts.len() as f64 { self.reduce_learnts(); } loop { if let Some(v) = self.order_heap.pop() { if self.define(v) { continue; } let lit = Lit::new(v.0, self.vardata.polarity[v]); self.vardata.trail.new_descion_level(); self.vardata.enqueue(lit, None); break; } else { self.status = Some(Status::Sat); self.models = self.vardata.assigns.clone(); return Status::Sat; } } } } } /// Solve a problem and return a enum `Status`. /// # Arguments /// * `time_limit` - The time limitation for searching. /// Exceeding the time limit returns `Indeterminate` pub fn solve(&mut self, time_limit: Option<Duration>) -> Status { if let Some(status) = self.status.as_ref() { return *status; } let start = Instant::now(); self.learnt_size_start.init(self.db.clauses.len()); let mut status = Status::Indeterminate; let mut restart_cnt = 0; while status == Status::Indeterminate { if let Some(time_limit) = time_limit { if start.elapsed() > time_limit { self.status = Some(Status::Indeterminate); return Status::Indeterminate; } } let nof_conflicts = self.restart_strat.luby(restart_cnt) as i32; status = self.search(nof_conflicts); restart_cnt += 1; } status } } } } #[allow(unused_macros)] macro_rules! eprint { ($($arg:tt)*) => { if cfg!(debug_assertions) { std::eprint!($($arg)*) } }; } #[allow(unused_macros)] macro_rules! eprintln { ($($arg:tt)*) => { if cfg!(debug_assertions) { std::eprintln!($($arg)*) } }; } #[allow(unused_macros)] macro_rules! dbg { ($($arg:tt)*) => { if cfg!(debug_assertions) { std::dbg!($($arg)*) } else { ($($arg)*) } }; } const CUSTOM_STACK_SIZE_MIB: Option<usize> = Some(1024); const INTERACTIVE: bool = false; fn main() -> std::io::Result<()> { match CUSTOM_STACK_SIZE_MIB { Some(stack_size_mib) => std::thread::Builder::new() .name("run_solver".to_owned()) .stack_size(stack_size_mib * 1024 * 1024) .spawn(run_solver)? .join() .unwrap(), None => run_solver(), } } fn run_solver() -> std::io::Result<()> { let stdin = std::io::stdin(); let reader = stdin.lock(); let stdout = std::io::stdout(); let writer = stdout.lock(); macro_rules! with_wrapper { ($($wrapper:expr)?) => {{ let mut writer = $($wrapper)?(writer); solve(reader, &mut writer)?; writer.flush() }}; } if cfg!(debug_assertions) || INTERACTIVE { with_wrapper!() } else { with_wrapper!(std::io::BufWriter::new) } } fn solve<R, W>(reader: R, mut writer: W) -> std::io::Result<()> where R: BufRead, W: Write, { let mut _scanner = lib::io::Scanner::new(reader); #[allow(unused_macros)] macro_rules! scan { ($T:ty) => { _scanner.parse_next::<$T>()?.unwrap() }; ($($T:ty),+) => { ($(scan!($T)),+) }; ($T:ty; $n:expr) => { _scanner.parse_next_n::<$T>($n)?.unwrap() }; ($($T:ty),+; $n:expr) => { iter::repeat_with(|| -> std::io::Result<_> { Ok(($(scan!($T)),+)) }) .take($n) .collect::<std::io::Result<Vec<_>>>()? }; } #[allow(unused_macros)] macro_rules! scan_bytes_map { ($f:expr) => { _scanner.map_next_bytes($f)? }; ($f:expr; $n:expr) => { _scanner.map_next_bytes_n($n, $f)? }; } #[allow(unused_macros)] macro_rules! print { ($($arg:tt)*) => { write!(writer, $($arg)*)? }; } #[allow(unused_macros)] macro_rules! println { ($($arg:tt)*) => { writeln!(writer, $($arg)*)? }; } #[allow(unused_macros)] macro_rules! answer { ($($arg:tt)*) => {{ println!($($arg)*); return Ok(()); }}; } { use screwsat::solver::*; let (n, m) = scan!(usize, usize); struct State { solver: Solver, v: u32, } impl State { fn new_var(&mut self) -> u32 { let v = self.v; self.v += 1; v } fn add_xor(&mut self, mut v: Vec<u32>, t: bool) { match v.len() { 0 => panic!(), 1 => { self.solver.add_clause(&[Lit::new(v[0], t)]); } 2 => { if t { self .solver .add_clause(&[Lit::new(v[0], false), Lit::new(v[1], false)]); self .solver .add_clause(&[Lit::new(v[0], true), Lit::new(v[1], true)]); } else { self .solver .add_clause(&[Lit::new(v[0], true), Lit::new(v[1], false)]); self .solver .add_clause(&[Lit::new(v[0], false), Lit::new(v[1], true)]); } } 3 => { if t { self.solver.add_clause(&[ Lit::new(v[0], true), Lit::new(v[1], true), Lit::new(v[2], true), ]); self.solver.add_clause(&[ Lit::new(v[0], true), Lit::new(v[1], false), Lit::new(v[2], false), ]); self.solver.add_clause(&[ Lit::new(v[0], false), Lit::new(v[1], true), Lit::new(v[2], false), ]); self.solver.add_clause(&[ Lit::new(v[0], false), Lit::new(v[1], false), Lit::new(v[2], true), ]); } else { self.solver.add_clause(&[ Lit::new(v[0], false), Lit::new(v[1], true), Lit::new(v[2], true), ]); self.solver.add_clause(&[ Lit::new(v[0], false), Lit::new(v[1], false), Lit::new(v[2], false), ]); self.solver.add_clause(&[ Lit::new(v[0], true), Lit::new(v[1], true), Lit::new(v[2], false), ]); self.solver.add_clause(&[ Lit::new(v[0], true), Lit::new(v[1], false), Lit::new(v[2], true), ]); } } _ => { let p = self.new_var(); let q = self.new_var(); self.add_xor(vec![p, q], true); let mut w = v.split_off(v.len() / 2); v.push(p); w.push(q); self.add_xor(v, !t); self.add_xor(w, false); } } } } let mut st = State { solver: Solver::default(), v: 30 * n as u32, }; for _ in 0..m { let a = scan!(usize); let b = scan!(usize; a); let y = scan!(u32); let b = b .into_iter() .map(|b_i| (b_i - 1) as u32) .collect::<Vec<_>>(); for d in 0..30 { let y = (y >> d) & 1 != 0; st.add_xor(b.iter().map(|&b_i| 30 * b_i + d).collect(), y); } } match st.solver.solve(None) { Status::Sat => { let mut x = vec![0u32; n]; for i in 0..n { for (d, &assign) in st.solver.models[30 * i..][..30].iter().enumerate() { x[i] |= match assign { LitBool::True => 1, LitBool::False => 0, LitBool::Undef => panic!(), } << d; } println!("{}", x[i]); } } Status::Unsat => { println!("-1"); } Status::Indeterminate => panic!(), } } #[allow(unreachable_code)] Ok(()) }