結果
問題 | No.1421 国勢調査 (Hard) |
ユーザー | togatoga |
提出日時 | 2021-03-09 13:16:14 |
言語 | Rust (1.83.0 + proconio) |
結果 |
WA
|
実行時間 | - |
コード長 | 64,009 bytes |
コンパイル時間 | 17,491 ms |
コンパイル使用メモリ | 379,044 KB |
実行使用メモリ | 813,080 KB |
最終ジャッジ日時 | 2024-10-11 03:16:19 |
合計ジャッジ時間 | 42,813 ms |
ジャッジサーバーID (参考情報) |
judge3 / judge5 |
(要ログイン)
ファイルパターン | 結果 |
---|---|
sample | AC * 2 |
other | AC * 14 MLE * 1 WA * 6 |
コンパイルメッセージ
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>>whereT: FromStr,{Ok(self.next()?.parse())}pub fn parse_next_n<T>(&mut self, n: usize) -> io::Result<Result<Vec<T>, T::Err>>whereT: 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>>whereF: 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>>>whereF: 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 variableassigns: 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 solvespub 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 variablespub 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 conflictfn 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 clausepub fn reserve_clause(&mut self, cla_num: usize) {self.db.clauses.reserve(cla_num);}/// # Arguments/// * `var_num` - The number of variablepub 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<()>whereR: 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(Some(Duration::from_millis(1500))) {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]);}},_ => {println!("-1");}}}#[allow(unreachable_code)]Ok(())}