mirror of
https://github.com/mii443/bg-sat.git
synced 2025-12-03 02:58:23 +00:00
number compare game
This commit is contained in:
mii443
5775
num_comp_base.cnf
Normal file
5775
num_comp_base.cnf
Normal file
File diff suppressed because it is too large
Load Diff
5413
num_comp_base.txt
Normal file
5413
num_comp_base.txt
Normal file
File diff suppressed because it is too large
Load Diff
@@ -74,6 +74,18 @@ impl CnfBuilder {
|
||||
self
|
||||
}
|
||||
|
||||
pub fn implies(&mut self, a: &Variable, b: &Variable) -> &mut Self {
|
||||
self.clause(&[a.negative(), b.positive()])
|
||||
}
|
||||
|
||||
pub fn negative_implies(&mut self, a: &Variable, b: &Variable) -> &mut Self {
|
||||
self.clause(&[a.positive(), b.negative()])
|
||||
}
|
||||
|
||||
pub fn right_negative_implies(&mut self, a: &Variable, b: &Variable) -> &mut Self {
|
||||
self.clause(&[a.negative(), b.negative()])
|
||||
}
|
||||
|
||||
pub fn exactly_k_true(&mut self, k: usize, vars: &[Variable]) -> &mut Self {
|
||||
self.at_least_k_true(k, vars);
|
||||
self.at_most_k_true(k, vars);
|
||||
@@ -99,6 +111,34 @@ impl CnfBuilder {
|
||||
self
|
||||
}
|
||||
|
||||
pub fn at_most_k_true_with_two_implies(
|
||||
&mut self,
|
||||
k: usize,
|
||||
vars: &[Variable],
|
||||
implies: &[i32],
|
||||
) -> &mut Self {
|
||||
if k + 1 <= vars.len() {
|
||||
let combinations = generate_combinations_optimized(vars, k + 1);
|
||||
|
||||
let new_clauses: Vec<Vec<i32>> = combinations
|
||||
.into_par_iter()
|
||||
.map(|combo| {
|
||||
let mut n: Vec<i32> = combo.iter().map(|v| v.negative()).collect();
|
||||
if !n.is_empty() {
|
||||
for imply in implies {
|
||||
n.push(-imply);
|
||||
}
|
||||
}
|
||||
n
|
||||
})
|
||||
.collect();
|
||||
|
||||
self.clauses.lock().unwrap().extend(new_clauses);
|
||||
}
|
||||
|
||||
self
|
||||
}
|
||||
|
||||
pub fn at_least_k_true(&mut self, k: usize, vars: &[Variable]) -> &mut Self {
|
||||
if k == 0 {
|
||||
return self;
|
||||
@@ -162,6 +202,38 @@ impl CnfBuilder {
|
||||
result
|
||||
}
|
||||
|
||||
pub fn to_human_readable(&self) -> String {
|
||||
let mut result = String::new();
|
||||
let var_names: HashMap<i32, String> = self
|
||||
.variables
|
||||
.iter()
|
||||
.map(|(name, var)| (var.id, name.clone()))
|
||||
.collect();
|
||||
|
||||
let clauses = self.clauses.lock().unwrap();
|
||||
for clause in &*clauses {
|
||||
let clause_str: Vec<String> = clause
|
||||
.iter()
|
||||
.map(|&lit| {
|
||||
let var_id = lit.abs();
|
||||
let var_name = var_names.get(&var_id).unwrap();
|
||||
if lit > 0 {
|
||||
var_name.clone()
|
||||
} else {
|
||||
format!("¬{}", var_name)
|
||||
}
|
||||
})
|
||||
.collect();
|
||||
result.push_str(&format!("({}) ∧\n", clause_str.join(" ∨ ")));
|
||||
}
|
||||
|
||||
if result.ends_with(" ∧\n") {
|
||||
result.truncate(result.len() - " ∧\n".len());
|
||||
}
|
||||
|
||||
result
|
||||
}
|
||||
|
||||
pub fn add_clauses_batch(&mut self, clauses: Vec<Vec<i32>>) {
|
||||
self.clauses.lock().unwrap().extend(clauses);
|
||||
}
|
||||
|
||||
@@ -2,6 +2,6 @@ pub mod dimacs;
|
||||
pub mod num_comp;
|
||||
fn main() {
|
||||
let num_comp = num_comp::NumComp::new();
|
||||
let dimacs = num_comp.generate_base_dimacs();
|
||||
println!("{}", dimacs);
|
||||
let cnf = num_comp.generate_base_dimacs();
|
||||
println!("{}", cnf.to_dimacs());
|
||||
}
|
||||
|
||||
168
src/num_comp.rs
168
src/num_comp.rs
@@ -1,5 +1,7 @@
|
||||
use crate::dimacs::{self, CnfBuilder, Variable};
|
||||
|
||||
static CARDS: i32 = 9;
|
||||
|
||||
pub struct NumComp {}
|
||||
|
||||
impl NumComp {
|
||||
@@ -11,52 +13,172 @@ impl NumComp {
|
||||
todo!()
|
||||
}
|
||||
|
||||
pub fn generate_base_dimacs(&self) -> String {
|
||||
pub fn generate_base_dimacs(&self) -> CnfBuilder {
|
||||
let mut cnf = dimacs::CnfBuilder::new();
|
||||
|
||||
// カード情報
|
||||
let self_cards = cnf.variables("self_card", 0..9);
|
||||
let opponent_cards = cnf.variables("opponent_card", 0..9);
|
||||
let self_cards_per_round: Vec<Vec<Variable>> = (0..CARDS)
|
||||
.into_iter()
|
||||
.map(|r| cnf.variables(&format!("self_card_{}_", r), 0..CARDS))
|
||||
.collect();
|
||||
|
||||
// ラウンドの情報
|
||||
let round_info = cnf.variables("round_info", 0..9 * 9);
|
||||
let opponent_cards_per_round: Vec<Vec<Variable>> = (0..CARDS)
|
||||
.into_iter()
|
||||
.map(|r| cnf.variables(&format!("opponent_card_{}_", r), 0..CARDS))
|
||||
.collect();
|
||||
|
||||
// 相手のラウンドの情報
|
||||
let opponent_round_info = cnf.variables("opponent_round_info", 0..9);
|
||||
let round_info: Vec<Vec<Variable>> = (0..CARDS)
|
||||
.into_iter()
|
||||
.map(|r| cnf.variables(&format!("round_info_{}_", r), 0..CARDS))
|
||||
.collect();
|
||||
|
||||
// ラウンドの勝敗
|
||||
let round_win = cnf.variables("round_win", 0..9);
|
||||
let round_lose = cnf.variables("round_lose", 0..9);
|
||||
let round_draw = cnf.variables("round_draw", 0..9);
|
||||
let opponent_round_info = cnf.variables("opponent_round_info", 0..CARDS);
|
||||
|
||||
// 各ラウンド
|
||||
for round in 0..9 {
|
||||
/* nを出し、引き分けの場合、相手は対応したカードを出し、相手はカードnを持っていない */
|
||||
for card in 0..9 {
|
||||
let round_win = cnf.variables("round_win", 0..CARDS);
|
||||
let round_lose = cnf.variables("round_lose", 0..CARDS);
|
||||
let round_draw = cnf.variables("round_draw", 0..CARDS);
|
||||
|
||||
for round in 0..CARDS as usize {
|
||||
for card in 0..CARDS as usize {
|
||||
if (card % 2) == 0 {
|
||||
Self::gen_dimacs_a_and_b_implies_c_and_not_d(
|
||||
&mut cnf,
|
||||
&round_info[round * 9 + card],
|
||||
&round_info[round][card],
|
||||
&round_draw[round],
|
||||
&opponent_round_info[round],
|
||||
&opponent_cards[card],
|
||||
&opponent_cards_per_round[round][card],
|
||||
);
|
||||
} else {
|
||||
Self::gen_dimacs_a_and_b_implies_not_c_and_not_d(
|
||||
&mut cnf,
|
||||
&round_info[round * 9 + card],
|
||||
&round_info[round][card],
|
||||
&round_draw[round],
|
||||
&opponent_round_info[round],
|
||||
&opponent_cards[card],
|
||||
&opponent_cards_per_round[round][card],
|
||||
);
|
||||
}
|
||||
|
||||
cnf.right_negative_implies(
|
||||
&round_info[round][card],
|
||||
&self_cards_per_round[round][card],
|
||||
);
|
||||
|
||||
if round != 0 {
|
||||
cnf.negative_implies(
|
||||
&self_cards_per_round[round - 1][card],
|
||||
&self_cards_per_round[round][card],
|
||||
);
|
||||
cnf.negative_implies(
|
||||
&opponent_cards_per_round[round - 1][card],
|
||||
&opponent_cards_per_round[round][card],
|
||||
);
|
||||
|
||||
let opponent_cards =
|
||||
Self::get_cards_under_k(&opponent_cards_per_round[round], card + 1, true);
|
||||
if !opponent_cards.is_empty() {
|
||||
cnf.at_most_k_true_with_two_implies(
|
||||
opponent_cards.len() - 1,
|
||||
&opponent_cards,
|
||||
&[
|
||||
round_info[round][card].positive(),
|
||||
round_win[round].positive(),
|
||||
opponent_round_info[round].positive(),
|
||||
],
|
||||
);
|
||||
}
|
||||
|
||||
let opponent_cards =
|
||||
Self::get_cards_under_k(&opponent_cards_per_round[round], card + 1, false);
|
||||
if !opponent_cards.is_empty() {
|
||||
cnf.at_most_k_true_with_two_implies(
|
||||
opponent_cards.len() - 1,
|
||||
&opponent_cards,
|
||||
&[
|
||||
round_info[round][card].positive(),
|
||||
round_win[round].positive(),
|
||||
opponent_round_info[round].negative(),
|
||||
],
|
||||
);
|
||||
}
|
||||
|
||||
let opponent_cards =
|
||||
Self::get_cards_over_k(&opponent_cards_per_round[round], card + 1, true);
|
||||
if !opponent_cards.is_empty() {
|
||||
cnf.at_most_k_true_with_two_implies(
|
||||
opponent_cards.len() - 1,
|
||||
&opponent_cards,
|
||||
&[
|
||||
round_info[round][card].negative(),
|
||||
round_lose[round].positive(),
|
||||
opponent_round_info[round].positive(),
|
||||
],
|
||||
);
|
||||
}
|
||||
|
||||
let opponent_cards =
|
||||
Self::get_cards_over_k(&opponent_cards_per_round[round], card + 1, false);
|
||||
if !opponent_cards.is_empty() {
|
||||
cnf.at_most_k_true_with_two_implies(
|
||||
opponent_cards.len() - 1,
|
||||
&opponent_cards,
|
||||
&[
|
||||
round_info[round][card].negative(),
|
||||
round_lose[round].positive(),
|
||||
opponent_round_info[round].negative(),
|
||||
],
|
||||
);
|
||||
}
|
||||
|
||||
if card == 0 {
|
||||
// (round_info[round][card] and round_win[round] and opponent_round_info[round]) -> opponent_cards_per_round[round][8]
|
||||
cnf.clause(&[
|
||||
round_info[round][card].negative(),
|
||||
round_win[round].negative(),
|
||||
opponent_round_info[round].negative(),
|
||||
opponent_cards_per_round[round][8].positive(),
|
||||
]);
|
||||
}
|
||||
|
||||
if card == 8 {
|
||||
// (round_info[round][card] and round_lose[round] and opponent_round_info[round]) -> opponent_cards_per_round[round][0]
|
||||
cnf.clause(&[
|
||||
round_info[round][card].negative(),
|
||||
round_lose[round].negative(),
|
||||
opponent_round_info[round].negative(),
|
||||
opponent_cards_per_round[round][0].positive(),
|
||||
]);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
cnf.clause(&[round_draw[0].positive()]);
|
||||
cnf.clause(&[round_info[0].positive()]);
|
||||
cnf.exactly_k_true(
|
||||
(CARDS - 1 - round as i32) as usize,
|
||||
&opponent_cards_per_round[round],
|
||||
);
|
||||
cnf.exactly_k_true(
|
||||
(CARDS - 1 - round as i32) as usize,
|
||||
&self_cards_per_round[round],
|
||||
);
|
||||
}
|
||||
|
||||
cnf.to_dimacs()
|
||||
cnf
|
||||
}
|
||||
|
||||
fn get_cards_under_k(cards: &[Variable], k: usize, is_odd: bool) -> Vec<Variable> {
|
||||
cards
|
||||
.iter()
|
||||
.enumerate()
|
||||
.filter(|(i, _)| (i + 1) < k && ((i % 2 != 0) ^ is_odd))
|
||||
.map(|(_, v)| v.clone())
|
||||
.collect()
|
||||
}
|
||||
|
||||
fn get_cards_over_k(cards: &[Variable], k: usize, is_odd: bool) -> Vec<Variable> {
|
||||
cards
|
||||
.iter()
|
||||
.enumerate()
|
||||
.filter(|(i, _)| (i + 1) > k && ((i % 2 != 0) ^ is_odd))
|
||||
.map(|(_, v)| v.clone())
|
||||
.collect()
|
||||
}
|
||||
|
||||
fn gen_dimacs_a_and_b_implies_c_and_not_d(
|
||||
|
||||
Reference in New Issue
Block a user