Updated the 01-27 and 02-03 sessions

Author: k-sidorov

_bibliography/s20250203.bib

@@ -0,0 +1,18 @@
+@InProceedings{10.1007/978-3-319-59776-8_1,
+author="Chihani, Zakaria
+and Marre, Bruno
+and Bobot, Fran{\c{c}}ois
+and Bardin, S{\'e}bastien",
+editor="Salvagnin, Domenico
+and Lombardi, Michele",
+title="Sharpening Constraint Programming Approaches for Bit-Vector Theory",
+booktitle="Integration of AI and OR Techniques in Constraint Programming",
+year="2017",
+publisher="Springer International Publishing",
+address="Cham",
+pages="3--20",
+abstract="We address the challenge of developing efficient Constraint Programming-based approaches for solving formulas over the quantifier-free fragment of the theory of bitvectors (BV), which is of paramount importance in software verification. We propose CP(BV), a highly efficient BV resolution technique built on carefully chosen anterior results sharpened with key original features such as thorough domain combination or dedicated labeling. Extensive experimental evaluations demonstrate that CP(BV) is much more efficient than previous similar attempts from the CP community, that it is indeed able to solve the majority of the standard verification benchmarks for bitvectors, and that it already complements the standard SMT approaches on several crucial (and industry-relevant) aspects, notably in terms of scalability w.r.t. bit-width, theory combination or intricate mix of non-linear arithmetic and bitwise operators. This work paves the way toward building competitive CP-based verification-oriented solvers.",
+isbn="978-3-319-59776-8",
+html="https://link.springer.com/chapter/10.1007/978-3-319-59776-8_1"
+}
+

_sessions/2025-01-27-teeth-scheduling.md

@@ -0,0 +1,13 @@
+---
+layout: session
+title: A Hybrid Approach for the Artificial Teeth Scheduling Problem
+host: Felix Winter
+session_type: research
+---
+
+Modern-day artificial tooth manufacturing relies on a highly automated production process that utilizes complex machine environments. The large-scale requirements in this area thus require automated scheduling methods that can efficiently minimize a multi-objective cost function while considering many complex constraints.
+
+We propose a novel approach to the ATSP that hybridizes exact and heuristic approaches in an innovative two-stage solution process. The first phase utilizes a novel subproblem formulation to efficiently batch product demands into compact jobs using exact solution methods based on constraint programming and column generation. In the second phase, the sequence of the resulting batch jobs is optimized using local search-based metaheuristics and hyper-heuristics.
+ 
+
+Experimental results show that the proposed method can successfully hybridize the strengths of the exact and heuristic methods to efficiently solve all benchmark instances. The objective costs of almost all instances are significantly improved compared with existing approaches, and we provide new upper bounds for all evaluated real-life instances.

_sessions/2025-02-03-bitvector-cp.md

@@ -0,0 +1,10 @@
+---
+layout: session
+title: Sharpening Constraint Programming Approaches for Bit-Vector Theory
+host: Maarten Flippo
+host_ref: https://maartenflippo.com
+session_type: paper
+related_papers: s20250103
+---
+
+We address the challenge of developing efficient Constraint Programming-based approaches for solving formulas over the quantifier-free fragment of the theory of bitvectors (BV), which is of paramount importance in software verification. We propose CP(BV), a highly efficient BV resolution technique built on carefully chosen anterior results sharpened with key original features such as thorough domain combination or dedicated labeling. Extensive experimental evaluations demonstrate that CP(BV) is much more efficient than previous similar attempts from the CP community, that it is indeed able to solve the majority of the standard verification benchmarks for bitvectors, and that it already complements the standard SMT approaches on several crucial (and industry-relevant) aspects, notably in terms of scalability w.r.t. bit-width, theory combination or intricate mix of non-linear arithmetic and bitwise operators. This work paves the way toward building competitive CP-based verification-oriented solvers.