mirror of
https://github.com/mii443/bg-sat.git
synced 2025-08-22 15:05:36 +00:00
optimize
This commit is contained in:
54
Cargo.lock
generated
54
Cargo.lock
generated
@ -5,3 +5,57 @@ version = 4
|
|||||||
[[package]]
|
[[package]]
|
||||||
name = "bg-sat"
|
name = "bg-sat"
|
||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
|
dependencies = [
|
||||||
|
"rayon",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "crossbeam-deque"
|
||||||
|
version = "0.8.6"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51"
|
||||||
|
dependencies = [
|
||||||
|
"crossbeam-epoch",
|
||||||
|
"crossbeam-utils",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "crossbeam-epoch"
|
||||||
|
version = "0.9.18"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e"
|
||||||
|
dependencies = [
|
||||||
|
"crossbeam-utils",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "crossbeam-utils"
|
||||||
|
version = "0.8.21"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "either"
|
||||||
|
version = "1.15.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "rayon"
|
||||||
|
version = "1.10.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "b418a60154510ca1a002a752ca9714984e21e4241e804d32555251faf8b78ffa"
|
||||||
|
dependencies = [
|
||||||
|
"either",
|
||||||
|
"rayon-core",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "rayon-core"
|
||||||
|
version = "1.12.1"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "1465873a3dfdaa8ae7cb14b4383657caab0b3e8a0aa9ae8e04b044854c8dfce2"
|
||||||
|
dependencies = [
|
||||||
|
"crossbeam-deque",
|
||||||
|
"crossbeam-utils",
|
||||||
|
]
|
||||||
|
@ -4,3 +4,4 @@ version = "0.1.0"
|
|||||||
edition = "2024"
|
edition = "2024"
|
||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
|
rayon = "1.10.0"
|
||||||
|
124
src/dimacs.rs
124
src/dimacs.rs
@ -1,4 +1,6 @@
|
|||||||
|
use rayon::prelude::*;
|
||||||
use std::collections::HashMap;
|
use std::collections::HashMap;
|
||||||
|
use std::sync::Mutex;
|
||||||
|
|
||||||
#[derive(Debug, Clone, PartialEq, Eq)]
|
#[derive(Debug, Clone, PartialEq, Eq)]
|
||||||
pub struct Variable {
|
pub struct Variable {
|
||||||
@ -7,10 +9,12 @@ pub struct Variable {
|
|||||||
}
|
}
|
||||||
|
|
||||||
impl Variable {
|
impl Variable {
|
||||||
|
#[inline]
|
||||||
pub fn positive(&self) -> i32 {
|
pub fn positive(&self) -> i32 {
|
||||||
self.id
|
self.id
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[inline]
|
||||||
pub fn negative(&self) -> i32 {
|
pub fn negative(&self) -> i32 {
|
||||||
-self.id
|
-self.id
|
||||||
}
|
}
|
||||||
@ -18,7 +22,7 @@ impl Variable {
|
|||||||
|
|
||||||
pub struct CnfBuilder {
|
pub struct CnfBuilder {
|
||||||
variables: HashMap<String, Variable>,
|
variables: HashMap<String, Variable>,
|
||||||
clauses: Vec<Vec<i32>>,
|
clauses: Mutex<Vec<Vec<i32>>>,
|
||||||
variable_counter: i32,
|
variable_counter: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -26,17 +30,17 @@ impl CnfBuilder {
|
|||||||
pub fn new() -> Self {
|
pub fn new() -> Self {
|
||||||
Self {
|
Self {
|
||||||
variables: HashMap::new(),
|
variables: HashMap::new(),
|
||||||
clauses: Vec::new(),
|
clauses: Mutex::new(Vec::new()),
|
||||||
variable_counter: 1,
|
variable_counter: 1,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn clause_count(&self) -> usize {
|
pub fn clause_count(&self) -> usize {
|
||||||
self.clauses.len()
|
self.clauses.lock().unwrap().len()
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn get_clauses(&self) -> &Vec<Vec<i32>> {
|
pub fn get_clauses(&self) -> Vec<Vec<i32>> {
|
||||||
&self.clauses
|
self.clauses.lock().unwrap().clone()
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn variable(&mut self, name: String) -> Variable {
|
pub fn variable(&mut self, name: String) -> Variable {
|
||||||
@ -60,7 +64,7 @@ impl CnfBuilder {
|
|||||||
}
|
}
|
||||||
|
|
||||||
pub fn clause(&mut self, literals: &[i32]) -> &mut Self {
|
pub fn clause(&mut self, literals: &[i32]) -> &mut Self {
|
||||||
self.clauses.push(literals.to_vec());
|
self.clauses.lock().unwrap().push(literals.to_vec());
|
||||||
self
|
self
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -76,10 +80,14 @@ impl CnfBuilder {
|
|||||||
|
|
||||||
pub fn at_most_k_true(&mut self, k: usize, vars: &[Variable]) -> &mut Self {
|
pub fn at_most_k_true(&mut self, k: usize, vars: &[Variable]) -> &mut Self {
|
||||||
if k + 1 <= vars.len() {
|
if k + 1 <= vars.len() {
|
||||||
for combo in combinations(vars, k + 1) {
|
let combinations = generate_combinations_optimized(vars, k + 1);
|
||||||
let clause: Vec<i32> = combo.iter().map(|v| v.negative()).collect();
|
|
||||||
self.clause(&clause);
|
let new_clauses: Vec<Vec<i32>> = combinations
|
||||||
}
|
.into_par_iter()
|
||||||
|
.map(|combo| combo.iter().map(|v| v.negative()).collect())
|
||||||
|
.collect();
|
||||||
|
|
||||||
|
self.clauses.lock().unwrap().extend(new_clauses);
|
||||||
}
|
}
|
||||||
|
|
||||||
self
|
self
|
||||||
@ -91,20 +99,30 @@ impl CnfBuilder {
|
|||||||
}
|
}
|
||||||
|
|
||||||
if k <= vars.len() {
|
if k <= vars.len() {
|
||||||
|
let mut all_new_clauses = Vec::new();
|
||||||
|
|
||||||
for i in 0..k {
|
for i in 0..k {
|
||||||
for combo in combinations(vars, i) {
|
let all_combinations = generate_combinations_optimized(vars, i);
|
||||||
let clause: Vec<i32> = combo.iter().map(|v| v.negative()).collect();
|
|
||||||
|
|
||||||
let rest: Vec<i32> = vars
|
let new_clauses: Vec<Vec<i32>> = all_combinations
|
||||||
.iter()
|
.into_par_iter()
|
||||||
.filter(|v| !combo.contains(v))
|
.map(|combo| {
|
||||||
.map(|v| v.positive())
|
let negated_combo: Vec<i32> = combo.iter().map(|v| v.negative()).collect();
|
||||||
.collect();
|
|
||||||
|
|
||||||
let clause: Vec<i32> = [clause, rest].concat();
|
let rest: Vec<i32> = vars
|
||||||
self.clause(&clause);
|
.iter()
|
||||||
}
|
.filter(|v| !combo.contains(v))
|
||||||
|
.map(|v| v.positive())
|
||||||
|
.collect();
|
||||||
|
|
||||||
|
[negated_combo, rest].concat()
|
||||||
|
})
|
||||||
|
.collect();
|
||||||
|
|
||||||
|
all_new_clauses.extend(new_clauses);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
self.clauses.lock().unwrap().extend(all_new_clauses);
|
||||||
} else {
|
} else {
|
||||||
self.clause(&[]);
|
self.clause(&[]);
|
||||||
}
|
}
|
||||||
@ -114,10 +132,11 @@ impl CnfBuilder {
|
|||||||
pub fn to_dimacs(&self) -> String {
|
pub fn to_dimacs(&self) -> String {
|
||||||
let mut result = String::new();
|
let mut result = String::new();
|
||||||
|
|
||||||
|
let clauses = self.clauses.lock().unwrap();
|
||||||
result.push_str(&format!(
|
result.push_str(&format!(
|
||||||
"p cnf {} {}\n",
|
"p cnf {} {}\n",
|
||||||
self.variable_counter - 1,
|
self.variable_counter - 1,
|
||||||
self.clauses.len()
|
clauses.len()
|
||||||
));
|
));
|
||||||
|
|
||||||
let mut sorted_vars = self.variables.values().cloned().collect::<Vec<_>>();
|
let mut sorted_vars = self.variables.values().cloned().collect::<Vec<_>>();
|
||||||
@ -127,7 +146,7 @@ impl CnfBuilder {
|
|||||||
result.push_str(&format!("c {}: {}\n", var.name, var.id));
|
result.push_str(&format!("c {}: {}\n", var.name, var.id));
|
||||||
}
|
}
|
||||||
|
|
||||||
for clause in &self.clauses {
|
for clause in &*clauses {
|
||||||
for &literal in clause {
|
for &literal in clause {
|
||||||
result.push_str(&format!("{} ", literal));
|
result.push_str(&format!("{} ", literal));
|
||||||
}
|
}
|
||||||
@ -136,9 +155,54 @@ impl CnfBuilder {
|
|||||||
|
|
||||||
result
|
result
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn add_clauses_batch(&mut self, clauses: Vec<Vec<i32>>) {
|
||||||
|
self.clauses.lock().unwrap().extend(clauses);
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn with_capacity(capacity: usize) -> Self {
|
||||||
|
Self {
|
||||||
|
variables: HashMap::new(),
|
||||||
|
clauses: Mutex::new(Vec::with_capacity(capacity)),
|
||||||
|
variable_counter: 1,
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn combinations<T: Clone>(items: &[T], k: usize) -> Vec<Vec<T>> {
|
fn generate_combinations_optimized<T: Clone + Send + Sync>(items: &[T], k: usize) -> Vec<Vec<T>> {
|
||||||
|
if k == 0 {
|
||||||
|
return vec![vec![]];
|
||||||
|
}
|
||||||
|
if items.is_empty() {
|
||||||
|
return vec![];
|
||||||
|
}
|
||||||
|
if k == 1 {
|
||||||
|
return items.iter().map(|item| vec![item.clone()]).collect();
|
||||||
|
}
|
||||||
|
|
||||||
|
if items.len() < 10 {
|
||||||
|
return combinations_sequential(items, k);
|
||||||
|
}
|
||||||
|
|
||||||
|
let first_element = items[0].clone();
|
||||||
|
let remaining = &items[1..];
|
||||||
|
|
||||||
|
let (mut with_first, without_first) = rayon::join(
|
||||||
|
|| {
|
||||||
|
let mut combos = generate_combinations_optimized(remaining, k - 1);
|
||||||
|
for combo in &mut combos {
|
||||||
|
combo.insert(0, first_element.clone());
|
||||||
|
}
|
||||||
|
combos
|
||||||
|
},
|
||||||
|
|| generate_combinations_optimized(remaining, k),
|
||||||
|
);
|
||||||
|
|
||||||
|
with_first.extend(without_first);
|
||||||
|
with_first
|
||||||
|
}
|
||||||
|
|
||||||
|
fn combinations_sequential<T: Clone>(items: &[T], k: usize) -> Vec<Vec<T>> {
|
||||||
if k == 0 {
|
if k == 0 {
|
||||||
return vec![vec![]];
|
return vec![vec![]];
|
||||||
}
|
}
|
||||||
@ -146,11 +210,15 @@ fn combinations<T: Clone>(items: &[T], k: usize) -> Vec<Vec<T>> {
|
|||||||
return vec![];
|
return vec![];
|
||||||
}
|
}
|
||||||
|
|
||||||
let mut result = combinations(&items[1..], k - 1);
|
let first_element = items[0].clone();
|
||||||
for combo in &mut result {
|
let remaining = &items[1..];
|
||||||
combo.insert(0, items[0].clone());
|
|
||||||
|
let mut with_first = combinations_sequential(remaining, k - 1);
|
||||||
|
for combo in &mut with_first {
|
||||||
|
combo.insert(0, first_element.clone());
|
||||||
}
|
}
|
||||||
|
|
||||||
result.extend(combinations(&items[1..], k));
|
let without_first = combinations_sequential(remaining, k);
|
||||||
result
|
|
||||||
|
[with_first, without_first].concat()
|
||||||
}
|
}
|
||||||
|
@ -3,7 +3,7 @@ pub mod dimacs;
|
|||||||
fn main() {
|
fn main() {
|
||||||
let mut cnf = dimacs::CnfBuilder::new();
|
let mut cnf = dimacs::CnfBuilder::new();
|
||||||
|
|
||||||
let vars = cnf.variables("x", 0..40);
|
let vars = cnf.variables("x", 0..7);
|
||||||
|
|
||||||
cnf.at_least_k_true(5, &vars);
|
cnf.at_least_k_true(5, &vars);
|
||||||
cnf.at_most_k_true(5, &vars);
|
cnf.at_most_k_true(5, &vars);
|
||||||
|
Reference in New Issue
Block a user