use std::time::Duration;
pub mod solver {
use std::{
collections::{HashMap, HashSet, VecDeque},
time::{Duration, Instant},
vec,
};
/// A boolean variable
pub type Var = usize;
/// A literal is either a variable or a negation of a variable.
/// (0, true) means x0 and (0, false) means ¬x0.
pub type Lit = (Var, bool);
#[derive(PartialEq, Debug)]
/// 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(Debug, Default)]
// A SAT Solver
pub struct Solver {
// the number of variables
n: usize,
// assignments for each variable
pub assigns: Vec<bool>,
// all clauses(original + learnt)
clauses: Vec<Vec<Lit>>,
// clauses that may be conflicted or propagated if a `lit` is false.
watchers: HashMap<Lit, Vec<usize>>,
// a clause index represents that a variable is forced to be assigned.
reason: Vec<Option<usize>>,
// decision level(0: unassigned, 1: minimum level)
level: Vec<usize>,
// assigned variables
que: VecDeque<Var>,
//the head index of `que` points unprocessed elements
head: usize,
}
impl Solver {
/// Enqueue a variable to assign a `value` to a boolean `assign`
fn enqueue(&mut self, var: Var, assign: bool, reason: Option<usize>) {
self.assigns[var] = assign;
self.reason[var] = reason;
self.level[var] = if let Some(last) = self.que.back() {
self.level[*last]
} else {
1
};
self.que.push_back(var);
}
// Create a new space for one variable.
pub fn new_var(&mut self) {
self.n += 1;
self.assigns.push(false);
self.reason.push(None);
self.level.push(0);
}
/// 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_unchecked(&mut self, clause: &[Lit]) {
assert!(clause.len() >= 2);
let clause_idx = self.clauses.len();
for &c in clause.iter() {
self.watchers.entry(c).or_insert(vec![]).push(clause_idx);
}
self.clauses.push(clause.to_vec());
}
/// 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]) {
if clause.len() == 1 {
self.enqueue(clause[0].0, clause[0].1, None);
return;
}
let clause_idx = self.clauses.len();
for &c in clause.iter() {
while c.0 >= self.assigns.len() {
self.new_var();
}
self.watchers.entry(c).or_insert(vec![]).push(clause_idx);
}
self.clauses.push(clause.to_vec());
}
/// 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<usize> {
while self.head < self.que.len() {
let p = {
let v = self.que[self.head];
self.head += 1;
(v, !self.assigns[v])
};
if let Some(watcher) = self.watchers.get(&p) {
'next_clause: for &cr in watcher.iter() {
let mut cnt = 0;
//let clause = &mut self.clauses[*cr];
let len = self.clauses[cr].len();
for c in 0..len {
let (v, sign) = self.clauses[cr][c];
if self.level[v] == 0 {
// this variable hasn't been decided yet
self.clauses[cr].swap(c, 0);
cnt += 1;
} else if self.assigns[v] == sign {
// this clause is already satisfied
self.clauses[cr].swap(c, 0);
continue 'next_clause;
}
}
if cnt == 0 {
return Some(cr);
} else if cnt == 1 {
// Unit clause
let (var, sign) = self.clauses[cr][0];
debug_assert!(self.level[var] == 0);
// NOTE
// I don't know how to handle this borrowing problem. Please help me.
// self.enqueue(var, sign, Some(cr));
self.assigns[var] = sign;
self.reason[var] = Some(cr);
self.level[var] = if let Some(last) = self.que.back() {
self.level[*last]
} else {
1
};
self.que.push_back(var);
}
}
}
}
None
}
/// Analyze a conflict clause and deduce a learnt clause to avoid a current conflict
fn analyze(&mut self, mut confl: usize) {
let mut que_tail = self.que.len() - 1;
let mut checked_vars = HashSet::new();
let current_level = self.level[self.que[que_tail]];
let mut learnt_clause = vec![];
let mut backtrack_level = 1;
let mut same_level_cnt = 0;
let mut skip = false;
loop {
for p in self.clauses[confl].iter() {
let (var, _) = *p;
if skip && var == self.que[que_tail] {
continue;
}
if self.level[var] == 0 {
continue;
}
// already checked
if !checked_vars.insert(var) {
continue;
}
debug_assert!(self.level[var] <= current_level);
if self.level[var] < current_level {
learnt_clause.push(*p);
backtrack_level = std::cmp::max(backtrack_level, self.level[var]);
} else {
same_level_cnt += 1;
}
}
// Find the latest a value that is checked
while !checked_vars.contains(&self.que[que_tail]) {
que_tail -= 1;
}
same_level_cnt -= 1;
// There is no variables that are at the conflict level
if same_level_cnt <= 0 {
break;
}
// Next
skip = true;
checked_vars.remove(&self.que[que_tail]);
debug_assert_eq!(self.level[self.que[que_tail]], current_level);
confl = self.reason[self.que[que_tail]].unwrap();
}
let p = self.que[que_tail];
learnt_clause.push((p, !self.assigns[p]));
if learnt_clause.len() == 1 {
backtrack_level = 1;
}
// Cancel decisions until the level is less than equal to the backtrack level
while let Some(p) = self.que.back() {
if self.level[*p] > backtrack_level {
self.level[*p] = 0;
self.que.pop_back();
} else {
break;
}
}
// propagate it by a new learnt clause
if learnt_clause.len() == 1 {
self.enqueue(p, !self.assigns[p], None);
self.head = self.que.len() - 1;
} else {
self.enqueue(p, !self.assigns[p], Some(self.clauses.len()));
self.head = self.que.len() - 1;
self.add_clause_unchecked(&learnt_clause);
}
}
/// 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,
que: VecDeque::new(),
head: 0,
clauses: Vec::new(),
reason: vec![None; n],
level: vec![0; n],
assigns: vec![false; n],
watchers: HashMap::new(),
};
for clause in clauses.iter() {
if clause.len() == 1 {
solver.enqueue(clause[0].0, clause[0].1, None);
} else {
solver.add_clause_unchecked(clause);
}
}
solver
}
/// Reserve the space of a clause database
/// # Arguments
/// * `cla_num` - The number of clause
pub fn reserve_clause(&mut self, cla_num: usize) {
self.clauses.reserve(cla_num);
}
// Reserve the space of variables
/// # Arguments
/// * `var_num` - The number of variable
pub fn reserve_variable(&mut self, var_num: usize) {
self.que.reserve(var_num);
self.clauses.reserve(var_num);
self.reason.reserve(var_num);
self.level.reserve(var_num);
self.assigns.reserve(var_num);
}
/// 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 {
let start = Instant::now();
loop {
if let Some(time_limit) = time_limit {
if start.elapsed() > time_limit {
// exceed the time limit
return Status::Indeterminate;
}
}
if let Some(confl) = self.propagate() {
//Conflict
let current_level = self.level[*self.que.back().unwrap()];
if current_level == 1 {
return Status::Unsat;
}
self.analyze(confl);
} else {
// No Conflict
// Select a decision variable that isn't decided yet
let mut p = None;
for v in 0..self.n {
if self.level[v] == 0 {
p = Some(v);
break;
}
}
if let Some(p) = p {
self.enqueue(p, self.assigns[p], None);
self.level[p] += 1;
} else {
// all variables are selected. which means that a formula is satisfied
return Status::Sat;
}
}
}
}
}
}
#[derive(Default)]
/// NOTE
/// declare variables to reduce the number of parameters for dp and dfs etc.
pub struct Solver {}
impl Solver {
pub fn solve(&mut self) {
let stdin = std::io::stdin();
let mut scn = fastio::Scanner::new(stdin.lock());
// let mut solver = screwsat::Solver::new(3, &vec![vec![(0, true), (1, false), (2, true)]]);
// let res = solver.solve(None);
// println!("{}", res);
let n: usize = scn.read();
let m: usize = scn.read();
if m == 0 {
println!("{}", n);
return;
}
let mut adjust = vec![vec![false; n]; n];
(0..m).for_each(|_| {
let a: usize = scn.read();
let b: usize = scn.read();
adjust[a - 1][b - 1] = true;
adjust[b - 1][a - 1] = true;
});
for k in 1..=n {
let mut clauses = vec![];
let mut color_clauses = vec![];
for i in 0..n {
let color_clause: Vec<_> = (0..k).map(|j| (k * i + j, true)).collect();
for j in 0..k {
for l in j + 1..k {
let mut a = color_clause[j];
a.1 = false;
let mut b = color_clause[l];
b.1 = false;
clauses.push(vec![a, b]);
}
}
//at least one color
color_clauses.push(color_clause.clone());
clauses.push(color_clause);
}
for i in 0..n {
for j in i + 1..n {
if !adjust[i][j] {
// not same color
for l in 0..k {
let mut p1 = color_clauses[i][l];
p1.1 = false;
let mut p2 = color_clauses[j][l];
p2.1 = false;
clauses.push(vec![p1, p2]);
}
}
}
}
let mut solver = solver::Solver::new(n * k + k, &clauses);
if solver::Status::Sat == solver.solve(Some(Duration::from_millis(300))) {
println!("{}", k);
return;
}
}
println!("{}", n);
}
}
pub mod fastio {
use std::collections::VecDeque;
use std::io::BufWriter;
use std::io::Write;
pub struct Writer<W: std::io::Write> {
writer: std::io::BufWriter<W>,
}
impl<W: std::io::Write> Writer<W> {
pub fn new(write: W) -> Writer<W> {
Writer {
writer: BufWriter::new(write),
}
}
pub fn flush(&mut self) {
self.writer.flush().unwrap();
}
pub fn write<S: std::string::ToString>(&mut self, s: S) {
self.writer.write(s.to_string().as_bytes()).unwrap();
}
pub fn writeln<S: std::string::ToString>(&mut self, s: S) {
self.write(s);
self.write('\n');
}
}
pub struct Scanner<R> {
stdin: R,
buffer: VecDeque<String>,
}
impl<R: std::io::BufRead> Scanner<R> {
pub fn new(s: R) -> Scanner<R> {
Scanner {
stdin: s,
buffer: VecDeque::new(),
}
}
pub fn read<T: std::str::FromStr>(&mut self) -> T {
while self.buffer.is_empty() {
let line = self.read_line();
for w in line.split_whitespace() {
self.buffer.push_back(String::from(w));
}
}
self.buffer.pop_front().unwrap().parse::<T>().ok().unwrap()
}
pub fn read_line(&mut self) -> String {
let mut line = String::new();
let _ = self.stdin.read_line(&mut line);
line
}
pub fn vec<T: std::str::FromStr>(&mut self, n: usize) -> Vec<T> {
(0..n).map(|_| self.read()).collect()
}
pub fn chars(&mut self) -> Vec<char> {
self.read::<String>().chars().collect()
}
}
}
fn main() {
std::thread::Builder::new()
.stack_size(64 * 1024 * 1024)
.spawn(|| {
let mut solver = Solver::default();
solver.solve()
})
.unwrap()
.join()
.unwrap();
}