pith. sign in

arxiv: 2606.06641 · v1 · pith:CPYV3NYRnew · submitted 2026-06-04 · 💻 cs.AI · cs.LO

Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver

Cody J Christopher , Charles Gretton This is my paper

Pith reviewed 2026-06-28 00:51 UTC · model grok-4.3

classification 💻 cs.AI cs.LO
keywords pseudo-Boolean SATGPU accelerationcontinuous local searchdiscrete Fourier transformJAXsymmetric constraintssatisfiability solver
0
0 comments X

The pith

AFSAT turns a proof-of-concept Fourier method into a working GPU solver for any mix of symmetric pseudo-Boolean constraints.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to engineer a continuous local search solver that runs on GPUs and accepts arbitrary combinations of symmetric constraint types and lengths in one instance. It starts from an earlier FastFourierSAT sketch and adds compact representations, a custom discrete Fourier transform, and JAX compilation to fix stability and speed problems. A sympathetic reader would expect this to let accelerator hardware tackle larger and more varied satisfiability instances without manual reformulation. The work focuses on practical throughput gains rather than new theoretical bounds.

Core claim

AFSAT realises the FastFourierSAT proof-of-concept as a complete solver that supports heterogeneous mixtures of symmetric constraints, delivers better numerical stability and memory use through a tailored discrete Fourier transform and compact data layouts, and obtains near-linear scaling across multiple accelerators by means of JAX array sharding and automatic parallelisation.

What carries the argument

Tailored discrete Fourier transform inside JAX-compiled continuous local search, which evaluates symmetric constraints in batches of candidate assignments while mitigating floating-point error.

If this is right

  • Problems no longer need to be split or padded to uniform constraint length before search begins.
  • Throughput grows nearly linearly when extra GPUs are added via array sharding.
  • Floating-point search remains stable enough for practical use without extra precision tricks.
  • Memory traffic drops because compact representations replace full matrix storage.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same JAX pipeline could be reused for other continuous relaxations of discrete constraint problems.
  • Hybrid workflows might combine AFSAT with learned heuristics that propose initial batches of assignments.
  • Benchmark suites that deliberately mix short and long symmetric clauses would become necessary to measure real-world gains.

Load-bearing premise

A custom Fourier transform plus JAX features can overcome floating-point and memory limits well enough to give reliable gains on arbitrary mixes of constraint lengths and types.

What would settle it

Run AFSAT on a collection of heterogeneous pseudo-Boolean instances and check whether solution quality or reported runtimes degrade sharply compared with a standard discrete solver on the same set.

read the original abstract

We present Accelerated Fourier SAT (AFSAT), a GPU-accelerated solver for pseudo-Boolean satisfiability based on continuous local search (CLS). AFSAT realises the proof-of-concept approach, FastFourierSAT, into a fully-engineered solver supporting any heterogeneous mixture of symmetric constraint types and lengths within a single problem instance. Using the JAX compiler, AFSAT leverages pure function composition, automatic vectorisation, automatic differentiation, and just-in-time (JIT) compilation to perform massively parallel CLS across batches of candidate assignments. We demonstrate substantially improved numerical stability, runtime performance, and memory efficiency over the proof-of-concept. We achieve this by way of identifying and addressing various limitations that arise from memory latency and floating-point representation, as well as leveraging automatic parallelisation and compact representations. The inherent representational and stability limitations of floating point are partially addressed by a tailored discrete Fourier transform implementation. We achieve near-linear throughput when scaling to multiple accelerators via JAX array sharding.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents Accelerated Fourier SAT (AFSAT), a JAX-based GPU-accelerated solver realizing the FastFourierSAT proof-of-concept for symmetric pseudo-Boolean SAT via continuous local search. It supports arbitrary heterogeneous mixtures of symmetric constraint types and lengths in a single instance, using pure function composition, automatic vectorization, differentiation, and JIT compilation for massively parallel search, with a tailored discrete Fourier transform to address floating-point issues, compact representations for memory efficiency, and JAX sharding for near-linear multi-accelerator scaling. The manuscript claims substantially improved numerical stability, runtime performance, and memory efficiency over the proof-of-concept.

Significance. If the claimed engineering advances and performance gains are substantiated, AFSAT would constitute a meaningful practical contribution to GPU-accelerated continuous local search SAT solvers, extending the applicability of Fourier-based methods to heterogeneous constraint sets and larger-scale problems on modern accelerator hardware.

major comments (2)
  1. Abstract: The central claims of 'substantially improved numerical stability, runtime performance, and memory efficiency' together with 'near-linear throughput when scaling to multiple accelerators' are asserted without any quantitative benchmarks, runtime tables, scaling plots, error metrics, or direct comparisons to FastFourierSAT or baseline solvers, rendering the primary engineering contribution unevaluable from the manuscript.
  2. Abstract (and implied implementation description): The statement that 'a tailored discrete Fourier transform implementation' partially addresses 'representational and stability limitations of floating point' provides no concrete description of the modifications, no analysis of numerical error before/after, and no evidence that the approach suffices for arbitrary heterogeneous constraint mixtures, leaving the weakest assumption untested.
minor comments (1)
  1. The manuscript would benefit from an explicit Experiments or Evaluation section containing the benchmarks referenced in the abstract.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We appreciate the referee's detailed feedback on our manuscript. We address each major comment below and indicate the revisions we will make to strengthen the paper.

read point-by-point responses

  1. Referee: Abstract: The central claims of 'substantially improved numerical stability, runtime performance, and memory efficiency' together with 'near-linear throughput when scaling to multiple accelerators' are asserted without any quantitative benchmarks, runtime tables, scaling plots, error metrics, or direct comparisons to FastFourierSAT or baseline solvers, rendering the primary engineering contribution unevaluable from the manuscript.

    Authors: The full manuscript includes comprehensive experimental evaluations with benchmarks, tables, plots, error metrics, and comparisons in the results section. However, we acknowledge that the abstract presents the claims at a high level without specific numbers. We will revise the abstract to incorporate key quantitative results, such as performance improvements and scaling factors, to make the contributions more immediately evaluable. revision: yes

  2. Referee: Abstract (and implied implementation description): The statement that 'a tailored discrete Fourier transform implementation' partially addresses 'representational and stability limitations of floating point' provides no concrete description of the modifications, no analysis of numerical error before/after, and no evidence that the approach suffices for arbitrary heterogeneous constraint mixtures, leaving the weakest assumption untested.

    Authors: The tailored DFT is detailed in the implementation and methods sections of the manuscript, with analysis of numerical stability and support for heterogeneous constraints demonstrated through experiments. To address the concern about the abstract, we will add a brief description of the DFT modifications and reference the supporting analysis and evidence from the experiments on heterogeneous instances. revision: partial

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper describes an engineering implementation of the prior FastFourierSAT proof-of-concept, using JAX primitives for vectorization, JIT, sharding, and a tailored DFT to address floating-point and memory issues in CLS for heterogeneous symmetric pseudo-Boolean constraints. Performance and stability claims are grounded in concrete implementation choices and empirical measurements rather than any equation that reduces to its own inputs, fitted parameters renamed as predictions, or load-bearing self-citations. The derivation chain consists of standard compiler and library features applied to an existing continuous-search formulation; no self-definitional, ansatz-smuggling, or renaming steps are present.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on the domain assumption that continuous local search via Fourier methods is viable for pseudo-Boolean SAT and that JAX reliably delivers the required automatic parallelisation and compilation; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption Continuous local search implemented via Fourier transforms can solve pseudo-Boolean SAT problems
    Central premise inherited from the FastFourierSAT proof-of-concept.
  • domain assumption JAX compiler features (vectorisation, automatic differentiation, JIT) enable massively parallel CLS on GPUs
    Invoked to justify the performance and scalability claims.

pith-pipeline@v0.9.1-grok · 5702 in / 1403 out tokens · 47593 ms · 2026-06-28T00:51:12.450473+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

134 extracted references · 23 canonical work pages

  1. [1]

    2025 , eprint=

    Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization , author=. 2025 , eprint=

    2025

  2. [2]

    Figueredo, A. J. and Wolf, P. S. A. , title =. Human Nature , volume =

  3. [3]

    Analysis of Boolean Functions , publisher=

    O'Donnell, Ryan , year=. Analysis of Boolean Functions , publisher=

  4. [4]

    Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    Massively parallel continuous local search for hybrid SAT solving on GPUs , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

  5. [5]

    arXiv preprint arXiv:2105.15183 , year=

    Efficient and Modular Implicit Differentiation , author=. arXiv preprint arXiv:2105.15183 , year=

    arXiv

  6. [6]

    arXiv:2402.09983 , year=

    Optimistix: modular optimisation in JAX and Equinox , author=. arXiv:2402.09983 , year=

    arXiv

  7. [7]

    PyTorch 2: Faster Machine Learning Through Dynamic Python Bytecode Transformation and Graph Compilation

    Pytorch 2: Faster machine learning through dynamic python bytecode transformation and graph compilation , author=. Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 , pages=. doi:10.1145/3620665.3640366 , url=

    work page doi:10.1145/3620665.3640366

  8. [8]

    and Haberland, Matt and Reddy, Tyler and Cournapeau, David and Burovski, Evgeni and Peterson, Pearu and Weckesser, Warren and Bright, Jonathan and

    Virtanen, Pauli and Gommers, Ralf and Oliphant, Travis E. and Haberland, Matt and Reddy, Tyler and Cournapeau, David and Burovski, Evgeni and Peterson, Pearu and Weckesser, Warren and Bright, Jonathan and. Nature Methods , year =

  9. [9]

    DeepMind and Babuschkin, Igor and Baumli, Kate and Bell, Alison and Bhupatiraju, Surya and Bruce, Jake and Buchlovsky, Peter and Budden, David and Cai, Trevor and Clark, Aidan and Danihelka, Ivo and Dedieu, Antoine and Fantacci, Claudio and Godwin, Jonathan and Jones, Chris and Hemsley, Ross and Hennigan, Tom and Hessel, Matteo and Hou, Shaobo and Kapturo...

  10. [10]

    Artificial Intelligence , volume=

    Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions , author=. Artificial Intelligence , volume=. 2021 , publisher=

    2021

  11. [11]

    International conference on principles and practice of constraint programming , pages=

    Towards an optimal CNF encoding of boolean cardinality constraints , author=. International conference on principles and practice of constraint programming , pages=. 2005 , organization=

    2005

  12. [12]

    International conference on principles and practice of constraint programming , pages=

    Efficient CNF encoding of boolean cardinality constraints , author=. International conference on principles and practice of constraint programming , pages=. 2003 , organization=

    2003

  13. [13]

    Information Processing Letters , volume=

    A linear-time transformation of linear inequalities into conjunctive normal form , author=. Information Processing Letters , volume=. 1998 , publisher=

    1998

  14. [14]

    and Stuckey, Peter J

    Bierlee, Hendrik and Dekker, Jip J. and Stuckey, Peter J. Revisiting Pseudo-Boolean Encodings from an Integer Perspective. Integration of Constraint Programming, Artificial Intelligence, and Operations Research. 2025

    2025

  15. [15]

    Impagliazzo, Russell and Paturi, Ramamohan , title =. J. Comput. Syst. Sci. , month = mar, pages =. 2001 , issue_date =. doi:10.1006/jcss.2000.1727 , abstract =

    work page doi:10.1006/jcss.2000.1727 2001

  16. [16]

    Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers , year =

    Elffers, Jan and Gir\'. Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers , year =. Theory and Applications of Satisfiability Testing – SAT 2018: 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018, Proceedings , pages =. doi:10.1007/978-3-319-9...

    work page doi:10.1007/978-3-319-94144-8_5 2018

  17. [17]

    2024 , url =

    Suresh Bolusani and Mathieu Besan. 2024 , url =

    2024

  18. [18]

    Journal on Satisfiability, Boolean Modeling and Computation , volume =

    Le Berre, Daniel and Parrain, Anne , title =. Journal on Satisfiability, Boolean Modeling and Computation , volume =. 2010 , pages =

    2010

  19. [19]

    2024 , number =

    Suresh Bolusani and Mathieu Besan. 2024 , number =

    2024

  20. [20]

    INFORMS J

    Shinano, Yuji and Heinz, Stefan and Vigerske, Stefan and Winkler, Michael , title =. INFORMS J. on Computing , month = feb, pages =. 2018 , issue_date =

    2018

  21. [21]

    ArXiv , year=

    401 and beyond: improved bounds and algorithms for the Ramsey algebra search , author=. ArXiv , year=

  22. [22]

    Algebra Universalis , year =

    Tomasz Kowalski , title =. Algebra Universalis , year =. doi:10.1007/s00012-015-0353-0 , issn =

    work page doi:10.1007/s00012-015-0353-0

  23. [23]

    Alm and David A

    Jeremy F. Alm and David A. Andrews , title =. Algebra Universalis , year =. doi:10.1007/s00012-019-0592-6 , issn =

    work page doi:10.1007/s00012-019-0592-6

  24. [24]

    In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving , year =

    Vinyals, Marc and Elffers, Jan and Gir\'. In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving , year =. Theory and Applications of Satisfiability Testing – SAT 2018: 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018, Proceedings , pa...

    work page doi:10.1007/978-3-319-94144-8_18 2018

  25. [25]

    1987 , issn =

    On the complexity of cutting-plane proofs , journal =. 1987 , issn =. doi:10.1016/0166-218X(87)90039-4 , author =

    work page doi:10.1016/0166-218x(87)90039-4 1987

  26. [26]

    Urquhart, Alasdair , title =. J. ACM , month = jan, pages =. 1987 , issue_date =. doi:10.1145/7531.8928 , abstract =

    work page doi:10.1145/7531.8928 1987

  27. [27]

    , title =

    Cook, Stephen A. , title =. Proceedings of the Third Annual ACM Symposium on Theory of Computing , pages =. 1971 , isbn =. doi:10.1145/800157.805047 , abstract =

    work page doi:10.1145/800157.805047 1971

  28. [28]

    , title =

    Cook, Stephen A. , title =. Proceedings of the Third Annual ACM Symposium on Theory of Computing , location =. 1971 , publisher =

    1971

  29. [29]

    1995 , publisher=

    A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization , author=. 1995 , publisher=

    1995

  30. [30]

    , booktitle =

    Karp, R. , booktitle =

  31. [31]

    2012 , keywords =

    Youssef Hamadi and Christoph Wintersteiger , title =. 2012 , keywords =

    2012

  32. [32]

    A Tree Decomposition Based Approach to Solve Structured SAT Instances

    Habet, Djamal and Paris, Lionel and Terrioux, Cyril , biburl =. A Tree Decomposition Based Approach to Solve Structured SAT Instances. , url =. ICTAI , ee =

  33. [33]

    Electron

    Eyal Amir and Sheila Mcllraith , title =. Electron. Notes Discret. Math. , volume =. 2001 , doi =

    2001

  34. [34]

    Wintersteiger , title =

    Youssef Hamadi and Christoph M. Wintersteiger , title =. 2013 , doi =

    2013

  35. [35]

    Marijn J. H. Heule and Oliver Kullmann and Siert Wieringa and Armin Biere , title =. Haifa Verification Conference 2011 , year =

    2011

  36. [36]

    Heule and Hans van Maaren , title =

    Marijn J.H. Heule and Hans van Maaren , title =. 2009 , month =

    2009

  37. [37]

    JaCk-SAT:

    Daniel Singer and Anthony Monnet , editor =. JaCk-SAT:. Parallel Processing and Applied Mathematics, 7th International Conference,. 2007 , doi =

    2007

  38. [38]

    and Moskewicz, Matthew H

    Zhang, Lintao and Madigan, Conor F. and Moskewicz, Matthew H. and Malik, Sharad , title =. Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design , pages =. 2001 , isbn =

    2001

  39. [39]

    An Extensible SAT-solver

    E \'e n, Niklas and S \"o rensson, Niklas. An Extensible SAT-solver. Theory and Applications of Satisfiability Testing. 2004

    2004

  40. [40]

    Manquinho and In

    Ruben Martins and Vasco M. Manquinho and In. An overview of parallel. Constraints An Int. J. , volume =. 2012 , doi =

    2012

  41. [41]

    and Madigan, Conor F

    Moskewicz, Matthew W. and Madigan, Conor F. and Zhao, Ying and Zhang, Lintao and Malik, Sharad , title =. Proceedings of the 38th Annual Design Automation Conference , pages =. 2001 , isbn =. doi:10.1145/378239.379017 , abstract =

    work page doi:10.1145/378239.379017 2001

  42. [42]

    2015 , eprint=

    Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers , author=. 2015 , eprint=

    2015

  43. [43]

    The Effect of Restarts on the Efficiency of Clause Learning , booktitle =

    Jinbo Huang , editor =. The Effect of Restarts on the Efficiency of Clause Learning , booktitle =. 2007 , url =

    2007

  44. [44]

    Between Restarts and Backjumps

    Ramos, Antonio and van der Tak, Peter and Heule, Marijn , biburl =. Between Restarts and Backjumps. , url =. SAT , editor =. doi:10.1007/978-3-642-21581-0_18 , interhash =

    work page doi:10.1007/978-3-642-21581-0_18

  45. [45]

    Information Processing Letters , year =

    Michael Luby and Alistair Sinclair and David Zuckerman , title =. Information Processing Letters , year =

  46. [46]

    2011 , issn =

    On the power of clause-learning SAT solvers as resolution engines , journal =. 2011 , issn =. doi:10.1016/j.artint.2010.10.002 , author =

    work page doi:10.1016/j.artint.2010.10.002 2011

  47. [47]

    Proceedings of the 23rd National Conference on Artificial Intelligence - Volume 1 , pages =

    Hertel, Philipp and Bacchus, Fahiem and Pitassi, Toniann and Van Gelder, Allen , title =. Proceedings of the 23rd National Conference on Artificial Intelligence - Volume 1 , pages =. 2008 , isbn =

    2008

  48. [48]

    Clause Size Reduction with all-UIP Learning

    Feng, Nick and Bacchus, Fahiem. Clause Size Reduction with all-UIP Learning. Theory and Applications of Satisfiability Testing -- SAT 2020. 2020

    2020

  49. [49]

    Haixia Jia and Cristopher Moore and Doug Strain , title =. J. Artif. Intell. Res. , volume =. 2007 , doi =

    2007

  50. [50]

    Concurrent Clause Strengthening , booktitle =

    Siert Wieringa and Keijo Heljanko , editor =. Concurrent Clause Strengthening , booktitle =. 2013 , doi =

    2013

  51. [51]

    A fast parallel SAT-solver --- efficient workload balancing , journal=

    B. A fast parallel SAT-solver --- efficient workload balancing , journal=. 1996 , month=

    1996

  52. [52]

    CoRR , volume =

    Jerry Lonlac and Engelbert Mephu Nguifo , title =. CoRR , volume =. 2017 , url =

    2017

  53. [53]

    2014 IEEE 26th International Conference on Tools with Artificial Intelligence , title=

    L. 2014 IEEE 26th International Conference on Tools with Artificial Intelligence , title=. 2014 , volume=

    2014

  54. [54]

    Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence,

    Mao Luo and Chu-Min Li and Fan Xiao and Felip Manyà and Zhipeng Lü , title =. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence,. 2017 , doi =

    2017

  55. [55]

    Minimizing Learned Clauses

    S \"o rensson, Niklas and Biere, Armin. Minimizing Learned Clauses. Theory and Applications of Satisfiability Testing - SAT 2009. 2009

    2009

  56. [56]

    Williams and P

    Brian C. Williams and P. Pandurang Nayak , title =. Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence,. 1997 , url =

    1997

  57. [57]

    Knoblock , title =

    Craig A. Knoblock , title =. Artif. Intell. , volume =. 1994 , doi =

    1994

  58. [58]

    Scalable Gromov-Wasserstein Learning for Graph Partitioning and Matching , volume =

    Xu, Hongteng and Luo, Dixin and Carin, Lawrence , booktitle =. Scalable Gromov-Wasserstein Learning for Graph Partitioning and Matching , volume =

  59. [59]

    Vivifying Propositional Clausal Formulae , booktitle =

    C. Vivifying Propositional Clausal Formulae , booktitle =. 2008 , doi =

    2008

  60. [60]

    Proceedings of the Tenth National Conference on Artificial Intelligence , pages =

    Selman, Bart and Levesque, Hector and Mitchell, David , title =. Proceedings of the Tenth National Conference on Artificial Intelligence , pages =. 1992 , isbn =

    1992

  61. [61]

    SIGART Bull

    Gu, Jun , title =. SIGART Bull. , month = jan, pages =. 1992 , issue_date =. doi:10.1145/130836.130837 , abstract =

    work page doi:10.1145/130836.130837 1992

  62. [62]

    and Walsh, Toby , biburl =

    Gent, Ian P. and Walsh, Toby , biburl =. An Empirical Analysis of Search in GSAT. , url =. J. Artif. Intell. Res. (JAIR) , keywords =. doi:10.1613/jair.7 , interhash =

    work page doi:10.1613/jair.7

  63. [63]

    Kautz and Bram Cohen , editor =

    Bart Selman and Henry A. Kautz and Bram Cohen , editor =. Noise Strategies for Improving Local Search , booktitle =. 1994 , url =

    1994

  64. [64]

    Washington, DC

    I. P. Gent and T. Walsh , TITLE =. Proc. of AAAI-93 , ADDRESS = "Washington, DC", PAGES =

  65. [65]

    Tabu Search for

    Bertrand Mazure and Lakhdar Sais and. Tabu Search for. Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference,. 1997 , url =

    1997

  66. [66]

    McAllester and Bart Selman and Henry A

    David A. McAllester and Bart Selman and Henry A. Kautz , editor =. Evidence for Invariants in Local Search , booktitle =. 1997 , url =

    1997

  67. [67]

    , editor =

    John Thornton and Duc Nghia Pham and Stuart Bain and Valnir Ferreira Jr. , editor =. Additive versus Multiplicative Clause Weighting for. Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California,. 2004 , url =

    2004

  68. [68]

    Duc Nghia Pham and John Thornton and Charles Gretton and Abdul Sattar , title =. J. Satisf. Boolean Model. Comput. , volume =. 2008 , doi =

    2008

  69. [69]

    Hoos , editor =

    Holger H. Hoos , editor =. An Adaptive Noise Mechanism for WalkSAT , booktitle =. 2002 , url =

    2002

  70. [70]

    ICCAD 2001

    IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281) , title=. 2001 , volume=

    2001

  71. [71]

    , title =

    Cheeseman, Peter and Kanefsky, Bob and Taylor, William M. , title =. Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI) , year =

  72. [72]

    Mézard and G

    M. Mézard and G. Parisi and R. Zecchina , title =. Science , volume =. 2002 , doi =. https://www.science.org/doi/pdf/10.1126/science.1073287 , abstract =

    work page doi:10.1126/science.1073287 2002

  73. [73]

    Proceedings of the Twenty-Seventh

    Katsirelos, George and Sabharwal, Ashish and Samulowitz, Horst and Simon, Laurent , title =. Proceedings of the Twenty-Seventh. 2013 , url =

    2013

  74. [74]

    Proceedings of the Thirty-Second

    Francesco Leofante , title =. Proceedings of the Thirty-Second. 2018 , crossref =

    2018

  75. [75]

    2011 , issn =

    Results of the enumeration of Costas arrays of order 29 , journal =. 2011 , issn =. doi:10.3934/amc.2011.5.547 , author =

    work page doi:10.3934/amc.2011.5.547 2011

  76. [76]

    and Erickson, Keith G

    Russo, Jon C. and Erickson, Keith G. and Beard, James K. , booktitle=. Costas array search technique that maximizes backtrack and symmetry exploitation , year=

  77. [77]

    and Cenkl, M

    Brown, C.P. and Cenkl, M. and Games, R.A. and Rushanan, J.J. and Moreno, O. , booktitle=. New Enumeration Results for Costas Arrays , year=

  78. [78]

    and Rickard, S

    Drakakis, K. and Rickard, S. and Beard, J. K. and Caballero, R. and Iorio, F. and O'Brien, G. and Walsh, J. , title =. IEEE Trans. Inf. Theor. , month = oct, pages =. 2008 , issue_date =. doi:10.1109/TIT.2008.928979 , abstract =

    work page doi:10.1109/tit.2008.928979 2008

  79. [79]

    Dagster: Parallel Structured Search with Case Studies

    Burgess, Mark Alexander and Gretton, Charles and Milthorpe, Josh and Croak, Luke and Willingham, Thomas and Tiu, Alwen. Dagster: Parallel Structured Search with Case Studies. PRICAI 2022: Trends in Artificial Intelligence. 2022

    2022

  80. [80]

    Proceedings of the Twenty-Eighth International Conference on Automated Planning and Scheduling,

    Binda Pandey and Jussi Rintanen , title =. Proceedings of the Twenty-Eighth International Conference on Automated Planning and Scheduling,. 2018 , crossref =

    2018

Showing first 80 references.